[Haskell-cafe] Infinite types should be optionally allowed
jvranish at gmail.com
Sat Feb 14 16:06:23 EST 2009
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
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 <lrpalmer at gmail.com> wrote:
> On Fri, Feb 13, 2009 at 4:04 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
>> On Fri, Feb 13, 2009 at 3:13 PM, Job Vranish <jvranish at 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:
>>> 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
> 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.
>>> 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 at haskell.org
More information about the Haskell-Cafe