newtype and existentials

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

newtype and existentials

Ralf Hinze
Is there a strong reason why

> {-# OPTIONS -fglasgow-exts #-}
> data Type :: (* -> *) where
>   Int   ::  Type Int
> data Dynamic  =  forall a . Dyn (a, Type a)

works, but not

> newtype Dynamic  =  forall a . Dyn (a, Type a)

Cheers, Ralf
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

RE: newtype and existentials

Simon Peyton Jones
yes.  a newtype declares a new type isomorphic to an existing type.  
        newtype T = MkT S
declares T to be isomorphic to S.

There is no existing Haskell type isomorphic to your Dynamic.

In concrete terms, the newtype constructor is discarded before we get to
System F; but we can't do that with an existential.

S

| -----Original Message-----
| From: [hidden email]
[mailto:glasgow-haskell-bugs-
| [hidden email]] On Behalf Of Ralf Hinze
| Sent: 18 November 2005 13:28
| To: [hidden email]
| Subject: newtype and existentials
|
| Is there a strong reason why
|
| > {-# OPTIONS -fglasgow-exts #-}
| > data Type :: (* -> *) where
| >   Int   ::  Type Int
| > data Dynamic  =  forall a . Dyn (a, Type a)
|
| works, but not
|
| > newtype Dynamic  =  forall a . Dyn (a, Type a)
|
| Cheers, Ralf
| _______________________________________________
| Glasgow-haskell-bugs mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

Re: newtype and existentials

Tomasz Zielonka
In reply to this post by Ralf Hinze
On Fri, Nov 18, 2005 at 02:28:28PM +0100, Ralf Hinze wrote:

> Is there a strong reason why
>
> > {-# OPTIONS -fglasgow-exts #-}
> > data Type :: (* -> *) where
> >   Int   ::  Type Int
> > data Dynamic  =  forall a . Dyn (a, Type a)
>
> works, but not
>
> > newtype Dynamic  =  forall a . Dyn (a, Type a)

I am not an expert in this area, but let's try to guess.

My guess is that there is no strong reason and the rule that
existentials can be only used in 'data' declarations is a bit
too restrictive. Usually, you restrict the existentially
quantified types to some type-classes. This requires storing
the type-class dictionaries in the data constructor, which
changes the representation of the type, so newtype can't be
used.

In your case you don't use type-class context to restrict 'a',
so it should be possible to use newtype. But the compiler
is not so smart to see this and it rejects this code anyway.

Did I win something? ;-)

Best regards
Tomasz
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

Re: newtype and existentials

Ralf Hinze
In reply to this post by Simon Peyton Jones
> yes.  a newtype declares a new type isomorphic to an existing type.  
>         newtype T = MkT S
> declares T to be isomorphic to S.
>
> There is no existing Haskell type isomorphic to your Dynamic.

Following your reasoning, shouldn't GHC also reject

> newtype D = D (D -> D)

because there is no existing Haskell type isomorphic to D? And
certainly, System F doesn't have recursive types either.

Cheers, Ralf
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

RE: newtype and existentials

Simon Peyton Jones
In reply to this post by Ralf Hinze
maybe so.  GHC does indeed treat recursive newtypes specially.  But I don't like that; it's a wart in the intermediate language.  But it's a wart I'd like to shrink, not grow.

S

| -----Original Message-----
| From: Ralf Hinze [mailto:[hidden email]]
| Sent: 18 November 2005 13:40
| To: Simon Peyton-Jones
| Cc: [hidden email]
| Subject: Re: newtype and existentials
|
| > yes.  a newtype declares a new type isomorphic to an existing type.
| >         newtype T = MkT S
| > declares T to be isomorphic to S.
| >
| > There is no existing Haskell type isomorphic to your Dynamic.
|
| Following your reasoning, shouldn't GHC also reject
|
| > newtype D = D (D -> D)
|
| because there is no existing Haskell type isomorphic to D? And
| certainly, System F doesn't have recursive types either.
|
| Cheers, Ralf
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

Re: newtype and existentials

Ross Paterson
In reply to this post by Simon Peyton Jones
On Fri, Nov 18, 2005 at 01:31:46PM -0000, Simon Peyton-Jones wrote:
> yes.  a newtype declares a new type isomorphic to an existing type.  
> newtype T = MkT S
> declares T to be isomorphic to S.
>
> There is no existing Haskell type isomorphic to your Dynamic.
>
> In concrete terms, the newtype constructor is discarded before we get to
> System F; but we can't do that with an existential.

The first argument, but not the second, also applies to

        newtype T = MkT (forall a. S)

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

RE: newtype and existentials

Simon Peyton Jones
In reply to this post by Ralf Hinze
true.  GHC's intermediate language has first-class universal
quantification, but not first-class existentials. I can't claim that is
the Right Thing, but it might explain why GHC at least makes the choices
it does

Simon

| -----Original Message-----
| From: Ross Paterson [mailto:[hidden email]]
| Sent: 18 November 2005 13:44
| To: Simon Peyton-Jones
| Cc: Ralf Hinze; [hidden email]
| Subject: Re: newtype and existentials
|
| On Fri, Nov 18, 2005 at 01:31:46PM -0000, Simon Peyton-Jones wrote:
| > yes.  a newtype declares a new type isomorphic to an existing type.
| > newtype T = MkT S
| > declares T to be isomorphic to S.
| >
| > There is no existing Haskell type isomorphic to your Dynamic.
| >
| > In concrete terms, the newtype constructor is discarded before we
get to
| > System F; but we can't do that with an existential.
|
| The first argument, but not the second, also applies to
|
| newtype T = MkT (forall a. S)

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs