[Haskell-cafe] A type level puzzle

[Richard Eisenberg]

On Aug 19, 2015, at 4:54 PM, Silvio Frischknecht <silvio.frischi at gmail.com> wrote:

>> 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.)
> 
> It's always nice to see things are happening. GHC is awesome.
> 
> The thing with the star also being a typeoperator is a bit unfortunate.
> I always thought it a bit inconsistent to use an operator lexem for
> typekind even though it's not an operator at all. A normal name would
> have done.

Agreed completely. But that backward-compatibility nightmare that this change would cause just isn't worth it.

> 
>> The bottom line: there is reason to hope that Haskell will have
>> dependent types within the next two years or so.
> 
> What exactly does that mean?
> 
> The ability to use normal functions, Ints and Strings at typelevel,
> instead of type families, Nats and Symbols.
> 
> or
> 
> Just have a type-level language that is similar to the commonly used
> type dependent languages.

While I'm not sure what will happen with Nat/Symbol vs Int/String yet, I am hoping that functions will just be able to be used in types. We'll see how it all works out. But I'm aiming more for the first description than the second.

As for timing: finishing an unpolished, not-ready-to-merge but functional implementation is part of my dissertation. I'm very much hoping to graduate by next summer, so there is a big incentive for me to actually get this done!

Richard