Conversation

Notices

1. Embed this notice
   Jade Master (jademastermath@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 01:11:02 JST Jade Master

   In case you were curious, here's what it looks like to solve differential equations in Idris2 (it is so concise huh) https://gist.github.com/Jademaster/242d53a9070d55b790b5c15e0db22a4a

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 01:11:00 JST julesh

     in reply to

     @JadeMasterMath This is a direct port from haskell of the Escardo-Pavlovic trick, right?

   • Embed this notice
     Jade Master (jademastermath@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 01:59:53 JST Jade Master

     in reply to

     • julesh

     @julesh I'm not aware of that trick, I made this up myself just by following Euler's method for solving a diffeq. Maybe the one fancy-ish thing that they also did is the the use of streams to represent solutions?

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 02:04:06 JST julesh

     in reply to

     @JadeMasterMath Look at the paper "Calculus in coinductive form" (for some reason I can't find a pdf in the first 30 seconds). I'll be impressed if you found the same thing, because it's a very strong contender for "most beautiful program ever written in human history"

   • Embed this notice
     Jade Master (jademastermath@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 02:04:07 JST Jade Master

     in reply to

     • julesh

     @julesh But if you show me the code it reminds you of I'd love to compare :P

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 02:05:59 JST julesh

     in reply to

     @JadeMasterMath Here is the paper
     https://www.kestrel.edu/people/pavlovic/papers/lapl-LICS98.pdf
     but I guess I wrongly remembered that it contained haskell code, that must be somewhere else. Viktor Winschel used to have it taped to his wall

   • Embed this notice
     Jade Master (jademastermath@mathstodon.xyz)'s status on Thursday, 12-Dec-2024 02:19:23 JST Jade Master

     in reply to

     • julesh

     @julesh wow, I am impressed this kinda thing is so revered. Iirc that paper does a *lot* more than the code I wrote.. the main thing was some sort of characterization of Taylor's theorem using streams? I don't have anything close that yet...