一类改变类型的替换

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)是一个幺半群的行为 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)之前是monoid,并且之前subst是monoid动作,那么subst现在应该是一个类别动作,但实际上类别动作只是仿函数(在这种情况下,从Hask的子类别到另一个子类别的仿函数) Hask).

现在有一些我们希望真实的属性SubstCat:

1. SubstCat node var Void 应该是地面替代的类型.
2. SubstCat Void var var 应该是扁平替换的类型.
3. instance (Eq node, Eq dom, Eq cod) ? Eq (SubstCat node dom cod) 应该存在(以及类似的实例Ord和Show).
4. 给定a,应该可以计算域变量集,图像项集和引入的变量集SubstCat node dom cod.
5. 我所描述的操作应该与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是无人居住的!

ÉrdiGergő在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

这种类型有一个明显的类别:由Term节点上的Monad实例给出的Kleisli类别.但是,我不确定这是否与通常的替代成分概念相对应.

它确实对应于它,并且它是对范围广泛的术语的并行替换的全面正确定义.您可能会注意到这种替换是完全的 ; 这是一个要求,如果你想要术语替换是总的,即它是一个从替换类别(Subst)到Set的仿函数.对于为什么部分替代不起作用一个简单的例子,如果你有一个空的SubstCat node () Void,那么你就必须打时创造任意封闭条件VarTerm ()的subst-和关闭而言,如果你选择根本不存在Void的node.

因此,如果你有Map dom (Term node cod),那么你有部分长期替代,即从仿函数SUBST到Kleisli类别Maybe(不考虑现在正式并发症的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个desiderata SubstCat是可能的,但不是当前的种类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.为此,我们在这里使用一个类型类; 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 Data.MemoTrie
import Control.Category.Constrained

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-特里结构类型:->:基本上是一个地图类型,但映射总是总.即,它们是正确的函数,但在内存固定的表示中 - 不需要闭包.这仅适用于不仅可订购而且完全可枚举的类型,这是HasTrie类所表达的类型; 因此我们无法定义实例,Control.Category.Category但我们可以为其可约束的链接定义一个实例.