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 <[email protected]>: > > 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 > > [email protected] > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > > > -- > Eugene Kirpichov > Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
