Recursive replacement in GADT

Question

Let's say I have the following GADT AST:

data O abc where Add :: O aaa Eq :: O ab Bool --... more operations data Tree a where N :: (O abc) -> Tree a -> Tree b -> Tree c L :: a -> Tree a 

Now I want to build a function that replaces all L (eave) s of type a in the tree, something like this:

 f :: a -> Tree b -> Tree b fx (L a) | typeof x == typeof a = L x fx (L a) = L a fx (N oab) = N o (fxa) (fxb) 

Is it possible to build such a function? (using classes, maybe?) Can it be done if changes are made to the GADT?

I already have a typeof function: typeof :: a -> Type inside the class.

Answer 1

The trick is to use type witnesses: http://www.haskell.org/haskellwiki/Type_witness

 data O abc where Add :: O aaa Eq :: O ab Bool instance Show (O abc) where show Add = "Add" show Eq = "Eq" data Tree a where T :: (Typeable a, Typeable b, Typeable c) => (O abc) -> Tree a -> Tree b -> Tree c L :: a -> Tree a instance (Show a) => Show (Tree a) where show (T oab) = "(" ++ (show o) ++ " " ++ (show a) ++ " " ++ (show b) ++ ")" show (L a) = (show a) class (Show a) => Typeable a where witness :: a -> Witness a instance Typeable Int where witness _ = IntWitness instance Typeable Bool where witness _ = BoolWitness data Witness a where IntWitness :: Witness Int BoolWitness :: Witness Bool dynamicCast :: Witness a -> Witness b -> a -> Maybe b dynamicCast IntWitness IntWitness a = Just a dynamicCast BoolWitness BoolWitness a = Just a dynamicCast _ _ _ = Nothing replace :: (Typeable a, Typeable b) => a -> b -> b replace ab = case dynamicCast (witness a) (witness b) a of Just v -> v Nothing -> b f :: (Typeable a, Typeable b) => b -> Tree a -> Tree a fx (L a) = L $ replace xa fx (T oab) = T o (fxa) (fxb) 

Answer 2

I do not think this is possible with the current GADT if you are not able to have a partially defined function. You can write

 --f :: (Typeable a, Typeable b) => a -> Tree b -> Tree a fx (L a) | show (typeOf x) == show (typeOf a) = L x 

but you cannot make this function final because you will need

  | otherwise = L a 

and this is not typical, since you just proved that L a :: Tree a and L x :: Tree x are different types.

However, if you define GADT as existentially quantified

 data Tree where N :: (O abc) -> Tree -> Tree -> Tree L :: Typeable a => a -> Tree f :: Typeable a => a -> Tree -> Tree fx (L a) | show (typeOf x) == show (typeOf a) = L x | otherwise = L a 

you lose type information in your Tree , but it is typechecks and is complete

another version that stores type information

 data Tree abc where N :: (O abc) -> Tree abc -> Tree abc -> Tree abc L :: Typeable a => a -> Tree abc f :: Typeable a => a -> Tree abc -> Tree abc fx (L a) | show (typeOf x) == show (typeOf a) = L x | otherwise = L a 

here you save type information for any possible value stored in L in the type Tree . This might work if you only need a few different types, but get cumbersome quickly.