4

假设我有以下 GADT AST：

data O a b c where 
    Add ::  O a a a
    Eq :: O a b Bool
    --... more operations

data Tree a where 
    N :: (O a b c) -> Tree a -> Tree b -> Tree c
    L :: a -> Tree a

现在我想构造一个函数来替换树中所有L类型的（屋檐） ，如下所示：a

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

有可能构建这样的功能吗？（可能使用类？）如果对 GADT 进行更改，是否可以完成？

我已经有一个 typeof 函数：typeof :: a -> Type在一个类中。

4

2 回答 2

2

我认为当前的 GADT 不可能做到这一点，除非您可以接受部分定义的功能。你可以写

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

但你不能使这个功能完全，因为你需要

   | otherwise = L a

这不会进行类型检查，因为您刚刚证明L a :: Tree a并且L x :: Tree x是不同的类型。

但是，如果您将 定义GADT为存在量化

data Tree where
    N :: (O a b c) -> Tree -> Tree -> Tree
    L :: Typeable a => a -> Tree

f :: Typeable a => a -> Tree -> Tree
f x (L a)
    | show (typeOf x) == show (typeOf a) = L x
    | otherwise = L a

你丢失了你的类型信息Tree，但是这个类型检查并且是总的

另一个保留类型信息的版本

data Tree a b c where
    N :: (O a b c) -> Tree a b c -> Tree a b c -> Tree a b c
    L :: Typeable a => a -> Tree a b c

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

L在这里，您保留类型中存储在 a中的任何可能值的类型信息Tree。如果您只需要几种不同的类型，这可能会起作用，但会很快变得笨重。

于 2013-03-13T23:41:35.790 回答
0

诀窍是使用类型见证：http ://www.haskell.org/haskellwiki/Type_witness

data O a b c where 
    Add ::  O a a a
    Eq :: O a b Bool

instance Show (O a b c) where
    show Add = "Add"
    show Eq = "Eq"

data Tree a where 
    T :: (Typeable a, Typeable b, Typeable c) => (O a b c) -> Tree a -> Tree b -> Tree c
    L :: a -> Tree a

instance (Show a) => Show (Tree a) where
    show (T o a b) = "(" ++ (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 a b = case dynamicCast (witness a) (witness b) a of
    Just v  -> v
    Nothing -> b

f :: (Typeable a, Typeable b) => b -> Tree a -> Tree a
f x (L a) = L $ replace x a
f x (T o a b) = T o (f x a) (f x b)
于 2013-03-14T15:16:18.943 回答