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.
