Infix expressions

[suhr]

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 ::.

[astampoulis]

Hi @suhr,

From my perspective, infix expressions for predicates are not as useful in λProlog as in other languages -- for example, predicates corresponding to standard binary operations such as + have three arguments instead of two, so infix notation does not really apply. Instead, custom mixfix notations (a la Agda) could be more useful (where notation for addition could look like _ + _ = _).

Still, supporting custom syntax is a change that is outside what I would like to add to the core of Makam, as I am mostly focusing on additions that can be implemented within Makam, rather than changes to the existing core itself. (A long-term goal is bootstrapping a new core.) Custom syntax is most typically useful for object languages, for which completely customizable parsers can be built using the syntax or peg libraries.

Of course, some special syntax is useful for making some very common things more readable, such as lists, tuples, and the standard predicates (e.g. and, ifte etc.). I'm happy to add more of those if they can help with readability. In particular:

• for ifte, you can use standard if P then Q else R notation
• for eq I have considered adding syntactic sugar (something like a = b as you suggest), but have been reluctant to do so. I had previously found that that kind of syntax misdirected people to think that eq is somehow more fundamental to the core of Makam than it is. So I would opt for syntax like a ~ b instead.

[brendanzab]

One place I found the lack of operators annoying was here:

    readback Length (local Level : neutral) (local Index) :-
        % Convert De Bruijn levels to De Bruijn indices using the following
        % arithmetic (this is a bit awkward to express in Makam):
        %
        % ```
        % Index = Length - (Level + 1)
        % ```
        plus 1 Level Level1,
        plus Level1 Index Length.

It might also benefit from function-style predicates like in Mercury to be truely useful though. I'd also be worried about things turning into operator soup like in Agda - a nice thing about Makam is that it forces you to come up with names for predicates!

[suhr]

It may be possible to construct a Prolog style evaluator that allows to write something like is Index (Length - (Level + 1)).

Though functional syntax sugar like in Ciao might be indeed sometimes useful.

a nice thing about Makam is that it forces you to come up with names for predicates

I believe predicates are often better named, the syntax is better with unicode infix operators and for functions it depends.

Anyway, it's great to have a choice.