|
% Tento soubor obsahuje jednoduchý typový systém |
|
% pro lambda kalkul (takzvaný STLC) s inty a booly navíc. |
|
% https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus |
|
% Je to takový zjednodušený základ pro typový systém Haskellu. |
|
|
|
?- set_prolog_flag(occurs_check, true). |
|
% ^ Tahle vlajka zařídí to, že Prolog selže při unifikaci druhu `X = f(X)`. |
|
% To se nám hodí, aby se Prolog nesnažil najít řešení pro rovnici typu `A = A -> B` |
|
% (To by se mohlo stát u výrazu jako `\x -> x x`) |
|
|
|
% Vyhledávání v asociovaném seznamu |
|
% to jest seznamu, který v sobě má (key, value) dvojice |
|
lookup([(X,A)|_], X, A). |
|
lookup([(Y,_)|T], X, A) :- \+ X = Y, lookup(T, X, A). |
|
|
|
% `typ/4` najde typ daného výrazu |
|
% a prochází až do hloubky dané Fuel |
|
% což je číslo v Peanově aritmetice |
|
% typ(+LookupDictionary, ?Expression, ?Type, +Fuel) |
|
|
|
% aplikace E na F má typ B pokud |
|
% ... E má typ A -> B |
|
% ... F má typ A |
|
typ(G, app(E, F), B, s(N)) :- |
|
typ(G, E, A -> B, N), |
|
typ(G, F, A, N). |
|
|
|
% funkce \x -> E má typ A -> B pokud |
|
% ... E má typ B v prostředí, ve kterém má x typ A |
|
typ(G, lam(var(X), E), A -> B, s(N)) :- |
|
typ([(X, A) | G], E, B, N). |
|
|
|
% x má typ A, pokud má tento typ v prostředí |
|
typ(G, var(X), A, s(_)) :- |
|
lookup(G, X, A). |
|
|
|
% čísla mají typ int |
|
typ(_, X, int, s(_)) :- |
|
integer(X). |
|
|
|
% konstanty fls, tru mají typ bool |
|
typ(_, fls, bool, s(_)). |
|
typ(_, tru, bool, s(_)). |
|
|
|
% A + B má typ int, pokud |
|
% ... A má typ int |
|
% ... B má typ int |
|
typ(_, A + B, int, s(N)) :- |
|
typ(G, A, int, N), |
|
typ(G, B, int, N). |
|
|
|
% Cvičení: Přidejte si ifzero(X, Then, Else), která má typ A, pokud: |
|
% ... X má typ int |
|
% ... Then má typ A |
|
% ... Else má také typ A |
|
|
|
% Překonvertuje Prologovská čísla na Peanova |
|
into_peano(0, z). |
|
into_peano(N, s(P)) :- |
|
N > 0, |
|
N1 is N - 1, |
|
into_peano(N1, P). |
|
|
|
% Vyrobí výraz dle typu, omezeno hloubkou dle Fuel |
|
synth(Expr, Type, Fuel) :- |
|
into_peano(Fuel, N), |
|
typ([], Expr, Type, N). |
|
|
|
% Zjisti typ pro daný výraz |
|
infer(Expr, Type) :- |
|
into_peano(10000, N), % |
|
typ([], Expr, Type, N). |
|
|
|
% |
|
% P Ř Í K L A D Y : |
|
% |
|
% najdi všechny výrazy hloubky < 4 typu int |
|
% > synth(E, int, 4). |
|
% |
|
% zjisti typ T pro \x -> 2 + x |
|
% > X = var(x), infer(lam(X, 2 + X), T). |
|
% |
|
% najdi všechny výrazy hloubky < 5 a typu bool -> bool -> int |
|
% > synth(E, bool -> bool -> int, 5). |