function_type naming

[tinyplasticgreyknight]

It's a bit confusing that the names of function_type (node 38) and lambda (node 44) don't match up in the way that e.g. int64_type/int64_value do.

There are two points to consider:

• should the canonical name for node 38 be lambda_type?
• should the canonical name for node 44 be lambda_value?

In my opinion, the first answer would be "yes", but I'm more ambivalent about the second. Certainly it would be the most consistent, but you mentioned that it would look a bit strange since lambda is a binding construct, and I see your point.

On the third hand, since the names aren't strictly speaking part of the format, perhaps consistency should win out?

[tinyplasticgreyknight]

Vaguely related, couldn't you consider the type of a lambda to be just an ordered pair of types? I don't know if that really helps with anything.

[IreneKnapp]

Well, if you use a more-generic type for lambdas, then you can't know by looking that they can be applied. It probably is possible to build a consistent type theory where anything that "looks like a function" can be treated as one, but I'm not aware of work in that direction and I don't think it would serve a useful purpose.

(I've never actually written the type theory axioms for Modern Data, since they're not too far from standard, but I plan to at some point; I think it's important to have in an appendix somewhere for users who want to reason about the system's properties.)

Let's make both of these changes. If the notion for keeping node 44 as "lambda" were that binding constructs get simpler names than everything else, then node 38 should never have been "function_type" to begin with, since, in fact, it also introduces a binding. The other binding constructs, of course, are "let" and "type_family", and their names are each already kind-of one-offs, so I don't think trying to be consistent with them makes sense.

So in summary:

• Node 38 should be lambda_type
• Node 44 should be lambda_value

I'll leave the issue open because, actually, I can't publish my own changes until I get sign-off from my employer! I kept ownership of this code from before I joined them, but for work on it going forward, since I like working for them it's easier if I do things their way. I'd better begin that process. :)