prefix type ascriptions

Stream: general

[Kyle Miller]

Sometimes I've thought a type ascription or cast could be clearer in certain cases if the type came at the beginning rather than at the end like in (x : t). I know show t, from x exists, but it's rather long in comparison, and I don't find it to be very mnemonic for things that aren't proofs. Borrowing an idea from common lisp, a possible alternative is the t, x.

notation `the `:0 y `, ` x:0 := (x : y)

This isn't anything like a serious proposal. I just thought I'd mention it in case it's interesting to anyone, or in case anyone has other ways of writing the type first.

For example, as a prefix it acts more like a coercion operator:

def foo {α : Type*} (x : α) := the option α, x

Of course, there's no need for new notation for this:

def the (α : Type*) (x : α) := x

def foo {α : Type*} (x : α) := the (option α) x

However, it's sort of nice how notation lets you avoid additional parentheses in both the type and the term.

def foo' := the ℤ, 17 + 20

[Kyle Miller]

(In the realm of mnemonic notation, it seems that $ can generally be pronounced as "of", and if one wanted it'd make a reasonable notation:

notation f ` of `:1 a:0 := f a

This goes against a quasi-rule, though, that infix notation should contain non-alphanumeric symbols.)

[Eric Wieser]

Note that show has different elaboration rules to :, and can prevent lemmas matching if part of the statement.

[Mac]

Kyle Miller said:

Sometimes I've thought a type ascription or cast could be clearer in certain cases if the type came at the beginning rather than at the end like in (x : t).

It is important to note that having the type after the term/variable is not purely a stylistic decision. As Lean has dependent types, the type of a declaration has to come after its parameters and the binders keep this ordering for consistency's sake.

-- ex: the parameter needs to precede the `def`'s type
def paradox (p : P) : ~P := ...
-- without a parameter, the signature looks much like a binder
-- thus, binders and type ascriptions follow this order as well
def foo : Int := (0 : Nat)

[Kyle Miller]

@Mac It seems you think I'm suggesting replacing :? I only mean to suggest that every once in a while readability can be improved if the type comes first, and this a possible way to accomplish it.

Also, what does dependent types have to do with this? other than the fact that in dependent type theory there's a x : t convention? In each binder, neither the variable nor the type can refer to each other, so they could reasonably come in either order. I follow you as far as there being many benefits to having so-called "duality of syntax" where conceptually related things are written the same way.

[Mac]

Kyle Miller said:

I follow you as far as there being many benefits to having so-called "duality of syntax" where conceptually related concepts are written the same way.

That was pretty much my whole point. The reason the type comes after a variable in a binder or ascription is so it mirrors the fact that the type comes after a signature in a declaration (the later of which is necessary because of dependent types).

[Eric Wieser]

I dispute the claim that dependent types impose a restriction on the order of the grammar

[Eric Wieser]

Why couldn't we have

def the vector n 3, of_zeros (the ℕ, n) := ...

[Eric Wieser]

I'm not saying it's better, but I don't see where the requirement that variables are introduced to the left of their use comes from

[Mario Carneiro]

In some ways it makes more sense to have \lam (the T, x), e from a binding structure point of view since x binds in e but not in T; putting the variable after the type means that you can add x to the context reading strictly left to right without having to skip over T. (In some languages, the lambda is represented internally as lam T (x. e) to make this binding structure explicit.)

[Eric Rodriguez]

I think what Mac was saying is that we can't have c++ style signatures for things due to dependent typing (i.e. no a^n + b^n ≠ c^n theorem flt (a b c : ℕ) (hc : c ≥ 2) (h : a*b*c ≠ 0)). But I agree with everyone else, I think this notation is nice.

[Kyle Miller]

@Mac One could argue that type ascription notation is backwards for dependent type reasons, and having it is a concession to "duality of syntax." You can't write the function def the (α : Type*) (x : α) := x with reversed arguments.

This might explain why every once in a while there's an expression where I feel like I'd rather put the type first.

[Mac]

I agree with everyone here that type ascriptions in the reverse order (i.e., the Nat x or, what I would like, just Nat x or Nat(x)) are useful, and, as @Kyle Miller pointed out, more logical with respect to dependent type theory. I was simply noting the logic behind not doing them that way is likely for "duality of syntax". Since types have to be written after the main signature a def for DTT, they are as written such in other places (bindings, type ascriptions, etc.) as well.

[Kyle Miller]

@Mac Sorry I'm still pulling on this thread about your claim that "as Lean has dependent types, the type of a declaration has to come after its parameters." In DTT, every term has a well-defined type, so there's no need for a type in a declaration. Imagine a bizarro-Lean where terms come after the type in a type ascription. Then this would be a valid way to write a definition:

lemma const (Prop : p q) := p → q → p : λ h _, h

This also has the nice property that you are able to see the type near the :=

[Kyle Miller]

(One problem with Nat x is that pi types have an evaluation rule in Lean, so you wouldn't be able to distinguish that kind of evaluation from a type ascription. You could get Nat(x) to work if you make whitespace significant, making Nat (x) parse differently.)

[Mac]

@Kyle Miller fair enough -- it would be more accurate to say that, if a declaration it has an explicit type, it has to come after its parameters. Also I would argue that, technically, that type still is coming after its parameters (just, in that case, in the body of the definition :laughing: .

[David Thrane Christiansen]

In addition to Common Lisp, Idris also uses the for type ascription, and it's defined as the Identity function with an explicit type argument.

[Eric Wieser]

I think that's exactly what show is defined as?