Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Messing with dependent type systems in makam (http://astampoulis.github.io/makam/)
(* terms *)
term : type.
universe : term.
annotate : term -> term -> term.
unitType : term.
unitTerm : term.
pairType : term -> (term -> term) -> term.
pairTerm : term -> term -> term.
pairElim : term -> (term -> term -> term) -> term.
funType : term -> (term -> term) -> term.
funTerm : (term -> term) -> term.
funElim : term -> term -> term.
(* values *)
neu : type.
whnf : type.
whnf_neu : neu -> whnf.
whnf_universe : whnf.
whnf_unitType : whnf.
whnf_unitTerm : whnf.
whnf_pairTerm : whnf -> whnf -> whnf.
(* semantics *)
eval : term -> whnf -> prop.
eval universe whnf_universe.
eval (annotate Term _) Term' :-
eval Term Term'.
eval unitTerm whnf_unitType.
eval unitType whnf_universe.
eval (pairType First Second) _ :-
eval First First',
TODO.
eval (pairTerm First Second) (whnf_pairTerm First' Second') :-
eval First First',
eval Second Second'.
eval (pairElim _ _) _ :- TODO.
eval (funType ParamType BodyType) _ :-
eval ParamType ParamType',
TODO.
eval (funTerm _) _ :- TODO.
eval (funElim _ _) _ :- TODO.
equal : whnf -> whnf -> prop.
equal whnf_universe whnf_universe.
equal whnf_unitType whnf_unitType.
equal whnf_unitTerm whnf_unitTerm.
equal (whnf_pairTerm First0 Second0) (whnf_pairTerm First1 Second1) :-
equal First0 First1,
equal Second0 Second1.
(* typing *)
check : term -> whnf -> prop.
synth : term -> whnf -> prop.
check (pairTerm First Second) _ :- TODO.
check (funTerm Body) _ :- TODO.
check Term Type :-
synth Term Type',
equal Type Type'.
synth universe whnf_universe.
synth (annotate Term Type) Type' :-
eval Type Type',
check Term Type'.
synth unitTerm whnf_unitType.
synth unitType whnf_universe.
synth (pairType FirstType SecondType) _ :- TODO.
synth (pairElim Head Body) _ :- TODO.
synth (funType ParamType BodyType) _ :- TODO.
synth (funElim Head Arg) _ :- TODO.
(* -------------------------------------------------------------------------- *)
(* tests *)
check universe Type ?
dependent : testsuite.
%testsuite dependent.
>> check universe whnf_universe ?
>> Yes.
>> check unitTerm whnf_unitType ?
>> Yes.
>> check universe (whnf_neu Type) ?
>> Yes.
>> synth (pairTerm _ _) _ ?
>> Impossible.
>> synth (funTerm _) _ ?
>> Impossible.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment