Type checking is decidable for all of the lambda cube, but not type inference.
Haskell 98 is a subset of Fw, Haskell with extensions is an superset of Fw. -- Lennart On Mon, May 25, 2009 at 12:59 PM, Brent Yorgey <byor...@seas.upenn.edu> wrote: > 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 > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe