hypertypes VS write-you-a-haskell

For the development of Lamdu I've embarked on a similar quest and ended up creating hypertypes after getting a helpful pointer in SO.

Otherwise I would go for modularity rather than extensibility and use hypertypes or an equivalent mechanism to represent the types.

Indeed, then it is definitely possible. i.e https://github.com/lamdu/hypertypes

Nice. Using this my type inference implementation benchmarked up to 2.5% faster and the switch wasn't difficult to do.

I think https://github.com/lamdu/hypertypes might be related. This is a generic programming API that seems to be based on hyperfunctions, but moved up to the type level?

I wrote an overview for several approaches folks came up with for this problem aka "the expression problem" including my own approach, "hypertypes" - see https://github.com/lamdu/hypertypes/blob/master/README.md

I highly recommend https://github.com/sdiehl/write-you-a-haskell as it is very developer friendly. It’s not complete, but it really gets the gears turning and will set you up for writing your own Hendley-Milner style type checker.

This is the best resource I know of: http://dev.stephendiehl.com/fun/006\_hindley\_milner.html https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs

I feel like Write You A Haskell was set out to introduce some of these foundational concepts in the right order: lambda calculus, to system-f to core - but that's more of a skeleton, right? What about logic? proofs? Is there anything else ... that can all be put together to create a "course" of some sort to master the theoretical concepts that Haskell stands upon?