Recent searches
Search options
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
@JadeMasterMath This is a direct port from haskell of the Escardo-Pavlovic trick, right?
@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?
@julesh But if you show me the code it reminds you of I'd love to compare :P
@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"
@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
@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...