[Haskell-cafe] Infinite types should be optionally allowed

[Job Vranish]

Sorry for bringing back an ancient thread but I'd still like to understand
this better.

It is still not obvious to me why typechecking infinite types is so hard. Is
determining type 'equivalence' the hard part? or is that a separate issue?


I wrote a simple infinite type inferer and made an attempt at an algorithm
that can answer your question.

The algorithm works like this: Given two types *a* and *b*: unify *a* with *
b*, if the resulting type is 'equivalent' to the original *a,* then *b* must
be (I think) at least as general as *a*.

To determine equivalence, I start with the head of both types (which are
represented as graphs) and check to see if the constructors are the same. If
they are then I set those two nodes 'equal' and recurse with the children.
It's a 'destructive' algorithm that effectively 'zips' the two graphs
together. It returns false if it encounters two constructors that are
different.


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 :)

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<http://www.nabble.com/There%27s-nothing-wrong-with-infinite-types%21-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
>> >>
>> >
>> >
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110220/f9f3c4f6/attachment.htm>