Cleaner syntax?

[VictorTaelin]

I've written an alternative parser for Morte with less symbols using binder:type body for λ, binder-type body for ∀. If you ignore λ's, ∀'s and arrows, and allow empty binders, you get something quite similar. For example, Zero, which currently is λ(a : *) → λ(succ : a → a → a) → λ(zero : a) → zero, could be written as λ a : * -> λ succ : (-a -a a) -> λ zero : a -> zero. But you can also drop those symbols and add line breaks:

a: *
succ: -a -a a
zero: a
zero

Another example, List.map:

u: *          # from type
v: *          # to type
f: -u v       # function to map
l: (List u)   # mapped list
a: *          
cons: -v -a a 
nil: a        
(l a (h:u (cons (f h))) nil)

IMO that looks cleaner.

[VictorTaelin]

Okay, from feedbacks, this might be way too lightweight, so, what about this?

-- Polymorphic types
Type a => 
Type b =>

-- Function arguments
(a -> b) func =>
(List a) list =>

-- Church-encoding of returned value
Type r => 
(a -> r -> r) cons => 
a nil =>

-- Returned value
(list r (a head => cons (func head)) nil)

Basically the same, but using -> for types and => for functions, allowing to drop the unicode for λ and ∀ and the noisy : symbol.

PS: I'm aware Morte isn't meant to be used directly, but people often do it for practice etc. - no need for them to suffer more than they already should...

[VictorTaelin]

(@paulotorrens)

[Gabriella439]

I think the main issue with this syntax is that whitespace is overloaded to mean two separate things:

• function application
• separating the bound variable name from its type

I think it's best to avoid using the same syntax for two separate language features

For example, it's not obvious to me what would be the syntax tree generated for this source code:

a b c => d e f => g h i

[VictorTaelin]

@Gabriel439 the same is true for (x : T) -> b, no? The rule is => has precedence, though. a b c => d e f => g h i would be parsed as: a (b c => (d (e f => (g h i)))). Here is a demo parser:

const parse = code => {
  let s = "(" + code + ")";
  let i = 0;
  const parseBind = () => {
    let parses = [];
    while (s[i]) {
      while (/\s/.test(s[i])) {
        ++i;
      };
      if (/\w/.test(s[i])) {
        let word = "";
        while (s[i] && /\w/.test(s[i])) {
          word += s[i++];
        }
        parses.push(["Var", word]);
      } else if (/\(/.test(s[i])) {
        const term = (++i, parseBind());
        parses.push((++i, term));
      } else if (/(=>|->)/.test(s.slice(i,i+2))) {
        const bind = parses.length > 1 ? parses.pop() : ["Var", ""];
        const type = parses.pop();
        parses.push([s.slice(i,i+=2) === "=>" ? "Lam" : "All", type, bind, parseBind()]);
      } else if (/\)/.test(s[i])) {
        break;
      }
    };
    return parses.reduce((parse, result) => ["App", parse, result]);
  };
  return parseBind();
};

const stringify = term => {
  const wrapIf = ([tag, str, wrap], cond) =>
    (cond(tag) ? wrap : (x => x))(str);

  const go = term => {
    switch (term[0]) {
      case "Var":
        return [term[0], term[1], x => x];
      case "App":
        const fun = wrapIf(go(term[1]), tag => !/App/.test(tag));
        const arg = wrapIf(go(term[2]), tag => true);
        return [term[0], fun + " " + arg, x => "(" + x + ")"];
      case "Lam":
      case "All":
        const type = wrapIf(go(term[1]), tag => true);
        const bind = wrapIf(go(term[2]), tag => true);
        const body = wrapIf(go(term[3]), tag => !/(Lam|All)/.test(tag));
        const spac = bind.length > 0 ? " " : "";
        const arrw = term[0] === "Lam" ? " => " : " -> ";
        return [term[0], type + spac + bind + arrw + body, x => "(" + x + ")"];
    }
  };
  return wrapIf(go(term), tag => !/(Lam|All|App)/.test(tag));
};

const print = x => console.log(stringify(parse(x)));

//const code = "(Type Nat => ((Nat x -> Nat y -> Nat) A B C) succ => Nat zero => zero) X";
const code = "a b c => d e f => g h i";

print(code);

Note I'm posting this just for inspiration! Morte can have different syntaxes, no need to change the existing project.