[Haskell-cafe] Infinite types should be optionally allowed

[Luke Palmer]

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.


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/20090213/fa3bf9af/attachment.htm