On Fri, 2007-09-14 at 10:42 +1200, ok wrote: > I wrote: > >> Since not all Turing machines halt, and since the halting problem is > >> undecidable, this means not only that some Haskell programs will make > >> the type checker loop forever, but that there is no possible meta- > >> checker that could warn us when that would happen. > > On 13 Sep 2007, at 4:27 pm, Stefan Holdermans wrote: > > Do not forget that both functional dependencies and associated > > types come with syntactic restrictions that are there just to > > "tame" the Turing completeness, i.e., to guarantee that type > > checking will actually terminate. > > I don't know anything about associated types, so can't comment on those. > But on the subject of functional dependencies, you and the author of the > article in Monad.Reader 8 *cannot* both be right, because the whole > point of that article is to explain how to program in the type system, > using, amongst other things, conditionals and recursion, in such a way > that a Turing machine can surely be simulated. If there is some > restriction to guarantee termination, then those techniques can't work. > > > > > Admittedly, it's my experience that whenever one wants to do > > something interesting (and here I mean "interesting" in a way that > > you would probably label as "rather twisted" ;-)), one has to > > bypass these restrictions (and, hence, allow for potentially > > undecidable instances). > > Ah, now we have it. To quote Conrad Parker: > This tutorial uses the Haskell98 type system extended with > multi-parameter typeclasses and undecidable instances. > We need to enable some GHC extensions to play with this type- > hackery: > $ ghci -fglasgow-exts -fallow-undecidable-instances > > That is the combination I'm talking about. > > > Now, I haven't really worked with associated types (or, for that > > matter, associated type synonyms), but my hope is that, when using > > those, turning off the checks is needed less often. We'll see. > > If you hope that, then we probably agree more than you might think. > My point is that the combination exists and is being explained so that > people can use it, and that the result is comparable in C++. (Imagine > Dame Edna Everage saying "I mean that in a loving way, possums.")
The type system doesn't help you avoid writing non-terminating programs, so i see no problem with it being possible giving programmers the power to express and check more complex properties of their programs -- as long as type-checking remains sound. From a practical standpoint, non-terminating type checks are just as much a bug as non-terminating library functions. Type systems need more thought anyways, so why not make sure it's terminating, too? The other extreme is to use dependent types everywhere, but this has a bit more drastic consequences to the accessibility and practicality of the language. I don't think this will become a mainstream tool any time soon, but it may turn out to be very valuable to library authors. We also shouldn't forget that this is a brand-new feature and requires proper evaluation; how better could this be achieved than by having it included as an optional feature in a mature and well-used compiler? I am glad that Haskellers try to integrate theory and practice that nicely. / Thomas _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe