consolidate nomenclature

[jonsterling]

We should make sure that the code is unified in its use of terminology (e.g. classifier vs. type, etc.). I'm fine with choosing any scheme of names...

But I wanted to propose an alternative scheme that might make more sense from the perspective of syntax:

1. "Classifiers" should be called arities.
2. "Base classifiers" should be called sorts.
3. "Substitutions" should be called something other than substitution; maybe spine, but perhaps something else would be clearer? I have no real preference.
4. Finally I am not sure what to say about "term" and "atomic term". Any thoughts?

[jonsterling]

For what it's worth, Jason Reed avoids the term "spine" and uses "substitution" instead, because these associate in the opposite way that people typically expect for spines. So, we might consider avoiding that term too—I just think "substitution" may be a little confusing for our intended audience / users.

[jonsterling]

We should also not use the symbol => for pi types, since this is apparently meant to be used for something else in racket.

[david-christiansen]

What about all?

[david-christiansen]

Lambda could be called bind in this regime.

[david-christiansen]

with might be an OK name as well

[jonsterling]

@david-christiansen 👍 to bind; to my ears, all sounds too logical, whereas we should find something that seems "syntaxy" or algebraic, I think. Would be good to also have something that looked good for non-dependent bindings.

[david-christiansen]

Good point. What about using for pi?

[jonsterling]

using is all right; might be a little too cute, but I'm not opposed to it.

[david-christiansen]

Here's a few more: take, with, binder, vars

[jonsterling]

Heh, I kind of like binder or vars. Seems very intuitive... My only concern is that using a word could make it a little hard/dense to read signatures, but maybe we want to provide special notations for those anyway, not sure.

[jonsterling]

For an ascii-art version, maybe we should reuse the notation of Martin-Löf's arities, ->>. Not sure if it's too confusing in combination with the other notations we have, like the "turnstile" >> (which maybe we should just write !-).

[jonsterling]

[realized I left a few words out of my last comment, updated in case you are looking at the email notification. I mean the idea of ->> as a proposal, not a recommendation.]

[emberian]

So vars for =>, bind for lam?

[jonsterling]

Definitely bind for lambda (which is currently written Λ); I'm not completely convinced about the other one, but feel free to do it.

[jonsterling]

Maybe $ should be named var or meta; in the LF calculus it is application, but when I think about how it would be used in practice by real users, it's to instantiate a (meta)variable. @david-christiansen what do you think?

[emberian]

Hm, Recognized specially within forms like cond. A => form as an expression is a syntax error.. Is it a big deal to re-use it here? Maybe...

[david-christiansen]

It means that client code can't use that version of cond together with our library, which is a pain, and it turns "missing import" errors into confusing syntax errors. So I think we should use something else.

I think var and meta say "introduce a meta", not "elim a meta". What about subst?

[david-christiansen]

Or plug?

[jonsterling]

Plug kind of makes sense! I like it better than subst, since we still need ordinary subst of variables.

On Jul 4, 2017, at 7:44 PM, David Christiansen notifications@github.com wrote:

Or plug?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[emberian]

I don't suppose we could just use... \Pi?

[emberian]

Maybe ==>?

[david-christiansen]

There's two downsides to \Pi:

1. It makes it confusing or impossible to implement a PRL with a pi type, and we expect them to usually have pi types.
2. It risks confusing the LF function space with the more powerful dependent function spaces of languages like Idris.

The LF operators are really more like syntax with binding and metavariables than they are like programs, and we want this distinction to be apparent.