使用延迟模态从固定点运算符计算（无限）树

Question

这是一个涉及循环绑定和无限数据结构的函数式编程难题。有点背景，稍等一下。

设置。让我们定义一个表示递归数据类型的数据类型：

type Var = String
data STerm = SMu Var STerm
           | SVar Var
           | SArrow STerm STerm
           | SBottom
           | STop
   deriving (Show)

即t ::= μα. t | α | t → t | ⊥ | ⊤。请注意，⊥ 表示没有居民的类型，而 ⊤ 表示有所有居民的类型。请注意 (μα. α) = ⊥，因为 μ 是最小定点运算符。

我们可以将递归数据类型解释为无限树，从 μα. t 到 t[α ↦ μα. t] 的重复展开而产生。（有关此过程的正式描述，请参阅http://lucacardelli.name/Papers/SRT.pdf）在Haskell中，我们可以定义一种惰性树，它没有μ-binders或变量：

data LTerm = LArrow LTerm LTerm
           | LBottom
           | LTop
   deriving (Show)

并且，在普通的Haskell中，一个从一个到另一个的转换函数：

convL :: [(Var, LTerm)] -> STerm -> LTerm
convL _ STop    = LTop
convL _ SBottom = LBottom
convL ctx (SArrow t1 t2) = LArrow (convL ctx t1) (convL ctx t2)
convL ctx (SVar v)
    | Just l <- lookup v ctx = l
    | otherwise = error "unbound variable"
convL ctx (SMu v t) = fix (\r -> convL ((v, r) : ctx) t)

但是，这个函数有一个问题：它没有生产力。如果你运行 convL [] (SMu "x" (SVar "x")) 你会死循环。在这种情况下，我们宁愿得到 LBottom。一个有趣的练习是直接修复此功能，使其具有生产力；但是，在这个问题中，我想以不同的方式解决问题。

延迟模态的生产力。 当我们构建上述循环数据结构时，我们需要确保在构建它们之前不使用我们的计算结果。延迟模式是一种确保我们编写高效（非无限循环）程序的方法。基本思路很简单：如果类型 Int 意味着我今天有一个整数，我定义一个类型构造函数 D，这样 D Int 就意味着我有一个类型 Int 明天。 D 是一个 Functor 和一个 Applicative（但不是 monad。）

-- D is abstract; you are not allowed to pattern match on it
newtype D a = D a
   deriving (Show)

instance Functor D where
    fmap f (D a) = D (f a)

instance Applicative D where
    D f <*> D a = D (f a)
    pure x = D x

用D，我们定义了一个定点运算符：它说要构造一个a的值，你可以访问你正在构造的a，只要你只用明天.

fixD :: (D a -> a) -> a
fixD f = f (D (fixD f))

例如，一个 Stream 包含我今天拥有的值 a 和我明天必须生成的一个流 Stream a。

data Stream a = Cons a (D (Stream a))

使用 fixD，我可以在流上定义一个 map 函数，保证高效，因为对 [=35= 的递归调用] 只用于产生明天需要的值。

instance Functor Stream where
    fmap f = fixD $ \go (Cons x xs) -> Cons (f x) (go <*> xs)

问题所在。这是 LTerm 的变体，具有显式延迟模式。

data Term = Arrow (D Term) (D Term)
          | Bottom
          | Top
    deriving (Show)

使用fixD（不允许非结构递归引用），如何编写函数conv :: STerm -> Term（或conv :: STerm -> D Term）？一个特别有趣的测试用例是SMu "x" (SArrow STop (SMu "y" (SVar "x")))；结果结构中不应有底部！

Update. 我不小心排除了 STerm 上的结构递归，这不是问题的意图；我已改写以删除该限制。

Answer 1

我的直觉是上下文应该只包含延迟项。这样，conv ctx (SMu "x" t) 将等同于 fixD (\d -> conv ((x,r):ctx) t)，就像原来的 convL.

如果是这种情况，那么您需要一种通用方法来在数据结构中包含延迟项，而不是只允许它们出现在箭头中：

data Term = Arrow Term Term
          | Bottom
          | Top
          | Next (D Term)

第一次尝试 conv 给我们：

conv :: [(Var, D Term)] -> STerm -> Term
conv _ STop = Top
conv _ SBottom = SBottom
conv ctx (SArrow t1 t2) = Arrow (conv ctx t1) (conv ctx t2)
conv ctx (SVar v)
  | Just l <- lookup v ctx = Next l
  | otherwise = error "unbound variable"
conv ctx (SMu v t) = fixD (\r -> conv ((x,r):ctx) t)

但是，这使用了对 conv 的无保护递归调用。如果你想避免这种情况，你可以将所有 fixD 递归调用包装在 Next.

中

conv :: [(Var, D Term)] -> STerm -> Term
conv = fixD step where
        step _ _ STop = Top
        step _ _ SBottom = Bottom
        step d ctx (SArrow t1 t2) = Arrow (Next $ d <*> pure ctx <*> pure t1) 
                                          (Next $ d <*> pure ctx <*> pure t2)
        step d ctx (SVar v)
          | Just l <- lookup v ctx = Next l
          | otherwise = error "unbound variable"
        step d ctx (SMu v t) = fixD (\r -> 
                                    Next $ d <*> pure ((x,r):ctx) <*> pure t)

我不确定这是否正是您要找的，因为 conv [] SMu "x" (SArrow SBottom (SMu "y" (SVar "x"))) 在生成的结构中仍然有底部。你想出门的类型是什么？

Answer 2

您打算在 convL 的 SMu 情况下仅禁止无限制递归 (fix)，还是在 SArrow 情况下禁止结构递归？

我不认为这在 STerm 上没有结构递归的解决方案，因为即使在无限 STerm 上我们也必须高效，例如：

foldr (\n -> SMu ("x" ++ show n)) undefined [0..]  -- μα. μβ. μγ. μδ. …

要通过 STerm 上的结构递归来做到这一点，似乎诀窍是将 Either Term (D Term) 存储在上下文中。当我们通过一个Arrow并产生一个D时，我们可以将所有的Right转换为Left。

type Ctx = [(Var, Either Term (D Term))]

dCtx :: Ctx -> D Ctx
dCtx = traverse (traverse (fmap Left . either pure id))

conv :: STerm -> Ctx -> Term
conv STop _ = Top
conv SBottom _ = Bottom
conv (SArrow t1 t2) ctx = Arrow (fmap (conv t1) (dCtx ctx)) (fmap (conv t2) (dCtx ctx))
conv (SVar v) ctx = case lookup v ctx of
                      Nothing -> error "unbound variable"
                      Just (Left t) -> t
                      Just (Right _) -> Bottom
conv (SMu v t) ctx = fixD (\dr -> conv t ((v, Right dr) : ctx))

使用延迟模态从固定点运算符计算（无限）树

Compute an (infinite) tree from fixpoint operator using delay modality

haskell

infinite

coinduction