The hoas support is kind of neat but idk.

hoas.makam

%open syntax.

%extend kz.

obj : type.
terminal : obj.
fn : obj -> obj -> obj.
tuple : obj -> obj -> obj.

typ : type.
mp : obj -> obj -> typ.

term : type.
id : term.
compose : term -> term -> term.
bang : term.
kappa : obj -> (term -> term) -> term.
lift : term -> term.
zeta : obj -> (term -> term) -> term.
pass : term -> term.

%end.

%extend kz.

typeof : term -> typ -> prop.

typeof id (mp A A).
typeof (compose F G) (mp A C) :-
    typeof F (mp B C),
    typeof G (mp A B).
typeof bang (mp _ terminal).
typeof (pass X) (mp (fn A B) B) :-
    typeof X (mp terminal A).
typeof (lift X) (mp B (tuple A B)) :-
    typeof X (mp terminal A).

typeof (kappa A F) (mp (tuple A B) C) :-
    (x:term -> typeof x (mp terminal A) -> typeof (F x) (mp B C)).

typeof (zeta A F) (mp B (fn A C)) :-
    (x:term -> typeof x (mp terminal A) -> typeof (F x) (mp B C)).

%end.

%extend kz.
val : type.
env : type.

bangval : val.
tupleval : val -> val -> val.
fnval : (term -> term) -> val -> val.

big : term -> val -> val -> prop.
big id X X.
big (compose F G) X Z :-
    big G X Y,
    big F Y Z.
big bang _ bangval.
big (lift F) B (tupleval A B) :-
    big F bangval A.
big (kappa _ F) (tupleval H T) Y :-
    (load:term -> big load bangval H -> big (F load) T Y).
big (zeta _ F) X (fnval F X).
big (pass X) (fnval F Y) Z :-
    big X bangval Val,
    (load:term -> big load bangval Val -> big (F load) Y Z).

%end.

%extend kz.
(* Integer Extras *)
integer : obj.

z : int -> term.
add : term.

typeof (z _) (mp terminal integer).
typeof add (mp (tuple integer (tuple integer terminal)) integer).

zval : int -> val.

big (z N) bangval (zval N).
big add (tupleval (zval X) (tupleval (zval Y) bangval)) (zval Z) :-
   plus X Y Z.

%end.

%extend kz.

(* Syntax *)
compound_obj_syn, obj_syn : syntax obj.
ty_syn : syntax typ.

expr, base : syntax term.

base_val, val_syn : syntax val.

var : type.
v : string -> var.
var_syn : syntax var.

mykappa : var -> obj -> term -> term.
load : var -> term.

subst : term -> term -> prop.

subst_ : [A] A -> A -> prop.
subst X Y :-
    demand.case_otherwise (subst_ X Y) (structural @subst X Y).

get : var -> term -> prop.

(* subst_ (kappa A F) Y :-
    subst_ (F _) G,
    unify Y (kappa A (fun x => F x)). *)
subst_ (load Var) Y :-
    print "get",
    get Var Y,
    print "did get".
subst_ (mykappa Var A Body) (kappa A F) :-
    print "let",
    (get Var X -> subst Body Y).

`(syntax_rules <<
  compound_obj_syn ->
      fn { <obj_syn> "⇒" <compound_obj_syn> }
      / tuple { <obj_syn> "×" <compound_obj_syn> }
      / obj_syn
 >>).
`(syntax_rules <<
  obj_syn ->
      integer { "Z" }
      / terminal { "1" }
      / { "(" <compound_obj_syn> ")" }
 >>).
`(syntax_rules <<
  ty_syn ->
      mp { <obj_syn> "→" <obj_syn> }
 >>).
`(syntax_rules <<
  var_syn ->
      v { <makam.string_literal> } ;
  expr ->
      compose { <base> "∘" <expr> }
      / mykappa { "κ" <var_syn> ":" <obj_syn> "." <expr> }
      / lift { "lift" <expr> }
      / pass { "pass" <expr> }
      / base
 >>).
`(syntax_rules <<
  base ->
      id { "id" }
      / bang { "!" }
      / add { "add" }
      / z { <makam.int_literal> }
      / load { <var_syn> }
      / { "(" <expr> ")" }
   >>).
 `(syntax_rules <<

  val_syn ->
       base_val
  >>).
`(syntax_rules <<
  base_val ->
      bangval { "!" }
      / zval { <makam.int_literal> }
      / tupleval { "⟨" <base_val> "," <val_syn> "⟩" }
      / { "(" <val_syn> ")" }

 >>).
%end.

kz.subst (kz.let (kz.v "x") (kz.z 5) (kz.load (kz.v "x"))) Y ?
kz.subst (kz.kappa kz.terminal (fun x_0_0 => kz.let (kz.v "x") x_0_0 (kz.load (kz.v "x")))) Y ?
run : (_ : string) -> prop.
run Input :-
    print_string "\n",
    print_string Input,
    print_string "\n",
    syntax.run kz.expr Input Named,
    print Named,
    kz.subst Named Term,
    print Term,
    kz.typeof Term Ty,
    syntax.run kz.ty_syn TyStr Ty,
    print_string ": ",
    print_string TyStr,
    print_string "\n",
    kz.big Term kz.bangval Y,
    syntax.run kz.val_syn YStr Y,
    print_string "⇒ ",
    print_string YStr,
    print_string "\n".

go : prop.
go :-
    run <<id>>,
    run << κ "x" : 1 . "x" >>.

go ?