[Haskell-cafe] A type level puzzle

[Silvio Frischknecht]

> 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.

> 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.

Silvio