haskell - Una categoría de sustituciones de cambio de tipo.

programming-languages agda

Question

La puesta en marcha

Considere un tipo de términos parametrizados sobre un tipo de node símbolos de función y un tipo de variables 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)

Este es un tipo útil, ya que codificamos los términos abiertos con el Term node Var , los términos cerrados con el Term node Void y los contextos con el Term node () .

El objetivo es definir un tipo de sustituciones en los Term de la manera más agradable posible. Aquí hay una primera puñalada:

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

Ahora definamos algunos valores auxiliares relacionados con la 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)))

Claramente, (Substitution nv, ∘, identity) es un monoide (ignorando la restricción Ord en ∘ ) y (Term nv, subst) es una acción monoide de Substitution nv .

Ahora supongamos que queremos que este esquema codifique sustituciones que cambien el tipo de variable . Esto se vería como un tipo de SubstCat que satisface la firma del módulo a continuación:

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

Esto es casi una Category Haskell, pero para las restricciones de Ord en. Podría pensar que si (Substitution nv, ∘, identity) era un monoide antes, y subst era una acción monoide antes, entonces subst debería ser ahora una acción de categoría, pero en realidad las acciones de categoría son solo funciones (en este caso, un functor de una subcategoría de Hask a otra subcategoría de Hask).

Ahora hay algunas propiedades que esperamos sean ciertas acerca de SubstCat :

1. SubstCat node var Void debe ser el tipo de sustituciones de suelo.
2. SubstCat Void var var debe ser el tipo de sustituciones planas.
3. instance (Eq node, Eq dom, Eq cod) ⇒ Eq (SubstCat node dom cod) debe existir (así como instancias similares para Ord y Show ).
4. Debería ser posible calcular el conjunto de variables de dominio, el conjunto de términos de imagen y el conjunto de variables introducidas, dado un SubstCat node dom cod .
5. Las operaciones que he descrito deben ser tan rápidas y eficientes en el espacio como sus equivalentes en la implementación de Substitution anterior.

El enfoque más simple posible para escribir SubstCat sería simplemente generalizar la Substitution :

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

Desafortunadamente, esto no funciona porque cuando ejecutamos subst puede darse el caso de que el término en el que estamos ejecutando la sustitución contenga variables que no están en el dominio del Map . Podríamos SubstCat en Substitution desde dom ~ cod , pero en SubstCat no tenemos manera de lidiar con estas variables.

Mi siguiente intento fue tratar este problema incluyendo también una función de tipo dom → cod :

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

Esto causa algunos problemas, sin embargo. En primer lugar, como SubstCat ahora contiene una función, ya no puede tener instancias Eq , Ord o Show . No podemos simplemente ignorar el campo dom → cod cuando se compara la igualdad, ya que la semántica de sustitución cambia dependiendo de su valor. En segundo lugar, ahora ya no es el caso de que SubstCat node var Void representa un tipo de sustituciones de tierra; de hecho, SubstCat node var Void está deshabitado !

Érdi Gergő sugirió en Facebook que utilizara la siguiente definición:

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

Esta es ciertamente una perspectiva fascinante. Hay una categoría obvia para este tipo: la categoría de Kleisli dada por la instancia de Monad en el Term node . Sin embargo, no estoy seguro de si esto corresponde realmente a la noción habitual de composición de sustitución. Desafortunadamente, esta representación no puede tener instancias para Eq et al. y sospecho que podría ser muy ineficiente en la práctica, ya que en el mejor de los casos terminará siendo una torre de cierres de altura Θ(n) , donde n es el número de inserciones. Tampoco permite el cálculo del conjunto de variables de dominio.

La pregunta

¿Existe un tipo sensible para SubstCat que se ajuste a mis requisitos? ¿Puedes probar que uno no existe? Si renuncio a tener instancias correctas de Eq , Ord y Show , ¿es posible?

Answer 1

Hay una categoría obvia para este tipo: la categoría de Kleisli dada por la instancia de Monad en el nodo Término. Sin embargo, no estoy seguro de si esto corresponde realmente a la noción habitual de composición de sustitución.

Corresponde a eso, y es una definición completa y completa de la sustitución paralela para términos bien definidos. Puede notar que esta sustitución es total ; este es un requisito si desea que la sustitución de términos sea total, es decir, que sea un functor de la categoría de sustituciones ( Subst ) a Set . Para un ejemplo simple de por qué las sustituciones parciales no funcionan, si tiene un SubstCat node () Void vacío SubstCat node () Void , entonces tendría que inventar términos cerrados arbitrarios cuando se golpea VarTerm () en los términos subst y cerrados ni siquiera existen si Void eliges Void para el node .

Por lo tanto, si tiene Map dom (Term node cod) entonces tiene una sustitución parcial del término, es decir, un funtor de Subst a la categoría Kleisli para Maybe (sin tener en cuenta las complicaciones formales de las restricciones 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

Ahora, la sustitución total del término junto con su 1 a 1 desiderata para SubstCat es posible, pero no con las clases actuales para SubstCat y Term . Como mencioné, en este caso, las sustituciones deben ser totales, pero en la actualidad solo podemos tener un SubstCat node dom cod con algún SubstCat node dom cod infinito, lo que hace que la igualdad de sustituciones sea indecidible.

Así que cambiemos a una formalización más precisa, que contiene solo lo que nos importa aquí. Tenemos términos no tipificados bien definidos, y asumimos que los términos son finitos y viven en contextos de variables finitas.

Los términos no tipificados implican que solo importan los tamaños de contextos variables. Entonces, Subst tiene números naturales como objetos:

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

Los términos están indexados por n :: Nat , que contienen n valores posibles para las variables:

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

Las sustituciones (morfismos) son vectores de términos:

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

La sustitución de términos es la siguiente:

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)

La composición es solo subst substancial:

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

La sustitución de identidad no es tan fácil. Tenemos que enviar a nivel de tipo Nat . Para esto, usamos aquí una clase de tipo; singletons serían una solución más pesada pero con más principios. La implementación en sí también es un poco alucinante. Hace uso del hecho de que Subst node nm es isomorfo a (Fin n -> Term node m) . De hecho, podríamos usar la representación funcional todo el tiempo, pero luego las instancias Eq, Ord and Show seguirían necesitando la conversión hacia atrás y no tendríamos las garantías de límite de espacio-tiempo de los vectores (estrictos).

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

¡Eso es! Las pruebas de las leyes de categoría para las leyes de Subst y funtor para subst se dejan como ejercicio.

PD: Observo que en la literatura y en los desarrollos formales de Agda / Coq, los índices Nat de Subst generalmente están en orden de intercambio, y la acción contravariante es sustancial .

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

El tipo memo-trie :->: es básicamente un tipo de mapa, pero los mapas son siempre totales. Es decir, son funciones propias, pero en una representación de memoria fija, no se necesitan cierres. Esto solo funciona para los tipos que no solo son ordenables sino que también son completamente enumerables, que es lo que expresa la clase HasTrie ; por lo tanto, no podemos definir una instancia para Control.Category.Category pero podemos definir una instancia para su pendiente pendiente .