[Haskell-cafe] Infinite types should be optionally allowed

[Job Vranish]

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