haskell - 一类改变类型的替换

Question

设置

考虑一种在函数符号类型上参数化的术语类型node和变量类型var :

data Term node var
  = VarTerm !var
  | FunTerm !node !(Vector (Term node var))
  deriving (Eq, Ord, Show)

instance Functor (Term node) where
  fmap f (VarTerm var)  = VarTerm (f var)
  fmap f (FunTerm n cs) = FunTerm n (Vector.map (fmap f) cs)

instance Monad (Term node) where
  pure = VarTerm
  join (VarTerm term) = term
  join (FunTerm n cs) = FunTerm n (Vector.map join cs)

这是一个有用的类型，因为我们使用 Term node Var 对开放术语进行编码。 ,
与 Term node Void 的封闭条款，以及带有 Term node () 的上下文.

目标是在 Term 上定义一种替换类型。 s 中最愉快的
可能的方式。这是第一个刺:

newtype Substitution (node ∷ Type) (var ∷ Type)
  = Substitution { fromSubstitution ∷ Map var (Term node var) }
  deriving (Eq, Ord, Show)

现在让我们定义一些与 Substitution 相关的辅助值。 :

subst ∷ Substitution node var → Term node var → Term node var
subst s (VarTerm var)  = fromMaybe (MkVarTerm var)
                         (Map.lookup var (fromSubstitution s))
subst s (FunTerm n ts) = FunTerm n (Vector.map (subst s) ts)

identity ∷ Substitution node var
identity = Substitution Map.empty

-- Laws:
--
-- 1. Unitality:
--    ∀ s ∷ Substitution n v → s ≡ (s ∘ identity) ≡ (identity ∘ s)
-- 2. Associativity:
--    ∀ a, b, c ∷ Substitution n v → ((a ∘ b) ∘ c) ≡ (a ∘ (b ∘ c))
-- 3. Monoid action:
--    ∀ x, y ∷ Substitution n v → subst (y ∘ x) ≡ (subst y . subst x)
(∘) ∷ (Ord var)
    ⇒ Substitution node var
    → Substitution node var
    → Substitution node var
s1 ∘ s2 = Substitution
          (Map.unionWith
           (λ _ _ → error "this should never happen")
           (Map.map (subst s1) (fromSubstitution s2))
           ((fromSubstitution s1) `Map.difference` (fromSubstitution s2)))

显然， (Substitution n v, ∘, identity)是一个幺半群(忽略 Ord对 ∘ 的约束) 和 (Term n v, subst)是一个幺半群 Action Substitution n v .

现在假设我们想让这个方案编码替换
改变变量类型。这看起来像某种类型 SubstCat满足以下模块签名:

data SubstCat (node ∷ Type) (domainVar ∷ Type) (codomainVar ∷ Type)
  = … ∷ Type

subst ∷ SubstCat node dom cod → Term node dom → Term node cod

identity ∷ SubstCat node var var

(∘) ∷ (Ord v1, Ord v2, Ord v3)
    → SubstCat node v2 v3
    → SubstCat node v1 v2
    → SubstCat node v1 v3

这几乎是一个 Haskell Category , 但对于 Ord对 ∘ 的限制.
你可能会认为如果 (Substitution n v, ∘, identity)之前是一个幺半群，
和 subst之前是一个幺半群 Action ，然后是 subst现在应该是一个类别
Action ，但实际上类别 Action 只是仿函数(在这种情况下，
从 Hask 的子类别到 Hask 的另一个子类别的仿函数)。

现在，我们希望 SubstCat 的某些属性是正确的。 :

SubstCat node var Void应该是地面换人的类型。

SubstCat Void var var应该是扁平换人的类型。

instance (Eq node, Eq dom, Eq cod) ⇒ Eq (SubstCat node dom cod)应该存在(以及 Ord 和 Show 的类似实例)。

应该可以计算域变量集，图像项
集和引入的变量集，给定 SubstCat node dom cod .

我所描述的操作应该是快速/节省空间的
作为Substitution 中的等价物上面的实现。

最简单的写法 SubstCat将是简单的
概括 Substitution :

newtype SubstCat (node ∷ Type) (dom ∷ Type) (cod ∷ Type)
  = SubstCat { fromSubstCat ∷ Map dom (Term node cod) }
  deriving (Eq, Ord, Show)

不幸的是，这不起作用，因为当我们运行 subst它可能是
如果我们正在运行替换的术语包含的变量是
不在 Map 的域中.我们可以在 Substitution 中解决这个问题
自从 dom ~ cod , 但在 SubstCat我们没有办法处理这些
变量。

我的下一个尝试是通过包含一个函数来处理这个问题
类型 dom → cod :

data SubstCat (node ∷ Type) (dom ∷ Type) (cod ∷ Type)
  = SubstCat
    !(Map dom (Term node cod))
    !(dom → cod)

然而，这会导致一些问题。首先，由于 SubstCat现在包含一个
函数，它不能再有 Eq , Ord , 或 Show实例。我们不可以
只需忽略 dom → cod比较相等时的字段，因为
替换的语义根据其值而变化。其次，现在
不再是 SubstCat node var Void代表一种地面
换人；事实上， SubstCat node var Void无人居住!

Érdi Gergő 在 Facebook 上建议我使用以下定义:

newtype SubstCat (node ∷ Type) (dom ∷ Type) (cod ∷ Type)
  = SubstCat (dom → Term node cod)

这无疑是一个迷人的前景。有一个明显的类别
类型: Monad 给出的 Kleisli 类别 Term node 上的实例.我是
不确定这是否真的对应于通常的替换概念
然而组成。不幸的是，这种表示不能有实例
对于 Eq等。我怀疑这在实践中可能效率很低，因为
在最好的情况下，它最终会成为一座高度封闭的塔 Θ(n) ,
在哪里 n是插入次数。它也不允许计算
域变量集。

问题
SubstCat 有一个合理的类型吗？符合我的要求吗？你能证明
那个不存在？如果我放弃拥有 Eq 的正确实例, Ord ,
和 Show ， 可能吗？

Answer 1

There is an obvious category for this type: the Kleisli category given by the Monad instance on Term node. I am not sure if this actually corresponds to the usual notion of substitution composition, however.

它确实与此相对应，并且它是对范围广泛的术语的并行替换的全面正确定义。你可能会注意到这个替换是完全的；如果您希望完全替换术语，这是一个要求，即。 e.它是从替换类别( Subst )到 的仿函数设置 .对于为什么部分替换不起作用的简单示例，如果您有一个空的 SubstCat node () Void ，那么您在点击 VarTerm () 时将不得不发明任意封闭术语在 subst - 如果您选择 Void，甚至不存在封闭术语对于 node .

因此，如果您有 Map dom (Term node cod)那么你有部分术语替换，i。 e.来自 的仿函数代理 Maybe 的 Kleisli 类别(暂时忽略 Ord 约束的正式复杂性):

type Subst node i j = Map i (Term node j)

subst :: Ord i => Subst node i j -> Term node i -> Maybe (Term node j)
subst sub (VarTerm x)    = Map.lookup x sub
subst sub (FunTerm f ts) = FunTerm f <$> traverse (subst sub) ts

现在，总术语替换以及您的 1-5 需求为 SubstCat是可能的，但在 SubstCat 的当前类型中不行和 Term .正如我所提到的，在这种情况下，替换必须是全部的，但目前我们只能有 SubstCat node dom cod有一些无限的 dom ，这使得替换的相等性不可判定。

所以让我们切换到更精确的形式化，它只包含我们在这里关心的内容。我们有范围很广的无类型术语，我们假设术语是有限的并且存在于有限变量上下文中。

无类型术语意味着只有变量上下文的大小很重要。所以， 代理 有自然数作为对象:

data Nat = Z | S Nat deriving (Eq, Show)

术语由 n :: Nat 编制索引, 包含 n变量的可能值:

-- {-# language TypeInType, GADTs, TypeFamilies, ScopedTypeVariables,
--           FlexibleInstances, MultiParamTypeClasses, RankNTypes,
--           TypeApplications, StandaloneDeriving #-}

data Fin n where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)
deriving instance Eq (Fin n)
deriving instance Ord (Fin n)
deriving instance Show (Fin n)

data Term node (n :: Nat) where
  VarTerm :: !(Fin n) -> Term node n
  FunTerm :: !node -> !(Vector (Term node n)) -> Term node n

deriving instance Eq node => Eq (Term node n)
deriving instance Ord node => Ord (Term node n)
deriving instance Show node => Show (Term node n)

替换(态射)是项的向量:

data Vec a n where
  Nil  :: Vec a Z
  (:>) :: a -> Vec a n -> Vec a (S n)
infixr 5 :>

deriving instance Eq a => Eq (Vec a n)
deriving instance Ord a => Ord (Vec a n)
deriving instance Show a => Show (Vec a n)

type Subst node i j = Vec (Term node j) i

术语替换如下:

subst :: Subst node i j -> Term node i -> Term node j
subst (t :> _ ) (VarTerm FZ)     = t
subst (_ :> ts) (VarTerm (FS x)) = subst ts (VarTerm x)
subst sub       (FunTerm f ts)   = FunTerm f (Vector.map (subst sub) ts)

组合只是逐点 subst :

comp :: Subst node i j -> Subst node j k -> Subst node i k
comp Nil       sub2 = Nil
comp (t :> ts) sub2 = subst sub2 t :> comp ts sub2

身份替换并不是那么容易。我们需要在类型级别上调度 Nat .为此，我们在这里使用一个类型类； singletons 将是一个更重但更有原则的解决方案。实现本身也有点令人费解。它利用了 Subst node n m与 (Fin n -> Term node m) 同构.事实上，我们可以一直使用函数表示，但是之后 Eq, Ord and Show实例仍然有效地需要向后转换，并且我们不会有(严格)向量的时空有界保证。

class Tabulate n where
  tabulate :: (Fin n -> Term node m) -> Subst node n m

instance Tabulate Z where
  tabulate f = Nil

instance Tabulate n => Tabulate (S n) where
  tabulate f = f FZ :> tabulate (f . FS)

idSubst :: Tabulate n => Subst node n n
idSubst = tabulate VarTerm

而已! Subst 的类别法则证明 subst 的仿函数定律留作练习。

PS:我注意到在文献和正式的 Agda/Coq 开发中， Nat Subst 的索引通常按交换顺序排列， subst有逆变作用。