haskell – 在GADT中递归替换

2023年5月5日 258次阅读

说我有以下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

现在我想构造一个函数来替换Tree中类型a的所有L(eave),如下所示：

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 – >在类中输入.

最佳答案 我不认为这对当前的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

你丢失了树中的类型信息,但是这个类型是完全的

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

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中的任何可能值的类型信息.如果您只需要几种不同的类型,这可能会有效,但会很快变得笨重.

点赞