type families + GADT = type unsafety?

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

type families + GADT = type unsafety?

Roberto Zunino-2
(Trac reports "database locked", posting here...)

Here's unsafeCoerce:

> type family Const a
> type instance Const a = ()
>
> data T a where T :: a -> T (Const a)
>
> coerce :: forall a b . a -> b
> coerce x = case T x :: T (Const b) of
>            T y -> y

And this indeed "works"... Here's the result with the latest RC:

*TypeFam> coerce () 2
<interactive>: internal error: stg_ap_v_ret
    (GHC version 6.9.20070918 for x86_64_unknown_linux)
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
Aborted

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

Re: type families + GADT = type unsafety?

Roberto Zunino-2
Roberto Zunino wrote:
> (Trac reports "database locked", posting here...)

For those interested, here are the follow-ups:

http://hackage.haskell.org/trac/ghc/ticket/1723

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

Re: type families + GADT = type unsafety?

Wolfgang Jeltsch-2
Am Donnerstag, 27. September 2007 15:27 schrieb Roberto Zunino:
> Roberto Zunino wrote:
> > (Trac reports "database locked", posting here...)
>
> For those interested, here are the follow-ups:
>
> http://hackage.haskell.org/trac/ghc/ticket/1723
>
> Regards,
> Zun.

simonpj writes there:
> Manuel is about to nuke the old GADT stuff in favour of the new type-family
> stuff.

This doesn’t mean that GADTs are being dropped in favor of type families, does
it?

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

RE: type families + GADT = type unsafety?

Simon Peyton Jones
|
| simonpj writes there:
| > Manuel is about to nuke the old GADT stuff in favour of the new type-
| family
| > stuff.
|
| This doesn’t mean that GADTs are being dropped in favor of type
| families, does
| it?
|

No... it's an implementation matter only, invisible to programmers

Simon

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

Re: type families + GADT = type unsafety?

Stefan O'Rear
In reply to this post by Wolfgang Jeltsch-2
On Thu, Sep 27, 2007 at 04:59:49PM +0200, Wolfgang Jeltsch wrote:

> Am Donnerstag, 27. September 2007 15:27 schrieb Roberto Zunino:
> > Roberto Zunino wrote:
> > > (Trac reports "database locked", posting here...)
> >
> > For those interested, here are the follow-ups:
> >
> > http://hackage.haskell.org/trac/ghc/ticket/1723
> >
> > Regards,
> > Zun.
>
> simonpj writes there:
> > Manuel is about to nuke the old GADT stuff in favour of the new type-family
> > stuff.
>
> This doesn’t mean that GADTs are being dropped in favor of type families, does
> it?
They are being dropped - from the typechecker.  The old syntax will
still work.

data Foo a where
   A :: Foo Int
   B :: Foo Bool


becomes

data Foo a = (a ~ Int) => A | (a ~ Bool) => B

(ignoring the H98 context issue).

Then, in a case statement, traditional GADT refinement reduces to a
special case of equality constraint discharging.  (Simon, does this mean
that non-~ discharging will become subject to GADT-style type annotation
rules?)

Stefan

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

signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: type families + GADT = type unsafety?

Tom Schrijvers-2
> (Simon, does this mean
> that non-~ discharging will become subject to GADT-style type annotation
> rules?)

No, it does not. No type annotations required in non-GADT-related code,
even if equalities are involved.

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re[2]: type families + GADT = type unsafety?

Bulat Ziganshin-2
In reply to this post by Stefan O'Rear
Hello Stefan,

Friday, September 28, 2007, 1:10:09 AM, you wrote:

> data Foo a where
>    A :: Foo Int
>    B :: Foo Bool

> becomes

> data Foo a = (a ~ Int) => A | (a ~ Bool) => B

hm :)  this looks like my quasi-proposal of unifying data and function
definitions still has some meaning. i proposed to define GADTs as

data Foo Int  = A
     Foo Bool = B

but, with help of guards, this may be also written as

data Foo a | a==Int  = A
           | a==Bool = B

next step should be to add pattern guards? :)


--
Best regards,
 Bulat                            mailto:[hidden email]

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