Constant definitions in Makam

[d4hines]

Here's an easy question: is there a way to define constant values in Makam? For example, I'm working through ICFP 2018 paper. I have a little implementation of the simply typed lambda calculus, and I want to convince myself of its correctness with some examples. So I've written the lambda encodings for booleans, lists, etc, but these are a hassle to copy-paste. Is there a way for me to define constants? I tried predicates on ground facts, but quickly got into an argument with the type checker and gave up. Thanks!

[brendanzab]

I've been wishing for this too - eg. for having a default typing context for my language. This is a bit related to #100 I think?

[astampoulis]

Hi @d4hines and @brendanzab ! There isn't a built-in way to define constants right now unfortunately. The situation is a little easier to work-around though compared to type-level constants: you could define a predicate to expand definitions in a term, before doing any other kind of computation (e.g. type-checking, evaluation, etc.).

Here's some code that you could use for now, but I'll see if I can add something like this to the standard library, or to the core eventually.

define : [A] A -> A -> prop.

expand_definitions, expand_definitions_aux : [A] A -> A -> prop.
expand_definitions X Y :-
  demand.case_otherwise
    (expand_definitions_aux X Y)
    (structural @expand_definitions X Y).

expand_definitions_aux D E when (define D E).

(* STLC *)

term : type.
lam : (term -> term) -> term.
app : term -> term -> term.

typ : type.
arrow : typ -> typ -> typ.

typecheck : term -> typ -> prop.

typecheck (lam E) (arrow T T') :-
  (x:term -> typecheck x T -> typecheck (E x) T').

typecheck (app E1 E2) T' :-
  typecheck E1 (arrow T T'), typecheck E2 T.

(* church numerals as example of definitions *)

intconst : int -> term.
define (intconst 0) (lam (fun z => lam (fun s => z))).
define (intconst N) (lam (fun z => lam (fun s => app s (Pred z s))))
    when lessthan 0 N true :-
  minus N 1 N',
  define (intconst N') (lam (fun z => lam (fun s => Pred z s))).

(expand_definitions (intconst 2) X, typecheck X Y) ?

There is an alternative approach, which is not common in textbooks: you could extend the base language with a constructor for using a definition, and then add a typing rule for those, that "looks up" the definition itself. Here's one way to do that:

(* STLC *)

term : type.
lam : (term -> term) -> term.
app : term -> term -> term.

typ : type.
arrow : typ -> typ -> typ.

typecheck : term -> typ -> prop.

typecheck (lam E) (arrow T T') :-
  (x:term -> typecheck x T -> typecheck (E x) T').

typecheck (app E1 E2) T' :-
  typecheck E1 (arrow T T'), typecheck E2 T.

(* add definitions *)

def : term -> term.
define : term -> term -> prop.

typecheck (def X) T :-
  define X Y, typecheck Y T.

intconst : int -> term.
define (intconst 0) (lam (fun z => lam (fun s => z))).
define (intconst N) (lam (fun z => lam (fun s => app s (Pred z s))))
    when lessthan 0 N true :-
  minus N 1 N',
  define (intconst N') (lam (fun z => lam (fun s => Pred z s))).

(typecheck (def (intconst 0)) Y) ?