Re: GADTs and functional dependencies

23 Sep 2008


      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
-}
class Class a b | a -> b where
  fun :: GADT a -> b
instance Class () () where
  fun GADT = ()
instance Class String Bool where
  fun GADT2 = True
main = print $ (fun GADT, fun GADT2) == ( (), True )

Re: GADTs and functional dependencies

Chris Kuklewicz