Polymorphism

[treeowl]

You mentioned in the talk that the GADT technique you discussed in the talk does not support polymorphism, but it seems that it actually is possible, although not easy (I'm working through it rather slowly). Take a look at Embedding F by Sam Lindley. They describe embeddings of System F in Haskell, O'Caml, and F_ω, and even an embedding of F_ω in Haskell .

[treeowl]

In some ways, https://www.haskell.org/pipermail/haskell-cafe/2007-December/037246.html looks even more interesting, though older. I think its undefined uses can probably all be replaced by Proxy these days.

[bmsherman]

Thanks for posting these interesting articles! Good finds! I figured that there should be a way to encode polymorphism using a datatype if the type operator was already known in advance, but couldn't think of any ways to realize general type-level lambdas. The Lindley article has the same opinion I did:

The need to define a new type constructor for each polymorphic type is inconvenient, but it seems unavoidable given that type constructors are not first-class in Haskell.

But that Haskell-Cafe email looks like it did find a way to get arbitrary type-level lambdas to work! It uses a neat trick to express the polymorphism. It's not perfect, and as a consequence of this trick, you can abuse the type-lambda by restricting it to an arbitrary type if you want, and then you are only allowed to apply it to the correct type. The Lindley article, and myself as well, wanted to hide the type variable so you can't mess with it like that. But it's actually really neat and a great workaround!

[treeowl]

I admit I'm still very far from understanding either of them. The Lindley article leaves that really annoying bit open. The code referenced in the email looks promising. My vague impression is that it does something related to an idea I was thinking about, allowing expressions to be constructed with polymorphic types and then only constraining those types at the very top level. But it's full of incomplete patterns and error calls and such, and I don't yet have a clue if it's possible to clean those up. I also don't know if either of these techniques would let you write a "type checker" converting a plain old AST for System F to the typed version for execution. Lindley-style, I'm imagining that if it's possible it will involve some fairly horrible pain with newtypes representing SKI or something. Unrelatedly, I strongly suspect that the Iso class Lindley uses could today be replaced by Coercible, with both inject and project replaced by coerce.