« Tying the knot » in #Haskell, #Idris and #OCaml : https://gitlab.com/chupin/tying-the-knot
Context: this week was the Midlands Graduate School (http://www.cs.nott.ac.uk/~psznhn/MGS2018/) in Nottingham. This was super cool, with many interesting courses and people!
The invited course was given by Edwin Brady on Idris. The above is the result of an interrogation of my supervisor: Idris is strict with explicitly lazy values, so is it powerful enough to apply some classical tying the knot tricks that make use of laziness?
However, because I use a fixed-point combinator, my implementation won't pass the totality checker, so I'm looking for a solution that will. Someone mentioned histomorphisms and dynamorphisms to me, I'm looking if something based on that will do the trick.
Oh and a little Idris flaw, when evaluating a lazy value, the result is not cached (you can see it if you use unsafePerformIO ;) ), so this make this sort of circular programming a bit pointless (at least for now)^^
So I implemented one of this classical problem (look at the README on Gitlab for a description), and the answer is yes! I first did it in OCaml (that I know much better than Idris), and then ported the OCaml version to Idris.
A nice thing about Idris is that the compiler is able to infer where to put Lazy and Force, so you don't have to write them yourself. That makes the Idris code much nicer to read :)