I'm pretty sure that the problem is decidable, at least with haskell 98 types (other type extensions may complicate things a bit). It ends up being a graph unification algorithm. I've tried some simple algorithms and they seem to work.
What do you mean by "the inference engine is only half of the story"? >From what I understand, the inference engine infers types via unification, if the types unify, then the unified types are the inferred types, if the types don't unify, then type check fails. Am I missing/misunderstanding something? I almost think that the problem might be solvable by just generating the appropriate newtype whenever an infinite type shows up, and doing the wrapping/unwrapping behind the scenes. This would be a hacked up way to do it, but I think it would work. On Fri, Feb 13, 2009 at 6:09 PM, Luke Palmer <lrpal...@gmail.com> wrote: > On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer <lrpal...@gmail.com> wrote: >> >> On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish <jvran...@gmail.com> wrote: >>> >>> There are good reasons against allowing infinite types by default >>> (mostly, that a lot of things type check that are normally not what we >>> want). An old haskell cafe conversation on the topic is here: >>> >>> http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types!-td7713737.html >>> >>> However, I think infinite types should be allowed, but only with an >>> explicit type signature. In other words, don't allow infinite types to >>> be inferred, but if they are specified, let them pass. I think it >>> would be very hard to shoot yourself in the foot this way. > > Oops! I'm sorry, I completely misread the proposal. Or read it correctly, > saw an undecidability hiding in there, and got carried away. > > What you are proposing is called equi-recursive types, in contrast to the > more popular iso-recursive types (which Haskell uses). There are plentiful > undecidable problems with equi-recursive types, but there are ways to pull > it off. The question is whether these ways play nicely with Haskell's type > system. > > But because of the fundamental computational problems associated, there > needs to be a great deal of certainty that this is even possible before > considering its language design implications. > >> >> That inference engine seems to be a pretty little proof-of-concept, >> doesn't it? But it is sweeping some very important stuff under the carpet. >> >> The proposal is to infer the type of a term, then check it against an >> annotation. Thus every program is well-typed, but it's the compiler's job >> to check that it has the type the user intended. I like the idea. >> >> But the inference engine is only half of the story. It does no type >> checking. Although checking is often viewed as the easier of the two >> problems, in this case it is not. A term has no normal form if and only if >> its type is equal to (forall a. a). You can see the problem here. >> >> Luke >> >>> >>> >>> Newtype is the standard solution to situations where you really need >>> an infinite type, but in some cases this can be a big annoyance. Using >>> newtype sacrifices data type abstraction and very useful type classes >>> like Functor. You can use multiparameter type classes and functional >>> dependencies to recover some of the lost abstraction, but then type >>> checking becomes harder to reason about and the code gets way more >>> ugly (If you doubt, let me know, I have some examples). Allowing >>> infinite types would fix this. >>> >>> I'm imagining a syntax something like this: >>> someFunctionThatCreatesInfiniteType :: a -> b | b = [(a, b)] >>> >>> Thoughts? Opinions? Am I missing anything obvious? >>> >>> - Job >>> _______________________________________________ >>> 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