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
. |- 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
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
C S :. f :. a $. g = f $. g $. (a :. g)
C K :. a $. g = a
n $. g = n :. norm g
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))
| Tm a :$ Tm a
| Pi (Tm a) (Tm a)
| 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
bra (V Ze) = C S :. C K :. C K
bra (V (Su x)) = C K :. V x
bra (C c) = C K :. C c
bra (f :. a) = C S :. bra f :. bra a
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
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
emb = magic
embd _ = Nothing
instance Fin x => Fin (Su x) where
top = Su top
emb Ze = Ze
emb (Su x) = Su (emb x)
embd Ze = Just Ze
embd (Su x) = fmap Su (embd x)
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
instance Le x y => Le (Su x) (Su y) where
wk x = case embd x of
Nothing -> top
Just y -> emb (wk y)
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ć?