[Haskell-cafe] Infinite types should be optionally allowed

Luke Palmer lrpalmer at gmail.com
Mon Feb 21 22:54:33 CET 2011


On Sun, Feb 20, 2011 at 6:01 PM, Job Vranish <jvranish at gmail.com> wrote:
> My current algorithm says that neither of the types you gave is strictly
> more general than the other, which I'm guessing is probably not true. I'm
> curious what the correct answer is and would appreciate someone pointing out
> the flaw in my reasoning/code :)

I don't remember how I constructed those terms, and I admit that I was
arguing out of my depth.  I really should have exposed my construction
-- we're all good engineers here, we know the difference between an
algorithm and intuition.

Things I have read since have suggested that I was wrong.  Pierce's
Types and Programming Languages has a chapter on equi-recursive types
which, if it does not provide insight itself, I'm sure has references
to papers that go into all the detail needed to answer this technical
question.

Luke

> My test code is on github here: https://github.com/jvranish/InfiniteTypes
> Also, is there a book you'd recommend that would explain this in further
> detail?
> Thanks,
> - Job
>
> On Mon, Feb 16, 2009 at 5:16 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
>>
>> On Sat, Feb 14, 2009 at 2:06 PM, Job Vranish <jvranish at gmail.com> wrote:
>>>
>>> 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?
>>
>> Sorry it took me so long to respond.  It took a while to formulate this
>> example.
>>
>> Here are two (convoluted) functions, passed to the fixtypes inference
>> engine:
>>
>> Expr> y (b (c i) (c (b b (b c (c i)))))
>> (fix b . (a -> b -> (a -> c -> d) -> d) -> c) -> c
>> Expr> y (b (c i) (b (c (b b (b c (c i)))) (b (c i) k)))
>> (fix c . ((a -> ((b -> c) -> d) -> (a -> d -> e) -> e) -> f) -> f)
>>
>> These are somewhat complex types; sorry about that.  But here's a
>> challenge:  is one of these types more general than the other?  For example,
>> if you wrote the first term and gave the second signature, should it
>> typecheck?  If you figure it out, can you give an algorithm for doing so?
>>
>> I'm not going to say how I came up with these functions, because that
>> would give away the answer :-)
>>
>> Luke
>>
>>>
>>>
>>> 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:
>>> >>>
>>> >>>
>>> >>> 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 at haskell.org
>>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> >>
>>> >
>>> >
>>
>
>
>



More information about the Haskell-Cafe mailing list