[Haskell-cafe] Haskell type system and the lambda cube

[Petr Pudlak]

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, whereas Haskell's Hindley-Milner type system is
decidable. From this I get that Haskell's type system can't be one of the
vertices of the cube.

(BWT, will some future version of Haskell consider including some kind of
dependent types?)

Petr

> 
> 2009/5/24 Petr Pudlak <deb at pudlak.name>:
> > Hi, I'm trying to get some better understanding of the theoretical foundations
> > behind Haskell. I wonder, where exactly does Haskell type system fit within the
> > lambda cube? <http://en.wikipedia.org/wiki/Lambda_cube>
> > I guess it could also vary depending on what extensions are turned on.
> >
> >    Thanks, Petr
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> 
> 
> 
> -- 
> Eugene Kirpichov
> Web IR developer, market.yandex.ru