J'ai donc réfléchi un peu plus et fait quelques progrès. Voici un premier coup de couteau à l'encodage de Martin-Löf est délicieusement simple (mais incompatible) Set : Set système dans une combinatoire de style. Ce n'est pas une bonne façon de terminer, mais c'est l'endroit le plus facile pour commencer. La syntaxe de ce type de théorie est juste lambda-calcul avec les annotations, les Pi-types, et un univers de Jeu.
Le Type De Cible De La Théorie
À des fins d'exhaustivité, je vais présenter les règles. Contexte validité juste dit que vous pouvez construire des contextes de vide en touchant des frais variables habiter Sets.
G |- valid G |- S : Set
-------------- ----------------------------- x fresh for G
. |- valid G, x:S |- valid
Et maintenant, nous pouvons dire comment faire pour synthétiser les types de termes dans un contexte donné, et comment changer le type de quelque chose, pour le calcul du comportement des termes qu'il contient.
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
Dans une petite variation de l'original, j'ai fait lambda la seule liaison de l'opérateur, de sorte que le deuxième argument de la Pi doit être une fonction de calcul de la façon dont le type de retour dépend de l'entrée. Par convention (par exemple, dans Agda, mais malheureusement pas en Haskell), la portée de la lambda s'étend rightwards autant que possible, de sorte que vous pouvez souvent laisser des abstractions unbracketed quand ils sont le dernier argument d'un ordre supérieur de l'opérateur: vous pouvez le voir, je l'ai fait avec Pi. Votre Agda type (x : S) -> T devient Pi S \ x:S -> T.
(Digression. Les annotations de Type lambda sont nécessaires si vous voulez être en mesure de synthétiser le type d'abstractions. Si vous changez de type de vérification que votre mode de fonctionnement, vous avez encore besoin d'annotations pour vérifier un bêta-redex comme (\ x -> t) s, comme vous l'avez aucun moyen de deviner les types de pièces que l'ensemble. Je conseille les concepteurs modernes vérification des types et de l'exclure de la bêta-redexes de la très syntaxe.)
(Digression. Ce système est incompatible en tant que Set:Set permet l'encodage d'une variété de "menteur paradoxes". Quand Martin-Löf proposé cette théorie, Girard lui a envoyé un encodage dans son propre incompatible Système U. ultérieures paradoxe en raison de Hurkens est la plus élégante toxiques de la construction que nous connaissons.)
Combinateur de la Syntaxe et de la Normalisation
De toute façon, nous avons deux symboles, Pi et Jeu, de sorte que nous pourrions peut-être gérer une combinatoire de traduction avec S, K et deux symboles: j'ai choisi de U pour l'univers et P pour le produit.
Nous pouvons maintenant définir le type combinatoire syntaxique (avec 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 :.
Notez que j'ai compris les moyens d'inclure des variables libres représenté par type a dans cette syntaxe. En plus d'être un réflexe de ma part (chaque syntaxe digne de ce nom est libre monade avec return d'incorporation de variables et d' >>= lance substitution), ça va être pratique pour représenter des étapes intermédiaires dans le processus de conversion termes avec la liaison de leur combinatoire forme.
Voici la normalisation:
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 exercice pour le lecteur est de définir un type pour exactement les formes normales et d'aiguiser les types de ces opérations.)
Représentant Type De La Théorie
Nous pouvons maintenant définir une syntaxe pour notre type de théorie.
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)
J'utilise un indice de de Bruijn représentation dans l'Bellegarde et Crochet (comme popularisé par les Oiseaux et Paterson). Le type Su a a un élément de plus que a, et nous l'utilisons comme le type de variables libres sous un classeur, avec Ze que la nouvelle variable liée et Su x étant la représentation décalée de l'ancien gratuit variable x.
La traduction des Termes de Combinators
Et avec ce fait, nous avons acquérir l'habitude de la traduction, basée sur le support de l'abstraction.
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
En tapant les Combinators
La traduction montre la manière dont nous utilisons les combinators, ce qui nous donne bien une idée de ce que leurs types. U et P sont simplement définir les constructeurs, donc, l'écriture non traduite en types et en permettant "Agda notation" pour Pi, nous devrions avoir
U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set
L' K combinator est utilisé pour soulever une valeur d'un certain type A pour une fonction constante par rapport a un autre type G.
G : Set A : Set
-------------------------------
K : (a : A) -> (g : G) -> A
L' S combinator est utilisé pour soulever des applications sur un type, sur lesquelles toutes les parties peuvent dépendre.
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 vous regardez le type d' S, vous verrez que c'est exactement unis le contexte de l'application de la règle de la théorie des types, de sorte que c'est ce qui le rend approprié pour refléter l'application de construire. C'est son travail!
Nous avons ensuite application uniquement pour fermé les choses
f : Pi A B
a : A
--------------
f a : B a
Mais il y a un hic. J'ai écrit les types de la combinators ordinaire type de théorie, pas de combinatoire théorie des types. Heureusement, j'ai une machine qui va faire la traduction.
Un Système De Type Combinatoire
---------
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
Donc là vous l'avez, dans toutes ses illisible gloire: une combinatoire de présentation de l' Set:Set!
Il y a encore un peu d'un problème. La syntaxe du système vous donne aucun moyen de deviner l' G, A et B paramètres pour S et, de même, pour K, juste des termes. En conséquence, nous pouvons le vérifier en tapant dérivations algorithmiquement, mais nous ne pouvons pas juste typecheck combinator termes que nous avons pu avec le système d'origine. Ce qui peut fonctionner, c'est d'exiger l'entrée de l'typechecker de porter des annotations de type sur les utilisations de S et K, de manière efficace de l'enregistrement de la dérivation. Mais c'est une autre boîte de pandore...
C'est un bon endroit pour s'arrêter, si vous avez été vif assez pour commencer. Le reste est "derrière les coulisses" des choses.
Générer les Types de la Combinators
J'ai généré ceux combinatoire types en utilisant le support de l'abstraction de la traduction de la théorie des types de termes. Pour montrer comment j'ai fait, et de mettre ce post pas entièrement inutile, permettez-moi de vous offrir mon équipement.
Je peux écrire les types de la combinators, entièrement prélevée sur leurs paramètres comme suit. Je me sers de mon handy pil de la fonction, qui combine Pi et lambda pour éviter de répéter le type de domaine, et plutôt bienveillant, me permet d'utiliser Haskell fonction de l'espace pour lier les variables. Peut-être que vous pouvez presque lire ce qui suit!
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)
Avec ces définie, j'ai extrait les pertinentes ouvrir subterms et a couru à travers la traduction.
Un de Bruijn d'Encodage Toolkit
Voici comment construire pil. Tout d'abord, je définir une classe d' Finite définit, pour les variables. Chaque série a un constructeur de préservation embedding dans le jeu ci-dessus, en plus d'un nouveau top élément, et vous pouvez leur dire à part: l' embd fonction vous indique si une valeur est dans l'image de l' emb.
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
Nous pouvons, bien sûr, instancier Fin pour Ze et 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
Maintenant, je peux définir des moins-ou-égal à égal, avec un affaiblissement de l'opération.
class (Fin x, Fin y) => Le x y where
wk :: x -> y
L' wk fonction doit intégrer les éléments d' x comme le plus grand des éléments d' y, de sorte que le supplément de choses en y sont plus petites, et donc dans de de Bruijn conditions de l'index, lié plus localement.
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
Et une fois que vous avez trié, un bit de rang n skullduggery fait le reste.
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 fonction d'ordre supérieur n'est pas seulement vous donner un terme représentant la variable, il vous donne une surcharge chose qui devient la représentation correcte de la variable dans un champ où la variable est visible. Qui est, le fait que je vais à la difficulté de distinguer les différentes portées par type donne le Haskell typechecker suffisamment d'informations pour calculer le décalage nécessaire pour la traduction de Bruijn représentation. Pourquoi garder un chien et d'écorce de vous-même?
