eqv seems to be useful when defining particular equivalence relations. For instance, unordered equivalence between sets. However, the problem in my opinion is that the default implementation (which is just syntactic equivalence) should do a recursive call to eqv.

The problem arises when using types that have subterms from other types, that could have an explicit eqv relation. For instance:

# eqv (expansion L) (expansion R) ?    
Impossible.

# eqv [ expansion L] [expansion R] ?
Yes:
L := R,
R := R.

# eqv (dyn (expansion L) ) (dyn (expansion R ) )?
Yes:
R := R,
L := R.

expansion has an explicit eqv relation, but list expansion doesn't care about that.

A different approach would be to redefine eqv for every datatype (list, map, ...) (like manually defining Eq on Haskell), but I think structural should work.

I'd be happy to make this change in a PR, let me know if you think this makes sense or if there's any particular reason not to do it.

Hi, I'm writing my first language using Makam and I loosely follow the first part of the tutorial.
My syntax rules don't compile and I can't figure out what is wrong. Here is the relavant part of my code.

%use basic_predicates.
%open syntax.

(* abstract syntax *)

expr : type.
intConst : int -> expr.
var : string -> expr.
lam : string -> expr -> expr.
app : expr -> expr -> expr.

env : type.
both : env -> env -> env.
def : string -> expr -> env.

(* concrete syntax *)

expr : syntax expr.
env : syntax env.

`(syntax_rules <<
    expr ->
        intConst { <makam.int_literal> }
      / var      { <makam.ident> }
      / lam      { "fun" <makam.ident> "." <expr> }
      / app      { <expr> <expr> }
      /          { "(" <expr> ")" }

    env ->
        both     { <def> ";" <env> }
      / def      { <makam.ident> "=" <expr> }
>>).

`(syntax.def_toplevel_js expr).
`(syntax.def_toplevel_js env).

I get the following errors:

!! Error in <string>:1:97-100:
   Term of type string -> expr -> env,
   whereas expected a type of form syntax env.


!! Error in file ./syntax.makam:22.18-33.1:
   parsing the syntax rules failed


!! Error in file ./syntax.makam:22.3-33.1:
   Error in staged code.

The error seems to be related to the subrule def { <makam.ident> "=" <expr> }. Athough I don't have a deep understanding of Makam I believe my code is correct. Please help.

P.S: it's not clear if I have to give my own definitions for the cases of expr and env besides the syntax rules. I get a different error if I omit them.

P.S.2: I installed Makam via npm. My version is 0.7.40.

In the following file:

typeof (mkpath (["tox"]) (["IpAddr"])) (join ([(ref (mkpath (["tox"]) (["Ipv4Addr"]))), (ref (mkpath (["tox"]) (["Ipv6Addr"])))])).
typeof (mkpath (["tox"]) (["Ipv4Addr"])) (prod ([(mkpath (["tox"]) (["Ipv4Addr", "0"])), (mkpath (["tox"]) (["Ipv4Addr", "1"]))])).
typeof (mkpath (["tox"]) (["Ipv4Addr", "0"])) (meet ([(val ((value_int 0x02)) integer), (u 1 big_endian)])).

Makam could report the lack of support for hexadecimals in a more clear way (by the way, consider supporting hexadecimals).

It would be convenient to be able to write type aliases, like:

byte : type.
byte = int.

I realise this could run into the same issue as adding functions though (like, it might require changing the core, which you want to avoid), so this might be too hard to do right now.

They are very convenient to have.

Hi!
I'd like to learn λ-Prolog. I've picked up a copy of Dale Miller's Programming with Higher Order Logic. It recommends the Teyjus system. Do you think I could get by using Makam instead? Are there large differences in syntax or semantics I should be concerned about?
Thanks!
Daniel Hines

The standard library and some of the examples use <- in clauses, but the tutorial uses :-. It seems like :- was added in 822a1f0 - is that now the preferred syntax?

As an aside I just want to really thank you for Makam, it's a really neat tool and I've been having a bunch of fun playing around with it. I also really appreciate that you have it published on NPM/Yarn - it makes it super easy to install. Thanks for all your work! 😍 👏 🎉

Hi! See this cool online demo: https://lingo-workbench.dev/ . More info: https://petevilter.me/post/datalog-typechecking/ . Author was able to implement very elegant universal IDE in browser using ideas similar to yours. The author wrote IDE using Datalog, which is similar to your Makam. (Dual issue: vilterp/datalog-ts#374 )

It seems that Makam follows the “fail on the first error” approach. It would be much nicer if Makam could report many valid errors at once.

For REPL driven development, it would be great to be able to import definitions from a file in REPL with a single command.

todo created by @astampoulis

original line:

// TODO: connect this to literature

from commit: bd03309

track progress: http://tododrop.com/todo/89

I'm running into this error with qualified imports (a reduced test case of a more complicated project):

a.makam:

foo : type.
foo : foo.

b.makam:

%import a.

bar : a.foo -> a.foo -> prop.
bar Foo Foo.

c.makam

%import a.
%import b.

b.bar a.foo Foo ?

Output:

$ /Users/brendan/dev/makam-error/node_modules/.bin/makam c.makam

	Makam, version 0.7.30


!! Error in file ./c.makam, line 4, characters 1-6:
   Term of type b.a.foo -> b.a.foo -> prop,
   whereas expected a type of form a.foo -> A -> prop.

Interestingly, removing %import a. from b.makam results in a successful run with Foo := a.foo., but that means that you can't run/test/import b.makam independently.

Infix only expressions look rather lispy:

ifte (is_simple Tx) (eq T Tx) (eq T (ref P))

It would be cool to have custom infix operators, so you could write something like

ifte (is_simple Tx) (T = Tx) (T = (ref P))

Currently it looks like that there's only * and ::.

I very well may be doing something wrong here, but basically I am struggling with extending the syntax theory:

%extend syntax.
followed_by: syntax A -> syntax B -> syntax A.
(*inline (followed_by _ _).*)
rule (followed_by P Follow) (apply cons [syntax.captured P, Follow]).
%end.

leads to

!! Error in file ./src/syntax.makam:7:67-68:
   Variable nil with type syntax.syntax_args (list A -> list A) A does not exist.

Interestingly modifying the stdlib itself leads to the same problem.

Makam version: 0.7.40

If I change the order of the c rules, the query works, but with this order, the second time it tries to solve the query c X, it no longer has the rule b 3 in scope.

a, b, c : int -> prop.

a X :-
    (b 3 ->
        c X).

c 2 :- print "2", refl.rules_get b L, print L, refl.assume_get b LL, print LL, b 3.
c 4 :- print "4", refl.rules_get b L, print L, refl.assume_get b LL, print LL, b 3.

(a X, eq X 4) ?
(*** Result
"2"
[ clause (b 3) success ]
[ clause (b 3) success ]
"4"
[  ]
[  ]
Impossible.
*)

When delayed higher-order unification problems remain unsolved, it would be useful to see the remaining constraints in the REPL.

Currently, asking a query such as eq (F 5) 5 ? gives back

Yes:
F := F.

There is no indication that there are still delayed unification problems.

For prior art on this, asking a similar query in Twelf, Teyjus, or ELPI with -delay-problems-outside-pattern-fragment, they all give a list of remaining constraints (or "disagreement pairs" for Teyjus).

!! Error in file ./doc/razbor.makam, line 1, characters 1-11:
   File list.makam not found (searched: [./doc/list.makam; /home/suhr/.npm-packages/lib/node_modules/makam/list.makam; /home/suhr/.npm-packages/lib/node_modules/makam/stdlib-cache/list.makam]).

While trying to import with %use list.

There's list.makam in /home/suhr/.npm-packages/lib/node_modules/makam/stdlib/. But there's no list.makam in /home/suhr/.npm-packages/lib/node_modules/makam/stdlib-cache/:

% ls -1 /home/suhr/.npm-packages/lib/node_modules/makam/stdlib-cache
1023965001.makam-cache
1098923814.makam-cache
1152327979.makam-cache
1406994528.makam-cache
1526945188.makam-cache
1584950368.makam-cache
1805749169.makam-cache
1845788431.makam-cache
1947437720.makam-cache
1954381117.makam-cache
910116983.makam-cache
990541764.makam-cache

Makam version: from npm.

    tests : testsuite.
    %testsuite tests.

    >> eqv 1 X ?
    >> Yes:
    >> X := 1.

$ makam error --run-tests

	Makam, version 0.7.31


!! Error in file ./error.makam, line 4, character 5:
   Parse error.

Ran into this issue when trying to put tests in a namespace!

Under the experimental/examples there's an issue with the call by need strategy.

In particular, in the evaluation rule for the app we introduce a local variable thunk that we'll use to simulate the call by name part of call by need, and a new clause stating how to evaluate this variable. Using memoized to implement sharing.

The problem is that the value V might be a lambda abstraction, with appearings of the new variable. In this case we would need to provide a global variable instead of a local one. I'm not completely sure if there's an idiomatic way to do this on Makam (or if it's even possible).

Example of failure:

If we execute the code as is, evaluating it prints:

-- Query result in file ./examples/experiments/stlc_strategies.makam, line 63, character 2 to line 66, character 71:
cbv eval
"evaluation"
tuple [ (tuple [  ]), (tuple [  ]) ]
cbname eval
"evaluation"
"evaluation"
tuple [ (tuple [  ]), (tuple [  ]) ]
cbneed eval
"evaluation"
tuple [ (tuple [  ]), (tuple [  ]) ]

If we change the following part ...

for:

(eq TERM (app (app (lam (fun x => lam (fun y => tuple [x, x, y, y])))  side_effect) (tuple [])),
 print_string "cbv eval\n", eval_cbv TERM CBV_VAL, print CBV_VAL,
 print_string "cbname eval\n", eval_cbnm TERM CBNM_VAL, print CBNM_VAL,
 print_string "cbneed eval\n", eval_cbnd TERM CBND_VAL, print CBND_VAL) ?

Evaluating it prints:

-- Query result in file ./examples/experiments/stlc_strategies.makam, line 63, character 2 to line 66, character 71:
cbv eval
"evaluation"
tuple [ (tuple [  ]), (tuple [  ]), (tuple [  ]), (tuple [  ]) ]
cbname eval
"evaluation"
"evaluation"
tuple [ (tuple [  ]), (tuple [  ]), (tuple [  ]), (tuple [  ]) ]
cbneed eval
Impossible.

I think there may be a problem with the way the default implementation of eqv is done.

In particular, unification of the two variables is performed even when the when clause fails.

An easy fix would be to implement it as:

eqv (X : A) Y when not(without_eqv_refl (Z : A)) :-
  eq X Y.

I'm not completely sure this is a bug, but I think is causing me a problem when one of these variables is guarded, then unification is performed, and this may cause an infinite loop (that I explicitely avoid in my own implementation of eqv).

The reason I'm not completely sure is that I tried to come out with a good small example and I couldn't, so maybe the problem is someplace else in my code. Will keep looking.

# step (teach  (tl F)(tb B))  R :- todo.

!! Error in <repl>:3:40:
   Parse error.

But step (teach (tl F) (tb B)) R :- todo. works.

Just ran across this:

%

Produces the following error:

$ makam error --run-tests

	Makam, version 0.7.30


!! Error in file ./error.makam, line 1, character 1:
   Parse error.

This can be annoying if you want to make stacked line comments, like:

% A dependently typed binary data description language, prototyped in Makam!
%
% This is an extension of Martin Löf type theory, with some builtin data types,
% like booleans, integers, and arrays, and support for defining binary format
% descriptions.

I'm guessing this is a result of this rule in the parser, added in #82?

Problem Description

I am not sure if this is the right question to ask but basically I am looking for a way to close an open term. Say, I have the following definitions:

term: type.
succ: term -> term.
argh: term.

The intended mode of use for bindmany.open would be something like this

succeeds: list term -> term -> prop.
succeeds [Arg] (succ Arg).

bindmany.open (bind "n" (fun n => body (succ n))) succeeds ?

which works well. However I want to do the inverse, ie. given Names, XS and Body I want to construct XS_Body.

Attempts

close: list string -> list A -> B -> bindmany A B -> prop.
close Names XS Body XS_Body :- assume_many nameofvar XS Names (apply XS_Body XS Body).

but this does not what I intended (especially that last example):

# binds ["n"] [(N: term)] (succ N) E' ?
Yes:
E' := bind "n" (fun anon7_0_0 => F anon7_0_0),
N := N.

# binds ["n"] [(N: term)] (succ N) (bind "n" (fun n => body (succ n))) ?
Yes:
N := N.

# binds ["n"] [(N: term)] (succ N) (bind "n" (fun _ => body (succ argh))) ?
Yes:
N := argh.

I also tried using bindmany.open XS_Body (pfun XS' Body' => (eq XS XS', eq Body Body')) but to no avail. I guess one could traverse the whole AST, replace each occurence of an X with a concretely named variable and then at the end resolve but it seems like a big hack and a lot of boiler plate.

More Context

Like I mentioned in the beginning I am not sure if I am asking the right question, so I will quickly explain where the problem is coming from. Maybe there is a better approach to solve this issue altogether:

Currently my typechecker is described with a predicate typeof: list predicate -> term -> typ -> prop (Γ ⊢ e : τ) which is working well for regular type inference. My goal is to extend it to typeof: list predicate -> term -> typ -> term -> prop (ie. Γ ⊢ e ⤳ e' : τ) which rewrites the term preserving its type.

As of now the rule for abstraction looks like so:

typeof P (elam XS_Body) (tarrow TS T) :-
  bindmany.open XS_Body (pfun XS Body =>
    assume_many typeof PS XS TS (typeof PS P Body T)).

but it should become something like:

typeof P (elam XS_Body) (tarrow TS T) (elam XS'_Body') :-
  bindmany.open XS_Body (pfun XS Body =>
    assume_many typeof PS XS TS XS' (typeof PS P Body T Body')).

and I am struggling how to make sure XS'_Body' is "XS' => Body'".

The following example shows some kind of problem (as far as I could tell) with how the runtime type checking works (I'm not too sure if this is a bug, or just a misunderstanding from my side)

(eq F (pfun (dyn A) (dyn B) => print "checking in"),
F (dyn 1) (dyn 2), print "done numbers",
refl.typstring F TyF, print TyF, print F,
F (dyn false) (dyn true), print "done booleans") ? 

Which outputs:

"checking in"
"done numbers"
"dyn -> dyn -> prop"
fun ~destruct0 ~destruct1 => newmeta (fun A => newmeta (fun B => and (eq (tuple ~destruct0 ~destruct1) (tuple (dyn A) (dyn B))) (print "checking in")))
Impossible.

If I change the true and false for 3 and 4 it works just fine.

I'll keep trying to narrow what's going on, but my guess is that the (fun A => ...) function is getting (for some reason) globally typed, instead of per application of F.

Specifically: mul and div, max and min, neg and comparisons.

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!

Hi! I've come across a strange issue, where this unification problem fails: a:t -> F (G a) = X. But if X is a ground term, it works.

	Makam, version 0.7.40

# %constraints+.
# t : type.
# x : t.
# eq : t -> t -> prop.
# eq X X.
# test : (t -> t) -> (t -> t) -> t -> prop.
# test F G X :- (a:t -> eq (F (G a)) X).
# test F G X ?
Impossible.

# test F G x ?
Yes:
G := G,
F := F.


Deferred Constraints:
eq (F (G a)) x

I have the latest version from npm.

(This isn't urgent to fix, at least not for my code, I'm just reporting in case it's helpful.)

todo created by @astampoulis

original line:

// TODO: flip the meaning of square bracket notation in types

from commit: bd03309

track progress: http://tododrop.com/todo/84

Right now, makam errors look like this:

!! Error in file ./razbor.makam, line 174, characters 1-12:
   Term of type ty -> ty -> ty -> prop,
   whereas expected a type of form ty -> ty -> ty -> ty -> prop.

But it would be better if they looked like this:

error[E0308]: mismatched types
  --> src/format.rs:52:1
   |
51 |   ) -> Option<String> {
   |        -------------- expected `Option<String>` because of return type
52 | /     for ann in annotations {
53 | |         match (ann.range.0, ann.range.1) {
54 | |             (None, None) => continue,
55 | |             (Some(start), Some(end)) if start > end_index => continue,
...  |
71 | |         }
72 | |     }
   | |_____^ expected enum `std::option::Option`, found ()

(this is annotate-snippets generated error)

Regardless of error formatting, it's important to have <file name>:line:column references, because they can be followed by a text editor.

The last commit in pa_monad_custom was 7 years ago: https://bitbucket.org/camlspotter/pa_monad_custom/commits/

It is impossible to compile on a modern system: omake errors with can not find OMakeroot or Root.om while oasis errors with OASIS format version '0.2' is not supported.

I want to specify the following thing in Makam: https://suhr.github.io/papers/opcalg.html

There's my previous attempt in Prolog (surely incomplete): https://gist.github.com/suhr/b31ae185dcb9ab87cc4208a29f8b2deb

This is my sketch in Makam: https://gist.github.com/suhr/a9bb1ebc517ea22836f5143b9d866181

The problem is, I'm new to HOAS and don't quite know how to specify polymorphic composition and concatenation. I looked at implementation of System F in examples, but it introduces extra terms polylam and polyinst, which purpose I do not really understand (especially polyinst).

I'd like to hear a few advices how to apply HOAS in this context.

The first blog posts are really well written and I would really like to see more content like it. 😁

In my binary data description language I'm trying to specify the binary parsing, and representing a byte stream as a list of integers (not sure if that's a great way to do it or not). In order to implement the decoding of integers it would be really handy to have bitwise operations, like shifting (left and right), bitwise-or, bitwise-and, etc. Not sure how difficult that would be to add to Makam or not though!

There seems to be a problem when mixing guard with unification variable renaming (unifying two unification variables together).

The constraints added by guard are not joined, but rather only one is kept. I'm not sure if this is intended, but it doesn't look like it.

If the problem is just to join constraints together, shouldn't be too big (a complete guess from someone that doesn't understand the whole language).

g : (list A) -> string -> prop.
g A S :-
    guard A (print S).

# (g A "AA", g B "BB", eq A B, eq B []) ?
"BB"
Yes:
B := [  ],
A := [  ].

# (g A "AA", g B "BB", eq B A, eq B []) ?
"AA"
Yes:
B := [  ],
A := [  ].

guardmany_aux defined in:

(guardmany_aux [X] Trigger (print "t") , failure)?

I'll write a PR as soon as I have some time, it doesn't look complicated, but wanted to put it up here.

At the moment I have to write the following:

>> synth (term.function_elim (term.ann (term.function_intro (term.function_intro (term.local 0))) (term.function_type term.universe (term.function_type (term.local 0) (term.local 1)))) term.int_type) Type ?
>> Yes:
>> Type := semantics.value.function_type semantics.value.int_type (semantics.closure [ semantics.value.int_type ] (term.local 1)).

This could be alleviated by some local imports, but it would be really nice to be able to write the following as well:

>> synth (term.function_elim 
>>           (term.ann (term.function_intro (term.function_intro (term.local 0))) 
>>                     (term.function_type term.universe 
>>                                         (term.function_type (term.local 0) 
>>                                                             (term.local 1)))) 
>>           term.int_type) 
>>       Type ?
>> Yes:
>> Type := semantics.value.function_type 
>>              semantics.value.int_type 
>>              (semantics.closure [ semantics.value.int_type ] (term.local 1)).

Something like this: https://lamport.azurewebsites.net/tla/summary-standalone.pdf (not necessary in pdf).