[Haskell-cafe] Infinite types should be optionally allowed

[Job Vranish]

Thanks,
Perhaps my algorithm works then. I shall have to read up more on these
things :)

- Job

On Mon, Feb 21, 2011 at 4:54 PM, Luke Palmer <lrpalmer at gmail.com> wrote:

> 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
> >>> >>
> >>> >
> >>> >
> >>
> >
> >
> >
>
> _______________________________________________
> 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/20110222/99437b1c/attachment.htm>