Instantiating constructor into application position does not work intuitively

[Quelklef]

(App f x) = (f x)
(Succ x) = (+ x 1)
(Main) = (Pair (App Succ 0) (App @x(Succ x) 0))

This HVM code reduces (Main) to (Pair ((Succ) 0) 1). I would intuitively expect (Pair 1 1).

My understanding for this is that in (App Succ 0), the expression Succ is actually shorthand for (Succ), so we have (App (Succ) 0) which reduces to ((Succ) 0) which does not reduce.

Would this be considered an issue, or just a gotcha for newcomers?

[Quelklef]

The rule for nullary constructors C that writing C == (C) is surprising to me, and is essentially the root of my intuition being wrong.

What's the reason for this rule? HOW.md doesn't seem to provide explanation. My guess is that having all constructors be applications (of arity ≥0) makes implementing rewrite rules somehow easier, but I don't want to assume.

[VictorTaelin]

That isn't an issue, but that's definitely confusing for newcomers. Global definitions must be seen as functions, and they need to be "called" to retrieve the right-hand side. So, in your example, ((Succ) 0) is applying Succ to 0 arguments, but it has 1 argument, so it won't reduce. That is why you need to curry it as λx(Succ x). This may help visualizing it:

Uncurried (correct)

(Foo a b) = (+ a b)
(Main) = (Foo 1 2)

Foo is a 2-argument function. (Foo 1 2) calls it with 2 arguments. Fine.

Curried (correct)

(Foo) = λa λb (+ a b)
(Main) = ((Foo) a b)

Foo is a 0-arguments function that returns a curried lambda. (Foo) calls it with 0 arguments, returning that curried lambda, which is then applied to 2 arguments. Fine.

Curried (wrong)

(Foo a b) = (+ a b)
(Main) = ((Foo) 1 2)

Foo is a 2-arguments functio. (Foo) calls it with 0 arguments. That is wrong.

Uncurried (wrong)

(Foo) = λa λb (+ a b)
(Main) = (Foo 1 2)

Foo is a 0-arguments function. (Foo 1 2) calls it with 2 arguments. That is wrong.

---

Why not make everything curried?

Uncurried functions are much faster. HVM is a global graph-rewrite machine that replaces left-hand sides by right-hand sides. Because of that, and unlike Haskell (that compiles functions to bytecode), HVM functions must alloc the right-hand side whenever they are called. This is required for fusion, beta-optimality, parallelism, etc. But that also means a definition like:

(Add a b) = 
  let succ_case = λpred (Add pred b)
  let zero_case = b
  (NatCase a succ_case zero_case)

Will alloc more data than a definition like:

(Add (Succ pred) b) = (Add pred b)
(Add Zero        b) = b

Because the right-hand sides are smaller. Splitting otherwise big function bodies into small function bodies through a Haskell-like equational notation is one of the main reasons HVM is much faster than previous optimal evaluators, so, if everything was curried, we'd get a substantial real-world impact on performance. A user-facing language that compiles to HVM (like Kind, Haskell, etc.) may still be fully curried, though, and use n-ary functions as a compile-time optimization, breaking case-trees into smaller rewrite rules!

[Quelklef]

Global definitions must be seen as functions, and they need to be "called" to retrieve the right-hand side

I'm fine with that; it makes sense to me that ((Succ) 0) does not reduce. My question is more like, why is (App Succ 0) parsed as (App (Succ) 0)? Why is there no way to manipulate using constructors directly?

[VictorTaelin]

@Quelklef hmm what would Succ parse as? Perhaps a neat idea would be to lookup the definition of Succ and add the lambdas (like, if Succ has two arguments, we parse it as λx λy (Succ x y)?). But anyway, HVM has lambdas, variables and constructors. Uppercase is used for constructors (not variables), so Succ couldn't mean anything other than a constructor with no arguments. Right?

[Quelklef]

HVM has lambdas, variables and constructors

Okay, I poked around language.rs, and figured out where my mental model is wrong.

Consider the two HVM expressions (F x) and (f x).

These two expressions parse very distinctly, something like Ctr F [ Var x ] and App (Var f) [ Var x ].

The expressions appear very similar, and I had assumed that they would parse more similarly. Something like, App (Symbol F) [ Var x ] and App (Var f) [ Var x ].

The crucial difference here is that I've given constructor names their own ast node type Symbol. If constructor names had their own AST node, then instantiations like (f 0)[f := Succ] could produce (Succ 0) instead of ((Succ) 0).

This would, of course, brings about difficulties regarding currying. Rewrite rules like (Apply2 f x y) = (f x y) would have to decide ahead-of-time if (f x y) is to be a curried call or not depending on if f is expected to be instantiated with a constructor name or with a λ-term.

Conceptually, constructors and λ-terms are similar: with both the definition (Succ) = λx. (+ x 1) and (Succ x) = (+ x 1), I think of Succ as "representing the same thing". It looks like in HVM this is mistaken, as constructors and λ-terms are meaningfully different.

They could, in theory, be unified, by giving constructor names an AST node, but I leave that decision to you. If they are to be kept distinct, I would suggest that App and Ctr use different syntax to make it more clear that they are distinct.

[VictorTaelin]

Yep, they could be unified, but then the optimizations above wouldn't apply; the de-unification is what made HVM so fast to begin with. Initially they had different syntaxes (constructors used []), but we found it aesthetically unappealing, so we used uppercase to distinguish. I can see how this caused confusion, though. Honestly not sure what the best option is, but these definitely are separate concepts. Thanks for the summary, hope it helps other readers.

[nmushegian]

Initially they had different syntaxes (constructors used []), but we found it aesthetically unappealing, so we used uppercase to distinguish. I can see how this caused confusion, though. Honestly not sure what the best option is, but these definitely are separate concepts.

FWIW I think the [] is a good choice because it has connotations like 'this is data', and while using lettercase for semantics is not the most offensive thing in the world, it is a bit harder to see what is happening at a glance.
This was the first thing I thought of for a language frontend (other than implied parens on top-level term expression)