Ik heb onlangs een universitaire opleiding afgerond met Haskell en Agda (een afhankelijke getypeerde functionele programmeertaal), en vroeg me af of het mogelijk was om lambda-calculus hierin te vervangen door combinatorische logica. Met Haskell lijkt dit mogelijk met de S en K combinators, waardoor het puntloos wordt. Ik vroeg me af wat het equivalent was voor Agda. D.w.z. kan men een afhankelijk getypeerde functionele programmeertaal equivalent maken aan Agda zonder variabelen te gebruiken?
Is het ook mogelijk om kwantificering op de een of andere manier te vervangen door combinators? Ik weet niet of dit toeval is, maar universele kwantificering laat een typesignatuur er bijvoorbeeld uitzien als een lambda-uitdrukking. Is er een manier om universele kwantificering van een typehandtekening te verwijderen zonder de betekenis ervan te veranderen? bijv. in:
forall a : Int -> a < 0 -> a + a < a
Kan hetzelfde worden uitgedrukt zonder een forall te gebruiken?
Antwoord 1, autoriteit 100%
Dus ik heb er wat meer over nagedacht en wat vooruitgang geboekt. Hier is een eerste poging om Martin-Löfs heerlijk eenvoudige (maar inconsistente) Set : Setsysteem in een combinatorische stijl te coderen. Het is geen goede manier om te eindigen, maar het is de gemakkelijkste plek om te beginnen. De syntaxis van deze typetheorie is gewoon lambda-calculus met typeannotaties, Pi-typen en een universumset.
De doeltypetheorie
Voor de volledigheid zal ik de regels presenteren. Contextvaliditeit zegt alleen dat je lege contexten kunt bouwen door nieuwe variabelen in Sets te plaatsen.
G |- valid G |- S : Set
-------------- ----------------------------- x fresh for G
. |- valid G, x:S |- valid
En nu kunnen we zeggen hoe we typen voor termen in een bepaalde context kunnen synthetiseren en hoe we het type van iets kunnen veranderen tot aan het rekengedrag van de termen die het bevat.
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
In een kleine variatie op het origineel heb ik lambda tot de enige bindende operator gemaakt, dus het tweede argument van Pi zou een functie moeten zijn die berekent hoe het retourtype afhangt van de invoer. Volgens afspraak (bijvoorbeeld in Agda, maar helaas niet in Haskell), strekt het bereik van lambda zich zo ver mogelijk naar rechts uit, dus je kunt abstracties vaak zonder haakjes laten als ze het laatste argument zijn van een operator van hogere orde: je kunt zien dat ik dat deed dat met Pi. Uw Agda-type (x : S) -> Twordt Pi S \ x:S -> T.
(Uitweiding. Typeannotaties op lambda zijn nodig als je het type abstracties wilt synthetiseren. Als je overschakelt naar type checkingem>als je modus operandi, heb je nog steeds annotaties nodig om een bèta-redex zoals (\ x -> t) ste controleren, omdat je de soorten onderdelen niet kunt raden van die van Ik raad moderne ontwerpers aan om typen te controleren en bèta-redexes uit te sluiten van de syntaxis.)
(Uitweiding. Dit systeem is inconsistent omdat Set:Setde codering van een verscheidenheid aan “leuge paradoxen” toestaat. Toen Martin-Löf deze theorie voorstelde, stuurde Girard hem een codering ervan in zijn eigen inconsistente System U. De daaropvolgende paradox vanwege Hurkens is de meest nette giftige constructie die we kennen.)
Combinatorsyntaxis en normalisatie
Hoe dan ook, we hebben twee extra symbolen, Pi en Set, dus misschien kunnen we een combinatorische vertaling maken met S, K en twee extra symbolen: ik koos U voor het universum en P voor het product.
Nu kunnen we de ongetypte combinatorische syntaxis (met vrije variabelen) definiëren:
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 :.
Merk op dat ik de middelen heb opgenomen om vrije variabelen op te nemen die worden vertegenwoordigd door type Ain deze syntaxis. Behalve dat het een reflex van mijn kant is (elke syntaxis die de naam waardig is, is een vrije monade met returningesloten variabelen en >>=voor vervanging), zal het handig zijn om tussenstadia weer te geven in het proces van het omzetten van termen met binding aan hun combinatorische vorm.
Hier is normalisatie:
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 $.
(Een oefening voor de lezer is om een type te definiëren voor precies de normaalvormen en de typen van deze bewerkingen aan te scherpen.)
Typetheorie representeren
We kunnen nu een syntaxis definiëren voor onze typetheorie.
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)
Ik gebruik een weergave van de Bruijn-index op de manier van Bellegarde en Hook (zoals gepopulariseerd door Bird en Paterson). Het type Su aheeft één element meer dan A, en we gebruiken het als het type vrije variabelen onder een binder, met Zeals de nieuw gebonden variabele en Su xis de verschoven weergave van de oude vrije variabele x.
Voorwaarden vertalen naar combinators
En daarmee krijgen we de gebruikelijke vertaling, gebaseerd op abstractie met haakjes.
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
De combinaties typen
De vertaling laat zien hoe we de combinators gebruiken, wat ons een aardig idee geeft van wat hun typen zouden moeten zijn. Uen Pzijn slechts setconstructors, dus als we onvertaalde typen schrijven en “Agda-notatie” voor Pi toestaan, zouden we moeten hebben
U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set
De Kcombinator wordt gebruikt om een waarde van een bepaald type Anaar een constante functie te tillen boven een ander type G.
G : Set A : Set
-------------------------------
K : (a : A) -> (g : G) -> A
De Scombinator wordt gebruikt om applicaties over een type te tillen, waarvan alle onderdelen afhankelijk kunnen zijn.
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)
Als je naar het type Skijkt, zul je zien dat het precies de gecontextualiseerdetoepassingsregel van de typetheorie aangeeft, dus dat maakt het geschikt om weerspiegelen de toepassingsconstructie. Dat is zijn werk!
We hebben dan alleen een aanvraag voor gesloten dingen
f : Pi A B
a : A
--------------
f a : B a
Maar er is een probleem. Ik heb de typen van de combinators geschreven in de gewone typetheorie, niet in de combinatorische typetheorie. Gelukkig heb ik een machine die de vertaling zal maken.
Een combinatiesysteem
---------
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
Dus daar heb je het, in al zijn onleesbare glorie: een gecombineerde presentatie van Set:Set!
Er is nog steeds een probleem. De syntaxis van het systeem geeft u geen manier om de parameters G, Aen Bvoor Sen dergelijke te raden voor K, alleen uit de voorwaarden. Dienovereenkomstig kunnen we typafleidingenalgoritmisch verifiëren, maar we kunnen niet zomaar combinatortermen typen zoals we dat konden met het originele systeem. Wat zou kunnen werken, is dat de invoer voor de typechecker typeannotaties moet bevatten over het gebruik van S en K, waardoor de afleiding effectief wordt vastgelegd. Maar dat is weer een blik wormen…
Dit is een goede plek om te stoppen, als je enthousiast genoeg bent geweest om te beginnen. De rest is “achter de schermen”.
Het genereren van de typen combinators
Ik heb die combinatorische typen gegenereerd met behulp van de haakabstractievertaling uit de relevante termen uit de typetheorie. Om te laten zien hoe ik het heb gedaan, en om dit bericht niet helemaal zinloos te maken, bied ik mijn apparatuur aan.
Ik kan de typen combinators, volledig geabstraheerd over hun parameters, als volgt schrijven. Ik maak gebruik van mijn handige functie pil, die Pi en lambda combineert om herhaling van het domeintype te voorkomen, en die me vrij behulpzaam in staat stelt om Haskell’s functieruimte te gebruiken om variabelen te binden. Misschien kun je het volgende bijna lezen!
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)
Nadat deze waren gedefinieerd, heb ik de relevante opensubtermen eruit gehaald en door de vertaling gehaald.
Een coderingstoolkit van de Bruijn
Hier leest u hoe u pilbouwt. Ten eerste definieer ik een klasse van Finite sets, gebruikt voor variabelen. Elke set heeft een constructorbehoudende embedding in de bovenstaande set, plus een nieuw top-element, en je kunt ze van elkaar onderscheiden: de embdfunctie vertelt je of een waarde in de afbeelding van embstaat.
class Fin x where
top :: Su x
emb :: x -> Su x
embd :: Su x -> Maybe x
We kunnen natuurlijk Fininstantiëren voor Zeen 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
Nu kan ik minder-of-gelijken definiëren, met een verzwakkingoperatie.
class (Fin x, Fin y) => Le x y where
wk :: x -> y
De functie wkmoet de elementen van xinsluiten als de grootsteelementen van y, zodat de extra dingen in yzijn kleiner, en dus in termen van de Bruijn index, meer lokaal gebonden.
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
En als je dat eenmaal hebt geregeld, doet een beetje slordigheid de rest.
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)
De functie van hogere orde geeft je niet alleen een term die de variabele vertegenwoordigt, het geeft je een overbelastding dat de juiste representatie van de variabele wordt in elk bereik waar de variabele zichtbaar is. Dat wil zeggen, het feit dat ik de moeite doe om de verschillende scopes te onderscheiden per typegeeft de Haskell typechecker genoeg informatie om de verschuiving te berekenen die nodig is voor de vertaling naar de Bruijn-representatie. Waarom een hond houden en zelf blaffen?
Antwoord 2, autoriteit 15%
Ik denk dat de “Bracket Abstraction” ook werkt voor afhankelijke typen
onder bepaalde omstandigheden. In sectie 5 van het volgende document:
je vindt enkele K- en S-types:
Schandalige maar zinvolle toevalligheden
Afhankelijke typeveilige syntaxis en evaluatie
Conor McBride, Universiteit van Strathclyde, 2010
Een lambda-uitdrukking omzetten in een combinatorische uitdrukking
komt ongeveer overeen met het omzetten van een natuurlijk deductiebewijs in
een Hilbert stijl proof.