[Haskell-cafe] A type level puzzle

[Richard Eisenberg]

On Aug 18, 2015, at 12:52 PM, Silvio Frischknecht <silvio.frischi at gmail.com> wrote:

>> I would avoid it, Haskell's type system is not a nice programming
>> language to work with
> 
> Do you know why this is so?

Here's my take: the type-level programming features have been added one-at-a-time, without a coherent attempt to make a "type-level programming language". So it's missing some niceties, like case statements in type family definitions and local definitions. Some of these are easier to add than others. (Actually, the two I've listed here wouldn't be bad. Lambda is another story, though.)

> And why dependent types are such a problem
> in Haskell?

No existing dependently typed language can infer the type of `length` from its body. But a dependently typed Haskell must do so. From a practical standpoint, GHC is just really big. And adding dependent types is a pervasive change that takes a *lot* of time.

My dissertation (github.com/goldfirere/thesis) is about adding dependent types to GHC. I believe I've solved the first problem, basically by copying Adam Gundry's approach (http://adam.gundry.co.uk/pub/thesis/). Still working on that practical problem, though. Expect some changes in time for 7.12 though. (See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1 for some discussion here.)

The bottom line: there is reason to hope that Haskell will have dependent types within the next two years or so.

Richard