¿Cuál es el equivalente lógico combinatorio de la teoría de tipos intuicionista?

Así que pensé un poco más en ello e hice algunos progresos. He aquí un primer intento de codificar el deliciosamente simple (pero inconsistente) Set : Set sistema de Martin-Löf en un estilo combinatorio. No es una buena manera de terminar, pero es el lugar más fácil para empezar. La sintaxis de esta teoría de tipos es simplemente lambda-cálculo con anotaciones de tipo, Pi-tipos, y un Conjunto de universo.

La Teoría del Tipo Objetivo

Para completar el bien, voy a presentar las reglas. La validez de contexto solo te dice puede construir contextos a partir de vacíos al anexar variables frescas que habitan Set s.

                     G |- valid   G |- S : Set
--------------     ----------------------------- x fresh for G
  . |- valid         G, x:S |- valid

Y ahora podemos decir cómo sintetizar tipos para términos en cualquier contexto dado, y cómo cambiar el tipo de algo hasta el comportamiento computacional de los términos que contiene.

  G |- valid             G |- S : Set   G |- T : Pi S \ x:S -> Set
------------------     ---------------------------------------------
  G |- Set : Set         G |- Pi S T : Set

  G |- S : Set   G, x:S |- t : T x         G |- f : Pi S T   G |- s : S
------------------------------------     --------------------------------
  G |- \ x:S -> t : Pi S T                 G |- f s : T s

  G |- valid                  G |- s : S   G |- T : Set
-------------- x:S in G     ----------------------------- S ={beta} T
  G |- x : S                  G |- s : T

En una pequeña variación del original, he hecho lambda el único operador de enlace, por lo que el segundo argumento de Pi debe ser una función que calcula la forma en que el tipo de retorno depende de la entrada. Por convención (por ejemplo, en Agda, pero lamentablemente no en Haskell), el alcance de lambda se extiende hacia la derecha en la medida de lo posible, por lo que a menudo puede dejar abstracciones sin envolver cuando son el último argumento de un operador de orden superior: se puede ver que hice eso con Pi. Su tipo Agda (x : S) -> T se convierte en Pi S \ x:S -> T.

(Digresión. Las anotaciones de tipo en lambda son necesarias si desea ser capaz de sintetizar el tipo de abstracciones. Si cambia a escribir marcando como su modus operandi, usted todavía necesita anotaciones para comprobar un beta-redex como (\ x -> t) s, ya que no tiene forma de adivinar los tipos de las partes de la del todo. Aconsejo a los diseñadores modernos que comprueben los tipos y excluyan los redexes beta de la sintaxis misma.)

(Digresión. Este sistema es inconsistente ya que Set:Set permite la codificación de una variedad de "paradojas mentirosas". Cuando Martin-Löf propuso esta teoría, Girard le envió una codificación de la misma en su propio Sistema inconsistente U. La paradoja posterior debida a Hurkens es la construcción tóxica más limpia que conocemos.)

Sintaxis Combinadora y Normalización

De todos modos, tenemos dos símbolos adicionales, Pi y Set, por lo que tal vez podríamos manejar una traducción combinatoria con S, K y dos símbolos adicionales: Elegí U para el universo y P para el producto.

Ahora podemos definir la sintaxis combinatoria sin tipo (con variables libres):

data SKUP = S | K | U | P deriving (Show, Eq)

data Unty a
  = C SKUP
  | Unty a :. Unty a
  | V a
  deriving (Functor, Eq)
infixl 4 :.

Tenga en cuenta que he incluido los medios para incluir variables libres representadas por el tipo a en esta sintaxis. Aparte de ser un reflejo de mi parte (toda sintaxis digna de este nombre es una mónada libre con return variables de embedding y >>= sustitución de perfoming), será útil representar etapas intermedias en el proceso de conversión de términos con enlace a su forma combinatoria.

Aquí está la normalización: {[59]]}

norm :: Unty a -> Unty a
norm (f :. a)  = norm f $. a
norm c         = c

($.) :: Unty a -> Unty a -> Unty a        -- requires first arg in normal form
C S :. f :. a $. g  = f $. g $. (a :. g)  -- S f a g = f g (a g)   share environment
C K :. a $. g       = a                   -- K a g = a             drop environment
n $. g              = n :. norm g         -- guarantees output in normal form
infixl 4 $.

(Un ejercicio para el lector es definir un tipo para exactamente las formas normales y afilar los tipos de estas operaciones.)

Que representa el tipo Teoría

Ahora podemos definir una sintaxis para nuestra teoría de tipos.

data Tm a
  = Var a
  | Lam (Tm a) (Tm (Su a))    -- Lam is the only place where binding happens
  | Tm a :$ Tm a
  | Pi (Tm a) (Tm a)          -- the second arg of Pi is a function computing a Set
  | Set
  deriving (Show, Functor)
infixl 4 :$

data Ze
magic :: Ze -> a
magic x = x `seq` error "Tragic!"

data Su a = Ze | Su a deriving (Show, Functor, Eq)

Utilizo una representación de índice de Bruijn en la forma de Bellegarde y Hook (popularizada por Bird y Paterson). El tipo Su a tiene un elemento más que a, y lo usamos como el tipo de variables libres bajo un aglutinante, con Ze como la variable recién enlazada y Su x siendo la representación desplazada de la antigua variable libre x.

Traduciendo Términos a Combinadores

Y con hecho esto, adquirimos la traducción habitual, basada enabstracción de corchetes .

tm :: Tm a -> Unty a
tm (Var a)    = V a
tm (Lam _ b)  = bra (tm b)
tm (f :$ a)   = tm f :. tm a
tm (Pi a b)   = C P :. tm a :. tm b
tm Set        = C U

bra :: Unty (Su a) -> Unty a               -- binds a variable, building a function
bra (V Ze)      = C S :. C K :. C K        -- the variable itself yields the identity
bra (V (Su x))  = C K :. V x               -- free variables become constants
bra (C c)       = C K :. C c               -- combinators become constant
bra (f :. a)    = C S :. bra f :. bra a    -- S is exactly lifted application

Escribiendo los Combinadores

La traducción muestra la forma en que usamos los combinadores, lo que nos da una pista sobre cuáles deberían ser sus tipos. U y P son solo constructores de conjuntos, por lo que, escribiendo tipos no traducidos y permitiendo la "notación Agda" para Pi, deberíamos tener

U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set

El combinador K se usa para elevar un valor de algún tipo A a una función constante sobre algún otro tipo G.

  G : Set   A : Set
-------------------------------
  K : (a : A) -> (g : G) -> A

El combinador S se usa para levantar aplicaciones sobre un tipo, del cual todas las partes pueden depender.

  G : Set
  A : (g : G) -> Set
  B : (g : G) -> (a : A g) -> Set
----------------------------------------------------
  S : (f : (g : G) ->    (a : A g) -> B g a   ) ->
      (a : (g : G) ->    A g                  ) ->
           (g : G) ->    B g (a g)

Si nos fijamos en el tipo de S, verá que establece exactamente la regla de aplicación contextualizada de la teoría de tipos, por lo que es lo que hace adecuado para reflejar la construcción de la aplicación. ¡Ese es su trabajo!

Entonces tenemos aplicación solo para cosas cerradas

  f : Pi A B
  a : A
--------------
  f a : B a

Pero hay un inconveniente. He escrito los tipos de combinadores en la teoría de tipos ordinaria, no en la teoría de tipos combinatoria. Afortunadamente, tengo una máquina que hará la traducción.

Un Sistema de Tipo Combinatorio

---------
  U : U

---------------------------------------------------------
  P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU)))

  G : U
  A : U
-----------------------------------------
  K : P[A](S(S(KP)(K[G]))(S(KK)(K[A])))

  G : U
  A : P[G](KU)
  B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU)))
--------------------------------------------------------------------------------------
  S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK))))
      (S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A])))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G]))))
      (S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))
      (S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))
      (S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK)))))))

  M : A   B : U
----------------- A ={norm} B
  M : B

Así que ahí lo tienes, en toda su gloria ilegible: ¡una presentación combinatoria de Set:Set!

Todavía hay un pequeño problema. La sintaxis del sistema no le da ninguna manera de adivinar el G, A y B parámetros para S y de manera similar para K, solo desde el plazo. Correspondientemente, podemos verificar escribiendo derivaciones algorítmicamente, pero no podemos simplemente typecheck combinator términos como podríamos con el sistema original. Lo que podría funcionar es requerir que la entrada al typechecker lleve anotaciones de tipo sobre los usos de S y K, registrando efectivamente la derivación. Pero esa es otra lata de gusanos...

Este es un buen lugar para parar, si has estado lo suficientemente interesado para comenzar. El resto es " detrás de escena" cosa.

Generando los Tipos de los Combinadores

Generé esos tipos combinatorios usando la traducción de abstracción de corchetes de los términos relevantes de la teoría de tipos. Para mostrar cómo lo hice, y hacer que este post no sea del todo inútil, permítanme ofrecer mi equipo.

Puedo escribir los tipos de los combinadores, totalmente abstraídos sobre sus parámetros, de la siguiente manera. Hago uso de mi práctica función pil, que combina Pi y lambda para evitar repetir el tipo de dominio, y bastante útil me permite utilizar el espacio de función de Haskell para unir variables. Tal vez casi se puede leer lo siguiente!

pTy :: Tm a
pTy = fmap magic $
  pil Set $ \ _A -> pil (pil _A $ \ _ -> Set) $ \ _B -> Set

kTy :: Tm a
kTy = fmap magic $
  pil Set $ \ _G -> pil Set $ \ _A -> pil _A $ \ a -> pil _G $ \ g -> _A

sTy :: Tm a
sTy = fmap magic $
  pil Set $ \ _G ->
  pil (pil _G $ \ g -> Set) $ \ _A ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ _ -> Set) $ \ _B ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ a -> _B :$ g :$ a) $ \ f ->
  pil (pil _G $ \ g -> _A :$ g) $ \ a ->
  pil _G $ \ g -> _B :$ g :$ (a :$ g)

Con estos definidos, extraje los correspondientes subtermos abiertos y los corrí a través de la traducción.

Un Kit de herramientas de codificación de Bruijn

He Aquí cómo construir pil. En primer lugar, defino una clase de Finconjuntos it, utilizados para las variables. Cada conjunto tiene un constructor-preservando emb edding en el conjunto anterior, más un nuevo top elemento, y puedes distinguirlos: la función embd te dice si un valor está en la imagen de emb.

class Fin x where
  top :: Su x
  emb :: x -> Su x
  embd :: Su x -> Maybe x

Podemos, por supuesto, instanciar Fin para Ze y Suc

instance Fin Ze where
  top = Ze              -- Ze is the only, so the highest
  emb = magic
  embd _ = Nothing      -- there was nothing to embed

instance Fin x => Fin (Su x) where
  top = Su top          -- the highest is one higher
  emb Ze     = Ze            -- emb preserves Ze
  emb (Su x) = Su (emb x)    -- and Su
  embd Ze      = Just Ze           -- Ze is definitely embedded
  embd (Su x)  = fmap Su (embd x)  -- otherwise, wait and see

Ahora puedo definir menos o iguales, con una operación debilitamiento.

class (Fin x, Fin y) => Le x y where
  wk :: x -> y

La función wk debe incrustar los elementos de x como los elementos mayores de y, de modo que las cosas adicionales en y son más pequeñas, y por lo tanto en términos de índice de Bruijn, local.

instance Fin y => Le Ze y where
  wk = magic    -- nothing to embed

instance Le x y => Le (Su x) (Su y) where
  wk x = case embd x of
    Nothing  -> top          -- top maps to top
    Just y   -> emb (wk y)   -- embedded gets weakened and embedded

Y una vez que tienes eso resuelto, un poco de skullduggery rango-n hace el resto.

lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
lam s f = Lam s (f (Var (wk (Ze :: Su x))))
pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
pil s f = Pi s (lam s f)

La función de orden superior no solo te da un término que representa la variable, te da una sobrecargada que se convierte en la representación correcta de la variable en cualquier ámbito donde la variable es visible. Es decir, el hecho de que me tome la molestia de distinguir los diferentes ámbitos por tipo le da al typechecker de Haskell suficiente información para calcular el desplazamiento requerido para la traducción a la representación de Bruijn. ¿Por qué tener un perro y ladrar?