Tried out makam (lambda Prolog dialect) http://astampoulis.github.io/makam/ . Remarkable velocity although poor tooling.

kappa.makam

%open syntax.

expr : type.

id : expr.
compose : expr -> expr -> expr.

bang : expr.

v : (_ : string) -> expr.

kappa : string -> expr -> expr.
lift : expr -> expr.

z : (_ : int) -> expr.
add : expr.

var : syntax string.
expr, base : syntax expr.

`(syntax_rules <<
  expr ->
      compose { <base> "∘" <expr> }
      / lift { "lift" <expr> }
      / base ;

  base ->
      id { "id" }
      / bang { "!" }
      / add { "add" }
      / kappa { "κ" <var> "." <expr> }
      / z { <makam.int_literal> }
      / v { <var> }
      / { "(" <expr> ")" } ;

  var -> { <makam.string_literal> }
  >>).
`(syntax.def_toplevel_js expr ).

val : type.
bangval : val.
zval : (_ : int) -> val.
tupleval : (_ : val) (_ : val) -> val.

(* TODO figure out lists later *)
env : type.
nil : env.
bind : (_ : string) (_ : val) (_ : env) -> env.

search : (Env : env) (Key : string) (Val : val) -> prop.
search (bind Key Val _) Key Val.
(* FIXME is there a not equals constraint to maybe use here? *)
search (bind _ _ Tail) Key Val :-
    search Tail Key Val.

eval : (_ : env) (_ : expr) (_ : val) (_ : val) -> prop.
eval _ id X X.
eval Env (compose F G) X Z :-
    eval Env G X Y,
    eval Env F Y Z.
eval _ bang _ bangval.

eval Env (v Var) bangval Y :-
    search Env Var Y.

eval Env (lift F) T (tupleval H T) :-
    eval Env F bangval H.
eval Env (kappa Var Body) (tupleval H T) Y :-
    eval (bind Var H Env) Body T Y.

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

evalstr : (_ : string) (_ : val) -> prop.
evalstr Input Output :-
    syntax.run expr Input Ast,
           eval nil Ast bangval Output.

evalstr << (add ∘ (lift 3)) ∘ lift 5 >> Y ?
evalstr << (κ "x" . (add ∘ (lift "x")) ∘ lift "x") ∘ lift 4 >> Y ?