type families + GADT = type unsafety?
(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.
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.
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
| | 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
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
(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: tom.schrijvers@cs.kuleuven.be
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:Bulat.Ziganshin@gmail.com
participants (6)
-
Bulat Ziganshin -
Roberto Zunino -
Simon Peyton-Jones -
Stefan O'Rear -
Tom Schrijvers -
Wolfgang Jeltsch