Jeśli coś jest proste, powinno być całkowicie wyjaśnione kilkoma słowami. Można to zrobić dla rachunku λ:

Rachunek λ jest gramatyką składniową (w zasadzie strukturą) z regułą redukcji (co oznacza, że ​​procedura wyszukiwania / zamiany jest wielokrotnie stosowana do każdego wystąpienia określonego wzorca, dopóki taki wzorzec nie istnieje).

Gramatyka:

Term = (Term Term) | (λ Var . Term) | Var

Reguła redukcji:

((λ var body) term) -> SUBS(body,var,term)
    where `SUBS` replaces all occurrences of `var`
    by `term` in `body`, avoiding name capture.

Przykłady:

(λ a . a)                             -> (λ a a)
((λ a . (λ b . (b a))) (λ x . x))     -> (λ b . (b (λ x x)))
((λ a . (a a)) (λ x . x))             -> (λ x . x)
((λ a . (λ b . ((b a) a))) (λ x . x)) -> (λ b . ((b (λ x . x)) (λ x . x)))
((λ x . (x x)) (λ x . (x x)))         -> never halts

Chociaż jest to nieco nieformalne, można argumentować, że jest to wystarczająco pouczające, aby normalny człowiek zrozumiał rachunek λ jako całość - i wymaga 22 linii przeceny. Próbuję zrozumieć systemy typu czystego / zależnego używane przez Idris / Agda i podobne projekty, ale krótszym wyjaśnieniem, które mogłem znaleźć, było po prostu łatwe - świetny artykuł, ale wydaje się, że zakłada on dużo wcześniejszej wiedzy (Haskell, indukcyjny definicje), których nie mam. Myślę, że coś krótszego, mniej bogatego może wyeliminować niektóre z tych barier. A zatem,

Czy można podać krótkie, pełne wyjaśnienie układów typu czystego / zależnego, w tym samym formacie, w którym przedstawiłem rachunek λ powyżej?

Zrzeczenie się

Jest to bardzo nieformalne, jak prosiłeś.

Gramatyka

W języku zależnym od typu mamy spoiwo na poziomie typu, a także na poziomie wartości:

Term = * | (∀ (Var : Term). Term) | (Term Term) | (λ Var. Term) | Var

Dobrze wpisany termin to termin z załączonym typem, napiszemy t ∈ σlub

σ
t

wskazując, że termin tma typ σ.

Zasady pisania

Dla uproszczenia wymagamy tego w λ v. t ∈ ∀ (v : σ). τobu przypadkach λi ∀wiążemy tę samą zmienną ( vw tym przypadku).

Zasady:

t ∈ σ is well-formed if σ ∈ * and t is in normal form (0)

*            ∈ *                                                 (1)
∀ (v : σ). τ ∈ *             -: σ ∈ *, τ ∈ *                     (2)
λ v. t       ∈ ∀ (v : σ). τ  -: t ∈ τ                            (3)
f x          ∈ SUBS(τ, v, x) -: f ∈ ∀ (v : σ). τ, x ∈ σ          (4)
v            ∈ σ             -: v was introduced by ∀ (v : σ). τ (5)

Zatem *„jest typem wszystkich typów” (1), ∀tworzy typy z typów (2), abstrakcje lambda mają typy pi (3), a jeśli vwprowadza je ∀ (v : σ). τ, to vma typ σ(5).

„w normalnej formie” oznacza, że ​​wykonujemy możliwie najwięcej redukcji, stosując zasadę redukcji:

„Reguła redukcji”

(λ v. b ∈ ∀ (v : σ). τ) (t ∈ σ) ~> SUBS(b, v, t) ∈ SUBS(τ, v, t)
    where `SUBS` replaces all occurrences of `v`
    by `t` in `τ` and `b`, avoiding name capture.

Lub w dwuwymiarowej składni gdzie

σ
t

oznacza t ∈ σ:

(∀ (v : σ). τ) σ    SUBS(τ, v, t)
                 ~>
(λ  v     . b) t    SUBS(b, v, t)

Można zastosować abstrakcję lambda do terminu, gdy termin ma ten sam typ co zmienna w powiązanym kwantyfikatorze. Następnie zmniejszamy zarówno abstrakcję lambda, jak i kwantyfikator forall w taki sam sposób, jak w czystym rachunku lambda wcześniej. Po odjęciu części poziomu wartości otrzymujemy regułę pisania (4).

Przykład

Oto operator aplikacji funkcji:

∀ (A : *) (B : A -> *) (f : ∀ (y : A). B y) (x : A). B x
λ  A       B            f                    x     . f x

(możemy skrócić ∀ (x : σ). τdo σ -> τjeżeli τnie wspominając x)

fzwraca B ydla dowolnego podanego ytypu A. Stosujemy fsię x, który jest odpowiedni rodzaj A, a substytutem ydla xw ∀PO ., więc f x ∈ SUBS(B y, y, x)~> f x ∈ B x.

Skróćmy teraz operatora aplikacji funkcji jako appi zastosujmy go do siebie:

∀ (A : *) (B : A -> *). ?
λ  A       B          . app ? ? (app A B)

Stawiam ?na warunki, które musimy podać. Najpierw wyraźnie wprowadzamy i tworzymy wystąpienia Aoraz B:

∀ (f : ∀ (y : A). B y) (x : A). B x
app A B

Teraz musimy ujednolicić to, co mamy

∀ (f : ∀ (y : A). B y) (x : A). B x

który jest taki sam jak

(∀ (y : A). B y) -> ∀ (x : A). B x

i co app ? ?otrzymuje

∀ (x : A'). B' x

To skutkuje

A' ~ ∀ (y : A). B y
B' ~ λ _. ∀ (x : A). B x -- B' ignores its argument

(patrz także Co to jest predykatywność? )

Nasze wyrażenie (po zmianie nazwy) staje się

∀ (A : *) (B : A -> *). ?
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

Ponieważ dla każdego A, Bi f(gdzie f ∈ ∀ (y : A). B y)

∀ (y : A). B y
app A B f

możemy utworzyć Ai Buzyskać (dla każdego fz odpowiednim typem)

∀ (y : ∀ (x : A). B x). ∀ (x : A). B x
app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) f

a podpis typu jest równoważny (∀ (x : A). B x) -> ∀ (x : A). B x.

Całe wyrażenie brzmi

∀ (A : *) (B : A -> *). (∀ (x : A). B x) -> ∀ (x : A). B x
λ  A       B          . app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B)

To znaczy

∀ (A : *) (B : A -> *) (f : ∀ (x : A). B x) (x : A). B x
λ  A       B            f                    x     .
    app (∀ (x : A). B x) (λ _. ∀ (x : A). B x) (app A B) f x

co po wszystkich obniżkach na poziomie wartości daje to samo app.

Więc choć wymaga to zaledwie kilka kroków w czystym rachunkiem lambda, aby uzyskać appod app app, w typie ustawienia (a zwłaszcza w sposób zależny od wpisane) musimy także dbać o unifikacji i rzeczy stają się bardziej złożone nawet z pewnym wygody inconsitent ( * ∈ *).

Sprawdzanie typu

• Jeśli tjest *następnie t ∈ *przez (1)
• Jeśli tjest ∀ (x : σ) τ, σ ∈? *, τ ∈? *(patrz uwaga na temat ∈?poniżej), a następnie t ∈ *przez (2)
• Jeśli tjest f x, f ∈ ∀ (v : σ) τaby część σ, a τ, x ∈? σa następnie t ∈ SUBS(τ, v, x)przez (4)
• Jeśli tjest to zmienna v, vwprowadzona została ∀ (v : σ). τnastępnie t ∈ σprzez (5)

Wszystkie są regułami wnioskowania, ale nie możemy zrobić tego samego dla lambdas (wnioskowanie typu jest nierozstrzygalne dla typów zależnych). Więc dla lambdas sprawdzamy ( t ∈? σ) zamiast wnioskować:

• Jeśli tjest λ v. bi sprawdzone przeciwko ∀ (v : σ) τ, b ∈? τtot ∈ ∀ (v : σ) τ
• Jeśli tjest coś innego i sprawdzone w stosunku do σtego, wywnioskuj rodzaj tużycia powyższej funkcji i sprawdź, czy tak jestσ

Sprawdzanie równości typów wymaga, aby były one w normalnej formie, więc aby zdecydować, czy tma typ σ, najpierw sprawdzamy, czy σma typ *. Jeśli tak, to σjest normalizowalny (paradoks modulo Girarda) i normalizuje się (stąd σstaje się dobrze uformowany przez (0)). SUBSnormalizuje również wyrażenia do zachowania (0).

Nazywa się to dwukierunkowym sprawdzaniem typu. Dzięki niemu nie musimy dodawać adnotacji do każdej lambda typem: jeśli w f xtypie fjest znany, to xjest sprawdzany pod kątem rodzaju argumentu fotrzymywanego zamiast wnioskowania i porównywania pod kątem równości (co jest również mniej wydajne). Ale jeśli fjest lambda, wymaga wyraźnej adnotacji typu (adnotacje są pomijane w gramatyce i wszędzie można dodać Ann Term Termlub λ' (σ : Term) (v : Var)do konstruktorów).

Rzuć też okiem na prostsze, łatwiejsze! post na blogu.

Chodźmy. Nie zawracam sobie głowy paradoksem Girarda, ponieważ odwraca on uwagę od głównych idei. Będę musiał przedstawić maszynerię prezentacyjną na temat osądów i pochodnych i tym podobnych.

Gramatyka

Termin :: = (Elim) | * | (Var: Termin) → Termin | λVar↦Term

Elim :: = Termin: Termin | Var | Elim Termin

Gramatyka ma dwie wzajemnie zdefiniowane formy, „terminy”, które są ogólnym pojęciem rzeczy (typy są rzeczami, wartości są rzeczami), w tym * (typ typów), typy funkcji zależnych i abstrakty lambda, ale także osadzają „ eliminacje ”(tzn.„ zastosowania ”zamiast„ konstrukcje ”), które są zagnieżdżonymi aplikacjami, w których rzecz ostatecznie w pozycji funkcji jest albo zmienną, albo terminem opatrzonym adnotacją ze swoim typem.

Zasady redukcji

(λy↦t: (x: S) → T) s ↝ t [s: S / y]: T [s: S / x]

(t: T) ↝ t

Operacja podstawienia t [e / x] zastępuje każde wystąpienie zmiennej x eliminacją e, unikając przechwytywania nazw. Aby utworzyć aplikację, która może zredukować, termin lambda musi być opatrzony adnotacjami według typu, aby wyeliminować . Adnotacja typu nadaje abstrakcji lambda rodzaj „reaktywności”, umożliwiając kontynuowanie aplikacji. Gdy osiągniemy punkt, w którym nie będzie już więcej aplikacji, a aktywny t: T zostanie ponownie osadzony w składni terminu, możemy usunąć adnotację typu.

Rozszerzmy relację redukcji by o zamknięcie strukturalne: zasady obowiązują w dowolnym miejscu warunków i eliminacji, że można znaleźć coś pasującego do lewej strony. Napisz ↝ * dla zwrotno-przechodniego (0-lub więcej-stopniowego) zamknięcia ↝. Powstały system redukcji jest zbieżny w tym sensie:

Jeśli s ↝ * p i s ↝ * q, to ​​istnieje takie r, że p ↝ * r i q ↝ * r.

Konteksty

Kontekst :: = | Kontekst, Var: Termin

Konteksty to sekwencje, które przypisują typy do zmiennych, rosnące po prawej stronie, które uważamy za „lokalny” koniec, mówiąc nam o ostatnio powiązanych zmiennych. Ważną właściwością kontekstów jest to, że zawsze można wybrać zmienną, która nie jest jeszcze używana w kontekście. Zachowujemy niezmienność, że zmienne przypisane typy w kontekście są różne.

Wyroki

Wyrok :: = Kontekst ⊢ Termin ma termin | Kontekst ⊢ Elim jest terminem

To jest gramatyka wyroków, ale jak je czytać? Na początek ⊢ jest tradycyjnym symbolem „kołowrotu”, oddzielającym założenia od wniosków: można je odczytać nieformalnie jako „mówi”.

G ⊢ T ma t

oznacza, że ​​w kontekście G typ T przyjmuje termin t;

G ⊢ e to S

oznacza, że ​​w kontekście G, eliminacja e ma typ S.

Sądy mają interesującą strukturę: zero lub więcej danych wejściowych , jeden lub więcej tematów , zero lub więcej danych wyjściowych .

INPUTS                   SUBJECT        OUTPUTS
Context |- Term   has    Term
Context |-               Elim      is   Term

Oznacza to, że musimy z góry zaproponować rodzaje terminów i po prostu je sprawdzić , ale syntezujemy rodzaje eliminacji.

Zasady pisania

Przedstawiam je w nieco niejasnym stylu prologicznym, pisząc J -: P1; ...; Pn, aby wskazać, że orzeczenie J obowiązuje, jeśli przesłanki od P1 do Pn również mają zastosowanie. Przesłanką będzie kolejny wyrok lub roszczenie o obniżkę.

Warunki

G ⊢ T ma t -: T ↝ R; G ⊢ R ma t

G ⊢ * ma *

G ⊢ * ma (x: S) → T -: G ⊢ * ma S; G, z: S! - * ma T [z / x]

G ⊢ (x: S) → T ma λy↦t -: G, z: S ⊢ T [z / x] ma t [z / y]

G ⊢ T ma (e) -: G ⊢ e jest T

Eliminacje

G ⊢ e to R -: G ⊢ e to S; S ↝ R

G, x: S, G '⊢ x to S

G ⊢ fs to T [s: S / x] -: G ⊢ f to (x: S) → T; G ⊢ S ma s

I to wszystko!

Tylko dwie reguły nie są ukierunkowane na składnię: reguła, która mówi „możesz zredukować typ, zanim użyjesz go do sprawdzenia terminu” oraz reguła, która mówi „możesz zredukować typ po zsyntetyzowaniu go z eliminacji”. Jedną z realnych strategii jest redukcja typów, dopóki nie ujawnisz najwyższego konstruktora.

Ten system nie jest silnie normalizujący (z powodu paradoksu Girarda, który jest paradoksem odwoływania się do kłamstwa), ale można go silnie normalizować, dzieląc * na „poziomy wszechświata”, gdzie wszelkie wartości, które dotyczą typów na niższych poziomach, same mają typy na wyższych poziomach, co zapobiega odwoływaniu się do siebie.

Ten system ma jednak w tym sensie właściwość zachowania typu.

Jeśli G ⊢ T ma t, a G ↝ * D i T ↝ * R i t ↝ r, to D ⊢ R ma r.

Jeśli G ⊢ e to S, a G ↝ * D i e ↝ f, to istnieje R takie, że S ↝ * R i D ⊢ f to R.

Konteksty można obliczać, umożliwiając obliczenie zawartych w nich terminów. Oznacza to, że jeśli orzeczenie jest teraz ważne, możesz obliczyć jego dane wejściowe tak, jak chcesz, i jeden temat, a następnie będzie można jakoś obliczyć jego dane wyjściowe, aby upewnić się, że wynikowy wyrok pozostanie ważny. Dowodem jest prosta indukcja na temat pisania na klawiaturze, biorąc pod uwagę zbieżność -> *.

Oczywiście przedstawiłem tutaj tylko rdzeń funkcjonalny, ale rozszerzenia mogą być dość modułowe. Oto pary.

Termin :: = ... | (x: S) * T | s, t

Elim :: = ... | e.head | e.tail

(s, t: (x: S) * T) .heads: S

(s, t: (x: S) * T) .tail ↝ t: T [s: S / x]

G ⊢ * ma (x: S) * T -: G ⊢ * ma S; G, z: S ⊢ * ma T [z / x]

G ⊢ (x: S) * T ma s, t -: G ⊢ S ma s; G ⊢ T [s: S / x] ma t

G ⊢ e.head is S -: G ⊢ e is (x: S) * T

G ⊢ e. Ogon to T [e.head / x] -: G ⊢ e to (x: S) * T

Korespondencja Curry-Howarda mówi, że istnieje systematyczna zgodność między systemami typów i systemami dowodzenia w logice. Przyjmując to zorientowane na programistę, możesz przekształcić to w następujący sposób:

• Logiczne systemy sprawdzające to języki programowania.
• Te języki są wpisywane statycznie.
• Obowiązkiem systemu czcionek w takim języku jest zakazanie programów, które konstruowałyby fałszywe dowody.

Patrząc pod tym kątem:

• Niekreślony rachunek lambda, który podsumowujesz, nie ma znaczącego systemu typów, więc zbudowany na nim system dowodzenia byłby niewłaściwy.
• Prosto wpisany rachunek lambda jest językiem programowania, który ma wszystkie typy niezbędne do budowania proofów dźwiękowych w logice sentymentalnej („jeśli / to”, „i”, „lub”, „nie”). Ale jego typy nie są wystarczająco dobre, aby sprawdzić dowody zawierające kwantyfikatory („dla wszystkich x, ...”; „istnieje x taki, że ...”).
• Rachunek lambda zależnie wpisany ma typy i reguły, które obsługują logikę sentymentalną i kwantyfikatory pierwszego rzędu (kwantyfikacja ponad wartościami).

Oto zasady naturalnego odliczenia dla logiki pierwszego rzędu, przy użyciu diagramu z pozycji Wikipedii na temat naturalnego odliczenia . Są to w zasadzie także zasady minimalnie zależnego rachunku lambda.

Pamiętaj, że reguły zawierają wyrażenia lambda. Można je odczytać jako programy, które konstruują dowody zdań reprezentowanych przez ich typy (lub, mówiąc bardziej zwięźle, mówimy, że programy są dowodami ). Podobne zasady redukcji, które podajesz, można zastosować do tych warunków lambda.

Dlaczego nam na tym zależy? Po pierwsze, ponieważ proofy mogą okazać się przydatnym narzędziem w programowaniu, a posiadanie języka, który może współpracować z proofami, ponieważ obiekty pierwszej klasy otwierają wiele możliwości. Na przykład, jeśli twoja funkcja ma warunek wstępny, zamiast zapisywać ją jako komentarz, możesz faktycznie zażądać jej dowodu jako argumentu.

Po drugie, ponieważ maszyneria systemu typów potrzebna do obsługi kwantyfikatorów może mieć inne zastosowania w kontekście programowania. W szczególności języki o typie zależnym obsługują uniwersalne kwantyfikatory („dla wszystkich x, ...”) za pomocą pojęcia zwanego typami funkcji zależnych - funkcją, w której typ statyczny wyniku może zależeć od wartości czasu wykonywania argumentu.

Aby nadać temu zastosowanie bardzo pieszo, piszę cały czas kod, który musi czytać pliki Avro , które składają się z rekordów o jednolitej strukturze - wszystkie mają ten sam zestaw nazw i typów pól. Wymaga to ode mnie:

1. Zakoduj na stałe strukturę rekordów w programie jako typ rekordu.
   • Zalety: Kod jest prostszy, a kompilator może wykryć błędy w moim kodzie
   • Wada: program jest zakodowany na stałe do odczytu plików zgodnych z typem rekordu.
2. Przeczytaj schemat danych w czasie wykonywania, reprezentuj go ogólnie jako strukturę danych i używaj go do ogólnego przetwarzania rekordów
   • Zalety: Mój program nie jest zakodowany na stałe tylko dla jednego typu pliku
   • Wady: kompilator nie może wychwycić tylu błędów.

Jak widać na stronie samouczka Avro Java , pokazują one, jak korzystać z biblioteki zgodnie z obydwoma tymi podejściami.

Z zależnymi typami funkcji możesz mieć ciasto i zjeść je, kosztem bardziej złożonego systemu typów. Możesz napisać funkcję, która odczytuje plik Avro, wyodrębnia schemat i zwraca zawartość pliku jako strumień rekordów, których typ statyczny zależy od schematu przechowywanego w pliku . Kompilator byłby w stanie wychwycić błędy, w których na przykład próbowałem uzyskać dostęp do nazwanego pola, które może nie istnieć w rekordach plików, które będzie przetwarzane w czasie wykonywania. Kochanie, co?