Haskell Apostasy #1: now where did they hide the higher-ranked polymorphism?
Tue, Dec 02, 2014./hacking/ocaml | LinkAbout fifteen years after it was cool (to type systems people), I figured it was time for me to try ocaml, or more broadly, to make my peace with this call-by-value thing. One motivation was because I work with a Frenchman, and another was that I want more space- and time-efficiency than Haskell allows. No, I'm not listening to you talk asymptotics or microbenchmarks or parallelism. So, where else to start than by trying to port Bird and Paterson's de Bruijn encoding? (Edward Kmett's recent work places this scheme in the vast terrain of representations of higher-order languages and sets the bar for type insanity / wizardry.)
Here's what I ended up with: Bird_Paterson_deBruijn.ml.
You'll see that I ran out of patience / interest in working out a full showE function for the efficient representation. I think you're supposed to normalise it first and use showT. As I observe in the file, Yallop and White have thought about how to massage the syntactic overhead of higher-ranked polymorphism (think Haskell's functors, monads, traversables, this crazy nested datatype stuff, etc.).
I came to think that ocaml's module and object systems (really row polymorphism) give Haskell's baroque combination of features some solid competition. I like being able to define lightweight namespaces that actually do encapsulate things. The uniformity of ocaml's type declarations (just say type) is awesome, and would be even more awesome if they'd wired row polymorphism in there too, rather than adding a whole pile of constructs for an object-oriented style that is foreign to just about everyone. I don't care about the fine details of syntax but would observe that its treatment of user-defined operators frankly sucks. *shrug*
Note that Bird and Paterson's scheme is a non-starter in Standard ML due to the latter not supporting polymorphic recursion.
I also tried to test this representation using an ad hoc QuickCheck-alike, using Pierre Lescanne's ideas about generating λ-terms. As Oleg shows, it takes some doing to generate interesting ones. More on this later perhaps.
