Czy w Systemie F à la Church możemy zautomatyzować wnioskowanie o typie dla eliminacji dla wszystkich?

Pytanie jest następujące. Zasadniczo, gdy ktoś ma taki termin$\Lambda X.t$, możemy wyeliminować forall poprzez zastosowanie tego terminu do typu, na przykład$(\Lambda X.t)[T]\to t[X:=T]$.

Załóżmy teraz, że jest to strzałka i chcemy podać jej argument, wówczas musielibyśmy zastosować ten termin do odpowiedniego typu, aby mógł otrzymać taki argument. O to pytam, czy mogę zautomatyzować: Czy można zbudować funkcję$f$ biorąc dwa warunki i zwracając typ taki, że $f<{\Lambda X.t}><{r}>$ podaj typ, który należy zastąpić $X$ w $t$ takie, że $t$ może zaakceptować argument $r$?

Kilka przykładów:

• $f<{\Lambda X.\lambda x^{X\to X}.t}><{\lambda x^T.x}>=T$.

• $f<{\Lambda X.\lambda x^X.r}><{(\lambda x^{R}.t^T)~s}>=T$

Nie jestem pewien, czy zrozumiałem pytanie. Najpierw staram się zredukować problem do następującego problemu zjednoczenia:

Biorąc pod uwagę układ F typu τ (X) z dowolną zmienną (typ) X i typ σ.
Czy można znaleźć taki typ γ, że τ (γ) = σ?

Oto pseudo-kod (z wyjątkiem zgłaszanego wyjątku, gdy nie jest jednoznaczny) do rozwiązania tego problemu.

unify (X, σ) = σ
unify (Y, Y) = Y
unify (τ₁ → τ₂, σ₁ → σ₂) = unify(τ₁,σ₁) → unify(τ₂,σ₂)
unify (∀Y.τ(Y), ∀Y.σ(Y)) = ∀Y.unify(τ(Y),σ(Y)) (with Y a fresh variable)
unify (_,_) = raise Not_unifiable

Możesz udowodnić (przez indukcję), że γ = τ (unify (τ (X), σ) działa, jeśli tylko wyjątek nie jest zgłoszony.

Teraz twój problem możesz wziąć

f (ΛX.t) (r) = match type of t with "τ₁ → τ₂" => unify (τ₁, type of r) | _ => fail end

(oczywiście twoja funkcja f powinna przyjąć jako argument kontekst, jeśli twoje terminy są otwarte).