Категория подстановочных замен

Настройка

Рассмотрим тип терминов, параметризованных по типу 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 nv, ∘, identity) является моноидом (игнорируя ограничение Ord на ∘) и (Term nv, subst) является моноидным действием Substitution nv.

Теперь предположим, что мы хотим сделать эту схему закодировать замены, которые изменяют тип переменной. Это будет выглядеть как некоторый тип 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

Это почти Category Haskell, но для ограничений Ord на ∘. Вы можете подумать, что если (Substitution nv, ∘, identity) раньше была моноидом, а subst был моноидным действием раньше, то subst теперь должен быть действием категории, но, по сути, действия категории - это просто функторы (в этом случае, функтор из подкатегории Хаска в другую подкатегорию Хаска).

Теперь есть некоторые свойства, которые, как мы надеемся, будут иметь отношение к 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. Должно быть возможным вычислить набор переменных домена, заданный набор изображений и введенный набор переменных, заданный 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 является необитаемым!

Érdi Gergő предложил в Facebook, что я использую следующее определение:

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

Это, безусловно, захватывающая перспектива. Для этого типа существует очевидная категория: категория Kleisli, заданная экземпляром Monad на Term node. Однако я не уверен, что это действительно соответствует обычному понятию подстановки. К сожалению, это представление не может иметь экземпляров для Eq et al. и я подозреваю, что на практике это может быть очень неэффективным, так как в лучшем случае это будет башня затворов высоты Θ(n), где n - количество вставок. Он также не позволяет вычислять набор переменных домена.

Вопрос

Есть ли разумный тип для SubstCat который соответствует моим требованиям? Можете ли вы доказать, что этого не существует? Если я откажусь от правильных экземпляров Eq, Ord и Show, возможно ли это?

Ответы

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

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

-- {-# 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)

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

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

{-# 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