4

次のGADTASTがあるとします。

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ここでは、タイプに格納されている可能な値のタイプ情報を保持します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 に答える