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. -Brent _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
