一类改变类型的替换

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 上定义一种替换类型可能的方式。这是第一次尝试：

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) 上的约束是 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 之前是一个幺半群动作，那么 subst 现在应该是一个类别动作，但事实上类别动作只是函子（在这种情况下，从 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.
我描述的操作应该是 fast/space-efficient 作为上面 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)

这无疑是一个迷人的前景。有一个明显的类别类型：Term node 上的 Monad 实例给出的 Kleisli 类别。我是不确定这是否真的符合通常的替代概念组成，但是。不幸的是，这种表示不能有实例 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) 到 Set 的函子。举一个为什么部分替换不起作用的简单示例，如果您有一个空的 SubstCat node () Void，那么在 subst 中点击 VarTerm () 时您将不得不发明任意封闭项 - 和封闭项如果您为 node 选择 Void，则甚至不存在。

因此，如果你有 Map dom (Term node cod) 那么你有部分术语替换，即。 e.从 Subst 到 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

现在，可以用 SubstCat 的 1-5 个期望项进行总词替换，但不能用 SubstCat 和 Term 的当前类型替换。正如我提到的，在这种情况下，替换必须是全部的，但目前我们可以只使用 SubstCat node dom cod 和一些无限的 dom，这使得替换的相等性不可判定。

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

非类型化术语意味着只有变量上下文的大小才重要。所以，Subst 有自然数作为对象：

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 上进行调度。为此，我们在这里使用类型class； 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 有逆变动作。

Answer 2

{-# LANGUAGE TypeFamilies, TypeOperators #-}

import <a href="http://hackage.haskell.org/package/MemoTrie-0.6.9/docs/Data-MemoTrie.html" rel="noreferrer">Data.MemoTrie</a>
import <a href="http://hackage.haskell.org/package/constrained-categories-0.3.1.0/docs/Control-Category-Constrained.html" rel="noreferrer">Control.Category.Constrained</a>

newtype SubstCat node dom cod = SubstCat (dom :->: Term node cod)

instance Category (SubstCat node) where
  type Object (SubstCat node) a = HasTrie a
  id = SubstCat (trie VarTerm)
  SubstCat f . SubstCat g = SubstCat $ fmap (untrie f =<<) g

memo-trie type :->: is basically a map type, but the mappings are always total. I.e., they are proper functions, but in a memory-fixed representation – no closures needed. This only works for types that are not only orderable but also completely enumeratable, which is what the HasTrie class expresses; thus we can't define an instance for Control.Category.Category but we can define an instance for its constrainable pendant.

一类改变类型的替换

A category of type-changing substitutions

haskell

programming-languages

agda

type-theory

设置

问题