Was ist das kombinatorische logische Äquivalent der intuitionistischen Typentheorie?

Ich habe kürzlich einen Universitätskurs mit Haskell und Agda (einer abhängigen typisierten funktionalen Programmiersprache) abgeschlossen und mich gefragt, ob es möglich ist, Lambda-Kalkül in diesen durch kombinatorische Logik zu ersetzen. Mit Haskell scheint dies mit den S- und K-Kombinatoren möglich zu sein, wodurch es punktfrei wird. Ich fragte mich, was das Äquivalent für Agda war. Kann man eine abhängig typisierte funktionale Programmiersprache erstellen, die Agda entspricht, ohne Variablen zu verwenden?

Ist es auch möglich, die Quantifizierung durch Kombinatoren zu ersetzen? Ich weiß nicht, ob dies ein Zufall ist, aber eine universelle Quantifizierung lässt beispielsweise eine Typensignatur wie einen Lambda-Ausdruck aussehen. Gibt es eine Möglichkeit, die universelle Quantifizierung aus einer Typensignatur zu entfernen, ohne ihre Bedeutung zu ändern? ZB in:

forall a : Int -> a < 0 -> a + a < a

Kann das Gleiche ohne Verwendung eines Foralls ausgedrückt werden?

Also habe ich ein bisschen mehr darüber nachgedacht und einige Fortschritte gemacht. Hier ist ein erster Versuch, Martin-Löfs wunderbar einfaches (aber inkonsistentes) Set : SetSystem in einem kombinatorischen Stil zu codieren . Es ist kein guter Weg, um fertig zu werden, aber es ist der einfachste Ort, um loszulegen. Die Syntax dieser Typentheorie ist nur Lambda-Kalkül mit Typanmerkungen, Pi-Typen und einer Universumsmenge.

Die Zieltyp-Theorie

Der Vollständigkeit halber werde ich die Regeln vorstellen. Die Kontextgültigkeit besagt lediglich, dass Sie Kontexte aus leeren Kontexten erstellen können, indem Sie neue Variablen in Sets nebeneinander setzen .

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

Und jetzt können wir sagen, wie man Typen für Begriffe in einem bestimmten Kontext synthetisiert und wie man den Typ von etwas bis zum Rechenverhalten der darin enthaltenen Begriffe ändert.

  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 einer kleinen Abweichung vom Original habe ich Lambda zum einzigen Bindungsoperator gemacht, daher sollte das zweite Argument von Pi eine Funktion sein, die berechnet, wie der Rückgabetyp von der Eingabe abhängt. Konventionell (z. B. in Agda, aber leider nicht in Haskell) erstreckt sich der Umfang von Lambda so weit wie möglich nach rechts, sodass Sie Abstraktionen oft ungebrochen lassen können, wenn sie das letzte Argument eines Operators höherer Ordnung sind: Sie können sehen, dass ich es getan habe das mit Pi. Ihr Agda-Typ (x : S) -> Twird Pi S \ x:S -> T.

( Exkurs . Typanmerkungen auf Lambda sind erforderlich, wenn Sie die Art der Abstraktionen synthetisieren möchten . Wenn Sie als Modusoperandi zur Typprüfung wechseln, benötigen Sie weiterhin Anmerkungen, um einen Beta-Redex wie zu überprüfen (\ x -> t) s, da Sie keine Möglichkeit haben Ich rate modernen Designern, die Typen zu überprüfen und Beta-Redexes von der Syntax auszuschließen.)

( Exkurs . Dieses System ist inkonsistent, da Set:Setes die Kodierung einer Vielzahl von "Lügnerparadoxen" ermöglicht. Als Martin-Löf diese Theorie vorschlug, schickte Girard ihm eine Kodierung in seinem eigenen inkonsistenten System U. Das nachfolgende Paradoxon aufgrund von Hurkens ist das sauberste giftige Konstruktion, die wir kennen.)

Kombinatorsyntax und Normalisierung

Wie auch immer, wir haben zwei zusätzliche Symbole, Pi und Set, so dass wir vielleicht eine kombinatorische Übersetzung mit S, K und zwei zusätzlichen Symbolen verwalten können: Ich habe U für das Universum und P für das Produkt gewählt.

Jetzt können wir die untypisierte kombinatorische Syntax (mit freien Variablen) definieren:

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 :.

Beachten Sie, dass ich die Mittel zum Einbeziehen von freien Variablen, die durch den Typ dargestellt werden, ain diese Syntax aufgenommen habe. Abgesehen davon, dass es meinerseits ein Reflex ist (jede Syntax, die diesen Namen verdient, ist eine freie Monade mit returnEinbettungsvariablen und >>=perfomierender Substitution), ist es praktisch, Zwischenstufen bei der Konvertierung von Begriffen mit Bindung an ihre kombinatorische Form darzustellen.

Hier ist die Normalisierung:

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 $.

(Eine Übung für den Leser besteht darin, einen Typ für genau die normalen Formen zu definieren und die Typen dieser Operationen zu schärfen.)

Darstellung der Typentheorie

Wir können jetzt eine Syntax für unsere Typentheorie definieren.

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)

Ich verwende eine de Bruijn-Indexdarstellung in der Art von Bellegarde und Hook (wie von Bird und Paterson populär gemacht). Der Typ Su ahat ein Element mehr als a, und wir verwenden ihn als Typ der freien Variablen unter einem Ordner, wobei Zedie neu gebundene Variable Su xdie verschobene Darstellung der alten freien Variablen ist x.

Begriffe in Kombinatoren übersetzen

Und damit erwerben wir die übliche Übersetzung, basierend auf der Klammerabstraktion .

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

Typisierung der Kombinatoren

Die Übersetzung zeigt die Art und Weise, wie wir die Kombinatoren verwenden, was uns einen ziemlichen Hinweis darauf gibt, welche Typen sie haben sollten. Uund Psind nur Set-Konstruktoren, also sollten wir haben, wenn wir nicht übersetzte Typen schreiben und "Agda-Notation" für Pi zulassen

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

Der KKombinator wird verwendet, um einen Wert eines Typs Agegenüber einem anderen Typ auf eine konstante Funktion zu heben G.

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

Der SKombinator wird verwendet, um Anwendungen über einen Typ zu heben, von dem alle Teile abhängen können.

  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)

Wenn Sie sich den Typ von ansehen S, werden Sie feststellen, dass er genau die kontextualisierte Anwendungsregel der Typentheorie angibt. Daher ist er geeignet, das Anwendungskonstrukt widerzuspiegeln. Das ist seine Aufgabe!

Wir haben dann nur Anwendung für geschlossene Sachen

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

Aber es gibt einen Haken. Ich habe die Typen der Kombinatoren in der gewöhnlichen Typentheorie geschrieben, nicht in der kombinatorischen Typentheorie. Zum Glück habe ich eine Maschine, die die Übersetzung macht.

Ein kombinatorisches Typsystem

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

Da haben Sie es also in all seiner unlesbaren Pracht: eine kombinatorische Darstellung von Set:Set!

Es gibt immer noch ein kleines Problem. Die Syntax des Systems gibt Ihnen keine Möglichkeit , das zu erraten G, Aund BParameter für Sund in ähnlicher Weise für die K, nur von den Bedingungen. Dementsprechend können wir Typisierungsableitungen algorithmisch überprüfen , aber wir können nicht einfach Kombinatorbegriffe typechecken, wie wir es mit dem ursprünglichen System könnten. Was möglicherweise funktioniert, besteht darin, dass die Eingabe in den Typechecker Typanmerkungen zu Verwendungen von S und K enthält, wodurch die Ableitung effektiv aufgezeichnet wird. Aber das ist eine andere Dose Würmer ...

Dies ist ein guter Ort, um anzuhalten, wenn Sie scharf genug waren, um anzufangen. Der Rest ist "hinter den Kulissen".

Generieren der Kombinatortypen

Ich habe diese kombinatorischen Typen mithilfe der Klammerabstraktionsübersetzung aus den relevanten typentheoretischen Begriffen generiert. Um zu zeigen, wie ich es gemacht habe und um diesen Beitrag nicht ganz sinnlos zu machen, möchte ich meine Ausrüstung anbieten.

Ich kann die Typen der Kombinatoren, die vollständig über ihre Parameter abstrahiert sind, wie folgt schreiben. Ich benutze meine praktische pilFunktion, die Pi und Lambda kombiniert, um eine Wiederholung des Domänentyps zu vermeiden, und die es mir recht hilfreich ermöglicht, den Funktionsraum von Haskell zum Binden von Variablen zu verwenden. Vielleicht können Sie fast das Folgende lesen!

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)

Nachdem diese definiert wurden, extrahierte ich die relevanten offenen Subterme und führte sie durch die Übersetzung.

A de Bruijn Encoding Toolkit

Hier erfahren Sie, wie Sie bauen pil. Zunächst definiere ich eine Klasse von Finite-Mengen, die für Variablen verwendet werden. Jede solche Menge hat eine konstruktorerhaltende embEinfügung in die obige Menge sowie ein neues topElement, und Sie können sie unterscheiden: Die embdFunktion sagt Ihnen, ob sich ein Wert im Bild von befindet emb.

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

Wir können natürlich Finfür Zeund instanziierenSuc

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

Jetzt kann ich mit einer Schwächungsoperation weniger oder gleich definieren .

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

Die wkFunktion sollte die Elemente xals die größten Elemente von einbetten y, damit die zusätzlichen Dinge in ykleiner und damit in de Bruijn-Indexbegriffen lokaler gebunden sind.

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

Und sobald Sie das geklärt haben, erledigt ein bisschen Schädelgraberei den 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)

Die Funktion höherer Ordnung gibt Ihnen nicht nur einen Begriff, der die Variable darstellt, sondern auch ein überladenes Element, das in jedem Bereich, in dem die Variable sichtbar ist, zur korrekten Darstellung der Variablen wird. Das heißt, die Tatsache, dass ich mir die Mühe mache, die verschiedenen Bereiche nach Typ zu unterscheiden, gibt dem Haskell-Typechecker genügend Informationen, um die Verschiebung zu berechnen, die für die Übersetzung in die de Bruijn-Darstellung erforderlich ist. Warum einen Hund behalten und sich bellen?

Ich denke, die "Bracket Abstraction" funktioniert unter bestimmten Umständen auch für abhängige Typen. In Abschnitt 5 des folgenden Dokuments finden Sie einige K- und S-Typen:

Unverschämte, aber bedeutungsvolle Zufälle
Abhängige typsichere Syntax und Bewertung
Conor McBride, University of Strathclyde, 2010

Die Umwandlung eines Lambda-Ausdrucks in einen kombinatorischen Ausdruck entspricht in etwa der Umwandlung eines natürlichen Abzugsbeweises in einen Hilbert-Beweis.