[Haskell-cafe] Haskell type system and the lambda cube
byorgey at seas.upenn.edu
Mon May 25 07:59:19 EDT 2009
On Sun, May 24, 2009 at 10:39:50AM +0200, Petr Pudlak wrote:
> On Sun, May 24, 2009 at 12:18:40PM +0400, Eugene Kirpichov wrote:
> > Haskell has terms depending on types (polymorphic terms) and types
> > depending on types (type families?), but no dependent types.
> But how about undecidability? I'd say that lambda2 or lambda-omega have
> undecidable type checking,
I don't think that's true. Unless I am mistaken, type checking is
decidable for all the vertices of the lambda cube.
> (BWT, will some future version of Haskell consider including some kind of
> dependent types?)
I doubt it. But there is a lot of current research into bringing as
much of the power of dependent types into the language (e.g. type
families) without actually bringing in all the headaches of
full-spectrum dependent types.
More information about the Haskell-Cafe