Jaki jest logiczny odpowiednik intuicjonistycznej teorii typów?

Question 1

Niedawno ukończyłem kurs uniwersytecki, na którym występowali Haskell i Agda (zależny funkcjonalny język programowania typizowanego) i zastanawiałem się, czy jest możliwe zastąpienie w nich rachunku lambda logiką kombinacyjną. W przypadku Haskella wydaje się to możliwe przy użyciu kombinatorów S i K, dzięki czemu jest to bezcelowe. Zastanawiałem się, jaki jest odpowiednik dla Agdy. To znaczy, czy można uczynić zależnie typizowany funkcjonalny język programowania jako odpowiednik Agdy bez używania jakichkolwiek zmiennych?

Czy można w jakiś sposób zastąpić kwantyfikację kombinatorami? Nie wiem, czy to zbieg okoliczności, ale na przykład uniwersalna kwantyfikacja sprawia, że sygnatura typu wygląda jak wyrażenie lambda. Czy istnieje sposób na usunięcie uniwersalnej kwantyfikacji z sygnatury typu bez zmiany jej znaczenia? Np. W:

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

Czy można to samo wyrazić bez użycia forall?

Question 2

Więc pomyślałem o tym trochę więcej i zrobiłem pewien postęp. Oto pierwsza próba zakodowania zachwycająco prostego (ale niespójnego) Set : Setsystemu Martina-Löfa w kombinacyjnym stylu. To nie jest dobry sposób na zakończenie, ale to najłatwiejsze miejsce na rozpoczęcie. Składnia tej teorii typów to po prostu rachunek lambda z adnotacjami typu, typami Pi i Zbiorem wszechświata.

Teoria typów docelowych

Dla kompletności przedstawię zasady. Prawidłowość kontekstu mówi tylko, że możesz budować konteksty z pustych, dołączając nowe zmienne zamieszkujące Sets.

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

A teraz możemy powiedzieć, jak syntetyzować typy terminów w dowolnym kontekście i jak zmienić typ czegoś, aż do obliczeniowego zachowania terminów, które zawiera.

  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

W niewielkiej odmianie oryginału, uczyniłem lambdę jedynym operatorem wiązania, więc drugim argumentem Pi powinna być funkcja obliczająca sposób, w jaki zwracany typ zależy od danych wejściowych. Zgodnie z konwencją (np. W Agdzie, ale niestety nie w Haskell), zakres lambda rozszerza się w prawo tak daleko, jak to możliwe, więc często można pozostawić abstrakcje bez nawiasów, gdy są ostatnim argumentem operatora wyższego rzędu: widzisz, że tak to z Pi. Twój typ Agdy (x : S) -> Tstaje się Pi S \ x:S -> T.

( Dygresja . Adnotacje typu na lambdzie są konieczne, jeśli chcesz mieć możliwość syntezy typu abstrakcji. Jeśli przełączysz na sprawdzanie typu jako modus operandi, nadal potrzebujesz adnotacji, aby sprawdzić beta-redex (\ x -> t) s, ponieważ nie masz możliwości odgadnąć typy części z całości. Radzę współczesnym projektantom sprawdzić typy i wykluczyć beta-redeksy z samej składni.)

( Dygresja . Ten system jest niespójny, ponieważ Set:Setpozwala na kodowanie różnych "paradoksów kłamców". Kiedy Martin-Löf zaproponował tę teorię, Girard przesłał mu zakodowanie jej w swoim własnym niespójnym Systemie U. Kolejnym paradoksem spowodowanym przez Hurkensa jest najładniejsza toksyczna konstrukcja, jaką znamy.)

Składnia i normalizacja kombinatora

W każdym razie mamy dwa dodatkowe symbole, Pi i Set, więc być może uda nam się połączyć kombinację z S, K i dwoma dodatkowymi symbolami: wybrałem U dla wszechświata i P dla produktu.

Teraz możemy zdefiniować nietypową składnię kombinacyjną (ze zmiennymi wolnymi):

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

Zauważ, że aw tej składni zawarłem środki umożliwiające uwzględnienie wolnych zmiennych reprezentowanych przez typ . Oprócz bycia refleksem z mojej strony (każda składnia godna tej nazwy jest wolną monadą z returnwbudowanymi zmiennymi i >>=dokonującym się podstawieniem), przydałoby się przedstawić etapy pośrednie w procesie konwersji terminów z wiązaniem z ich kombinacyjną formą.

Oto normalizacja:

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

(Ćwiczenie dla czytelnika polega na zdefiniowaniu typu dokładnie dla form normalnych i wyostrzeniu typów tych operacji).

Reprezentująca teorię typów

Możemy teraz zdefiniować składnię dla naszej teorii typów.

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)

Używam reprezentacji indeksu de Bruijna w stylu Bellegarde and Hook (spopularyzowanym przez Birda i Patersona). Typ Su ama o jeden element więcej niż ai używamy go jako typu wolnych zmiennych w segregatorze, Zejako nowo powiązanej zmiennej i Su xbędącej przesuniętą reprezentacją starej wolnej zmiennej x.

Tłumaczenie terminów na kombinatory

Po wykonaniu tych czynności uzyskujemy zwykłe tłumaczenie oparte na abstrakcji nawiasów .

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

Wpisywanie kombinatorów

Tłumaczenie pokazuje sposób, w jaki używamy kombinatorów, co daje nam pewną wskazówkę, jakie powinny być ich typy. Ui Psą tylko konstruktorami zestawów, więc pisząc nieprzetłumaczone typy i zezwalając na „notację Agda” dla Pi, powinniśmy mieć

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

KSyntezatora służy do podnoszenia wartości pewnego rodzaju Ado stałej funkcji przez jakiegoś innego rodzaju G.

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

SSyntezatora jest używany do zastosowań wyporu ponad typu, po którym wszystkie części mogą być uzależnione.

  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)

Jeśli spojrzysz na typ S, zobaczysz, że dokładnie określa kontekstową regułę stosowania teorii typów, więc to sprawia, że nadaje się do odzwierciedlenia konstrukcji aplikacji. To jego praca!

Mamy wtedy podanie tylko do spraw zamkniętych

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

Ale jest haczyk. Napisałem typy kombinatorów w teorii typów zwykłych, a nie w teorii typów kombinacyjnych. Na szczęście mam maszynę, która wykona tłumaczenie.

System typów kombinacyjnych

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

Więc masz to, w całej swojej nieczytelnej chwale: kombinacyjna prezentacja Set:Set!

Nadal jest mały problem. Składnia systemu daje nie sposób odgadnąć G, Aa Bparametry Si podobnie dla K, tylko od warunków. Odpowiednio, możemy algorytmicznie weryfikować wyprowadzanie typograficzne, ale nie możemy po prostu sprawdzać terminów kombinatora, tak jak to było w przypadku oryginalnego systemu. To, co może zadziałać, to wymaganie, aby dane wejściowe do sprawdzarki typu zawierały adnotacje typu dotyczące zastosowań S i K, skutecznie rejestrując derywację. Ale to kolejna puszka robaków ...

To dobre miejsce na przystanek, jeśli byłeś wystarczająco chętny, aby zacząć. Reszta to sprawy „za kulisami”.

Generowanie typów kombinatorów

Wygenerowałem te kombinacyjne typy przy użyciu tłumaczenia abstrakcji nawiasów z odpowiednich terminów teorii typów. Aby pokazać, jak to zrobiłem i sprawić, by ten post nie był do końca bezcelowy, pozwól mi zaoferować swój sprzęt.

Potrafię zapisać typy kombinatorów, całkowicie wyabstrahowane z ich parametrów, w następujący sposób. Korzystam z mojej poręcznej pilfunkcji, która łączy Pi i lambdę, aby uniknąć powtarzania typu domeny, i raczej w przydatny sposób pozwala mi używać przestrzeni funkcyjnej Haskella do wiązania zmiennych. Być może prawie możesz przeczytać poniższe!

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)

Po ich zdefiniowaniu wyodrębniłem odpowiednie otwarte podteksty i przepuściłem je przez tłumaczenie.

A de Bruijn Encoding Toolkit

Oto jak budować pil. Po pierwsze, definiuję klasę Finzbiorów ite, używanych dla zmiennych. Każdy taki zestaw zawiera embedding z zachowaniem konstruktora w powyższym zestawie oraz nowy topelement, który można odróżnić od siebie: embdfunkcja informuje, czy wartość znajduje się w obrazie emb.

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

Możemy oczywiście utworzyć instancję Findla ZeiSuc

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

Teraz mogę zdefiniować mniej lub równe, z osłabiającą operacją.

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

wkFunkcja powinna osadzić elementy xjak największych elementów y, tak że dodatkowe rzeczy ysą mniejsze, a zatem de Bruijn względem indeksu, związana bardziej lokalnie.

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

A kiedy już to załatwisz, odrobina umiejętności rangi n skullduggery zrobi resztę.

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)

Funkcja wyższego rzędu nie tylko podaje termin reprezentujący zmienną, ale daje ci przeciążoną rzecz, która staje się poprawną reprezentacją zmiennej w dowolnym zakresie, w którym zmienna jest widoczna. Oznacza to, że fakt, że zadaję sobie trud rozróżnienia różnych zakresów według typu, daje kontrolerowi typu Haskell wystarczającą ilość informacji do obliczenia przesunięcia wymaganego do tłumaczenia na reprezentację de Bruijna. Po co trzymać psa i szczekać?

Question 3

Wydaje mi się, że „Bracket Abstraction” działa również w przypadku typów zależnych w pewnych okolicznościach. W sekcji 5 tego artykułu znajdziesz kilka typów K i S:

Skandaliczne, ale znaczące zbiegi okoliczności
Zależna składnia i ocena bezpieczna dla typu
Conor McBride, University of Strathclyde, 2010

Przekształcenie wyrażenia lambda w wyrażenie kombinatoryczne z grubsza odpowiada konwersji naturalnego dowodu dedukcji na dowód w stylu Hilberta.

Answer 1

Niedawno ukończyłem kurs uniwersytecki, na którym występowali Haskell i Agda (zależny funkcjonalny język programowania typizowanego) i zastanawiałem się, czy jest możliwe zastąpienie w nich rachunku lambda logiką kombinacyjną. W przypadku Haskella wydaje się to możliwe przy użyciu kombinatorów S i K, dzięki czemu jest to bezcelowe. Zastanawiałem się, jaki jest odpowiednik dla Agdy. To znaczy, czy można uczynić zależnie typizowany funkcjonalny język programowania jako odpowiednik Agdy bez używania jakichkolwiek zmiennych?

Czy można w jakiś sposób zastąpić kwantyfikację kombinatorami? Nie wiem, czy to zbieg okoliczności, ale na przykład uniwersalna kwantyfikacja sprawia, że sygnatura typu wygląda jak wyrażenie lambda. Czy istnieje sposób na usunięcie uniwersalnej kwantyfikacji z sygnatury typu bez zmiany jej znaczenia? Np. W:

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

Czy można to samo wyrazić bez użycia forall?

Answer 2

21

Zacznij od ustalenia najbardziej zależnych typów możliwych dla K (łatwe) i S (raczej włochate). Byłoby interesujące dorzucić stałe dla Set i Pi, a następnie spróbować zrekonstruować podstawowy (niespójny) system Set: Set. Pomyślałbym dalej, ale muszę złapać samolot.

pigworker,

Answer 3

Więc pomyślałem o tym trochę więcej i zrobiłem pewien postęp. Oto pierwsza próba zakodowania zachwycająco prostego (ale niespójnego) Set : Setsystemu Martina-Löfa w kombinacyjnym stylu. To nie jest dobry sposób na zakończenie, ale to najłatwiejsze miejsce na rozpoczęcie. Składnia tej teorii typów to po prostu rachunek lambda z adnotacjami typu, typami Pi i Zbiorem wszechświata.

Teoria typów docelowych

Dla kompletności przedstawię zasady. Prawidłowość kontekstu mówi tylko, że możesz budować konteksty z pustych, dołączając nowe zmienne zamieszkujące Sets.

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

A teraz możemy powiedzieć, jak syntetyzować typy terminów w dowolnym kontekście i jak zmienić typ czegoś, aż do obliczeniowego zachowania terminów, które zawiera.

  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

W niewielkiej odmianie oryginału, uczyniłem lambdę jedynym operatorem wiązania, więc drugim argumentem Pi powinna być funkcja obliczająca sposób, w jaki zwracany typ zależy od danych wejściowych. Zgodnie z konwencją (np. W Agdzie, ale niestety nie w Haskell), zakres lambda rozszerza się w prawo tak daleko, jak to możliwe, więc często można pozostawić abstrakcje bez nawiasów, gdy są ostatnim argumentem operatora wyższego rzędu: widzisz, że tak to z Pi. Twój typ Agdy (x : S) -> Tstaje się Pi S \ x:S -> T.

( Dygresja . Adnotacje typu na lambdzie są konieczne, jeśli chcesz mieć możliwość syntezy typu abstrakcji. Jeśli przełączysz na sprawdzanie typu jako modus operandi, nadal potrzebujesz adnotacji, aby sprawdzić beta-redex (\ x -> t) s, ponieważ nie masz możliwości odgadnąć typy części z całości. Radzę współczesnym projektantom sprawdzić typy i wykluczyć beta-redeksy z samej składni.)

( Dygresja . Ten system jest niespójny, ponieważ Set:Setpozwala na kodowanie różnych "paradoksów kłamców". Kiedy Martin-Löf zaproponował tę teorię, Girard przesłał mu zakodowanie jej w swoim własnym niespójnym Systemie U. Kolejnym paradoksem spowodowanym przez Hurkensa jest najładniejsza toksyczna konstrukcja, jaką znamy.)

Składnia i normalizacja kombinatora

W każdym razie mamy dwa dodatkowe symbole, Pi i Set, więc być może uda nam się połączyć kombinację z S, K i dwoma dodatkowymi symbolami: wybrałem U dla wszechświata i P dla produktu.

Teraz możemy zdefiniować nietypową składnię kombinacyjną (ze zmiennymi wolnymi):

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

Zauważ, że aw tej składni zawarłem środki umożliwiające uwzględnienie wolnych zmiennych reprezentowanych przez typ . Oprócz bycia refleksem z mojej strony (każda składnia godna tej nazwy jest wolną monadą z returnwbudowanymi zmiennymi i >>=dokonującym się podstawieniem), przydałoby się przedstawić etapy pośrednie w procesie konwersji terminów z wiązaniem z ich kombinacyjną formą.

Oto normalizacja:

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

(Ćwiczenie dla czytelnika polega na zdefiniowaniu typu dokładnie dla form normalnych i wyostrzeniu typów tych operacji).

Reprezentująca teorię typów

Możemy teraz zdefiniować składnię dla naszej teorii typów.

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)

Używam reprezentacji indeksu de Bruijna w stylu Bellegarde and Hook (spopularyzowanym przez Birda i Patersona). Typ Su ama o jeden element więcej niż ai używamy go jako typu wolnych zmiennych w segregatorze, Zejako nowo powiązanej zmiennej i Su xbędącej przesuniętą reprezentacją starej wolnej zmiennej x.

Tłumaczenie terminów na kombinatory

Po wykonaniu tych czynności uzyskujemy zwykłe tłumaczenie oparte na abstrakcji nawiasów .

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

Wpisywanie kombinatorów

Tłumaczenie pokazuje sposób, w jaki używamy kombinatorów, co daje nam pewną wskazówkę, jakie powinny być ich typy. Ui Psą tylko konstruktorami zestawów, więc pisząc nieprzetłumaczone typy i zezwalając na „notację Agda” dla Pi, powinniśmy mieć

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

KSyntezatora służy do podnoszenia wartości pewnego rodzaju Ado stałej funkcji przez jakiegoś innego rodzaju G.

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

SSyntezatora jest używany do zastosowań wyporu ponad typu, po którym wszystkie części mogą być uzależnione.

  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)

Jeśli spojrzysz na typ S, zobaczysz, że dokładnie określa kontekstową regułę stosowania teorii typów, więc to sprawia, że nadaje się do odzwierciedlenia konstrukcji aplikacji. To jego praca!

Mamy wtedy podanie tylko do spraw zamkniętych

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

Ale jest haczyk. Napisałem typy kombinatorów w teorii typów zwykłych, a nie w teorii typów kombinacyjnych. Na szczęście mam maszynę, która wykona tłumaczenie.

System typów kombinacyjnych

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

Więc masz to, w całej swojej nieczytelnej chwale: kombinacyjna prezentacja Set:Set!

Nadal jest mały problem. Składnia systemu daje nie sposób odgadnąć G, Aa Bparametry Si podobnie dla K, tylko od warunków. Odpowiednio, możemy algorytmicznie weryfikować wyprowadzanie typograficzne, ale nie możemy po prostu sprawdzać terminów kombinatora, tak jak to było w przypadku oryginalnego systemu. To, co może zadziałać, to wymaganie, aby dane wejściowe do sprawdzarki typu zawierały adnotacje typu dotyczące zastosowań S i K, skutecznie rejestrując derywację. Ale to kolejna puszka robaków ...

To dobre miejsce na przystanek, jeśli byłeś wystarczająco chętny, aby zacząć. Reszta to sprawy „za kulisami”.

Generowanie typów kombinatorów

Wygenerowałem te kombinacyjne typy przy użyciu tłumaczenia abstrakcji nawiasów z odpowiednich terminów teorii typów. Aby pokazać, jak to zrobiłem i sprawić, by ten post nie był do końca bezcelowy, pozwól mi zaoferować swój sprzęt.

Potrafię zapisać typy kombinatorów, całkowicie wyabstrahowane z ich parametrów, w następujący sposób. Korzystam z mojej poręcznej pilfunkcji, która łączy Pi i lambdę, aby uniknąć powtarzania typu domeny, i raczej w przydatny sposób pozwala mi używać przestrzeni funkcyjnej Haskella do wiązania zmiennych. Być może prawie możesz przeczytać poniższe!

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)

Po ich zdefiniowaniu wyodrębniłem odpowiednie otwarte podteksty i przepuściłem je przez tłumaczenie.

A de Bruijn Encoding Toolkit

Oto jak budować pil. Po pierwsze, definiuję klasę Finzbiorów ite, używanych dla zmiennych. Każdy taki zestaw zawiera embedding z zachowaniem konstruktora w powyższym zestawie oraz nowy topelement, który można odróżnić od siebie: embdfunkcja informuje, czy wartość znajduje się w obrazie emb.

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

Możemy oczywiście utworzyć instancję Findla ZeiSuc

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

Teraz mogę zdefiniować mniej lub równe, z osłabiającą operacją.

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

wkFunkcja powinna osadzić elementy xjak największych elementów y, tak że dodatkowe rzeczy ysą mniejsze, a zatem de Bruijn względem indeksu, związana bardziej lokalnie.

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

A kiedy już to załatwisz, odrobina umiejętności rangi n skullduggery zrobi resztę.

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)

Funkcja wyższego rzędu nie tylko podaje termin reprezentujący zmienną, ale daje ci przeciążoną rzecz, która staje się poprawną reprezentacją zmiennej w dowolnym zakresie, w którym zmienna jest widoczna. Oznacza to, że fakt, że zadaję sobie trud rozróżnienia różnych zakresów według typu, daje kontrolerowi typu Haskell wystarczającą ilość informacji do obliczenia przesunięcia wymaganego do tłumaczenia na reprezentację de Bruijna. Po co trzymać psa i szczekać?

Answer 4

to może być bardzo głupie, ale jak zmieni się to zdjęcie, jeśli dodasz Fkombinator? Fzachowuje się różnie w zależności od pierwszego argumentu: Jeśli Ajest atomem Mi Nsą wyrażeniami i PQjest złożeniem, to FAMN -> Mi F(PQ)MN -> NPQ. Nie można tego przedstawić w SK(I)rachunku różniczkowym, ale Kmożna to przedstawić jako FF. Czy można w ten sposób przedłużyć darmowy MLTT?

kram1032

Answer 5

Jestem prawie pewien, że jest problem z tą procedurą abstrakcji nawiasów, a konkretnie z częścią „kombinatory stają się stałymi”, która tłumaczy λx.c na Kc dla kombinatorów c ∈ {S, K, U, P}. Problem w tym, że te kombinatory są polimorficzne i mogą być używane w typie zależnym od x; taki typ nie może być zachowany przez to tłumaczenie. Jako konkretny przykład tłumaczony jest termin λ (A : Set) → λ (a : A) → atypu , którego nie można użyć w typie, w którym typ drugiego argumentu zależy od pierwszego argumentu. (A : Set) → (a : A) → AS(S(KS)(KK))(KK)

Anders Kaseorg,

Answer 6

Wydaje mi się, że „Bracket Abstraction” działa również w przypadku typów zależnych w pewnych okolicznościach. W sekcji 5 tego artykułu znajdziesz kilka typów K i S:

Skandaliczne, ale znaczące zbiegi okoliczności
Zależna składnia i ocena bezpieczna dla typu
Conor McBride, University of Strathclyde, 2010

Przekształcenie wyrażenia lambda w wyrażenie kombinatoryczne z grubsza odpowiada konwersji naturalnego dowodu dedukcji na dowód w stylu Hilberta.

Jaki jest logiczny odpowiednik intuicjonistycznej teorii typów?

Odpowiedzi:

Teoria typów docelowych

Składnia i normalizacja kombinatora

Reprezentująca teorię typów

Tłumaczenie terminów na kombinatory

Wpisywanie kombinatorów

System typów kombinacyjnych

Generowanie typów kombinatorów

A de Bruijn Encoding Toolkit