Equirecursive types?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Equirecursive types?

Jim Apple-3
According to Pierce's book, O'Caml has an optional equirecursive type
extension that turns off the occurs check. Is there any particular
reason Haskell doesn't have that available?

Here's what got me thinking about it:
http://lambda-the-ultimate.org/node/1360#comment-15656

Jim
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equirecursive types?

Ross Paterson
On Sun, Mar 26, 2006 at 01:22:17PM -0500, Jim Apple wrote:
> According to Pierce's book, O'Caml has an optional equirecursive type
> extension that turns off the occurs check. Is there any particular
> reason Haskell doesn't have that available?

It's certainly feasible, though turning off the occurs check doesn't
do it: you need to use the unification algorithm for regular trees (see
e.g. section 6.7 of the revised Dragon Book).  You also need to decide
what to do about

        type T = T

I think the arguments against it are:
 * many common errors will lead to perfectly legal types.
 * it adds convenience, but not expressive power.
 * it only works for regular types, where the arguments of uses of the
   type constructor on the rhs are the same as (or a permutation of)
   the arguments on the lhs, so this is out:

        type T a = Either a (T (a,a))

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equirecursive types?

John Hughes-4
In reply to this post by Jim Apple-3

>From: Ross Paterson <[hidden email]>
>
>On Sun, Mar 26, 2006 at 01:22:17PM -0500, Jim Apple wrote:
>  
>
>>According to Pierce's book, O'Caml has an optional equirecursive type
>>extension that turns off the occurs check. Is there any particular
>>reason Haskell doesn't have that available?
>>    
>>
>
>It's certainly feasible, though turning off the occurs check doesn't
>do it: you need to use the unification algorithm for regular trees (see
>e.g. section 6.7 of the revised Dragon Book).  You also need to decide
>what to do about
>
> type T = T
>
>I think the arguments against it are:
> * many common errors will lead to perfectly legal types.
> * it adds convenience, but not expressive power.
> * it only works for regular types, where the arguments of uses of the
>   type constructor on the rhs are the same as (or a permutation of)
>   the arguments on the lhs, so this is out:
>
> type T a = Either a (T (a,a))
>
>  
>
Indeed, error messages in common cases would be worsened significantly,
because as Ross says, common errors (such as forgetting a parameter in a
recursive call) would lead to legal definitions that cause a type error
when applied. Partly for this reason, OCaml permits recursion only in
object types, if I remember rightly, where it's most useful. In other
cases the occurs check is still used.

John

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equirecursive types?

lee marks-2
In reply to this post by Jim Apple-3
John Hughes wrote:
> ...
> >
> Indeed, error messages in common cases would be worsened significantly,
> because as Ross says, common errors (such as forgetting a parameter in a
> recursive call) would lead to legal definitions that cause a type error
> when applied. Partly for this reason, OCaml permits recursion only in
> object types, if I remember rightly, where it's most useful. In other
> cases the occurs check is still used.
>

Couldn't this be mitigated by requiring an explicit type annotation on the function being called
recursively? In other words infinite types are never silently inferred, but can only coincide with
explicit signatures.

So this is legal:

  type Fix s a = s a (Fix s a)

  fold :: Functor (s a) => (s a b -> b) -> Fix s a -> b
  fold f = f . fmap (fold f)

but this is not:

  fold f = f . fmap (fold f)


I guess it just seems that banning infinite types altogether is throwing the baby with the bath.



__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around
http://mail.yahoo.com 
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: Equirecursive types?

ihope
On 3/27/06, lee marks <[hidden email]> wrote:

> So this is legal:
>
>   type Fix s a = s a (Fix s a)
>
>   fold :: Functor (s a) => (s a b -> b) -> Fix s a -> b
>   fold f = f . fmap (fold f)
>
> but this is not:
>
>   fold f = f . fmap (fold f)

data Fix s a = Fix {runFix :: s a (Fix s a)}

fold :: Functor (s a) => (s a b -> b) -> Fix s a -> b
fold f g = f . fmap (fold f) . runFix

Yes, we can build infinite types :-) My favorite so far:

data Self a = Self {runSelf :: Self a -> a}
fix f = (\(Self g) -> f (g (Self g))) (Self (\(Self g) -> f (g (Self g))))

That one seems to give GHCi something to think about! Adding a type
annotation doesn't help.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe