On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz
<[EMAIL PROTECTED]> wrote:
> You cannot create a normal function "fun". You can make a type class
> function
>
> fun :: Class a b => GADT a -> b
>
>> data GADT a where
>> GADT :: GADT ()
>> GADT2 :: GADT String
>>
>> -- fun1 :: GADT () -> () -- infers type
>> fun1 g = case g of
>> (GADT :: GADT ()) -> ()
>>
>> -- fun2 :: GADT String -> Bool -- infers type
>> fun2 g = case g of
>> (GADT2 :: GADT String) -> True
>>
>> -- "fun" cannot type check. The type of 'g' cannot be both "GADT ()" and
>> "GADT String"
>> -- This is because "fun" is not a member of type class.
>> {- fun g = case g of
>> (GADT :: GADT ()) -> ()
>> (GADT2 :: GADT String) -> True
>> -}
It may be that fun cannot type check, but surely it isn't for the
reason you've given.
data Rep a where
Unit :: Rep ()
Int :: Rep Int
zero :: Rep a -> a
zero r = case r of
Unit -> ()
Int -> 0
The type of r is "both" Rep () and Rep Int. No type class needed.
If I had to guess, I'd say the original problem is that any
specialization triggered by the functional dependency happens before
the specialization triggered by pattern matching on the GADT. If I
recall correctly, it is known that GADTs and fundeps don't always work
nicely together.
The example does seem to work if translated to use type families.
type family Fam t :: *
type instance Fam () = ()
data GADT a where
GADT :: GADT ()
fun :: GADT a -> Fam a
fun GADT = ()
--
Dave Menendez <[EMAIL PROTECTED]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
