5
$\begingroup$

In order to get acquainted with Lean and programming with dependent types I am trying to implement basic operations for a Vector datatype defined following the example in TPiL as:

inductive Vector (α : Type u) : Nat → Type u
  | nil  : Vector α 0
  | cons : α → {n : Nat} → Vector α n → Vector α (n+1)

I tried implementing an append function to concatenate two vectors as

def append : Vector α m → Vector α n → Vector α (m + n)
  | nil, v => v
  | cons h t, v => cons h (append t v)

but in the nil case I get the error

type mismatch
  v
has type
  Vector α n : Type ?u.1240
but is expected to have type
  Vector α (0 + n) : Type ?u.1240

The type checker apparently can't tell that Vector α n and Vector α (0 + n) are the same type. It works if I instead change the type of append to Vector α m → Vector α n → Vector α (n + m), so that the expected type is Vector α (n + 0). So apparently it can't tell that addition is commutative.

If I do change the type to Vector α (n + m), then later when I use it to implement a function to reverse a vector it fails to type check again:

def reverse : {n : Nat} -> Vector α n → Vector α n
  | 0, nil => nil
  | n' + 1, cons h t => append (reverse t) (cons h nil)

The reason is that on the recursive call it expects reverse t to be of type Vector α 1 and cons h nil to be of type Vector α n' (rather than the other way around) so that the result will have type Vector α (n' + 1) (rather than Vector α (1 + n')). So again the problem is that it doesn't realize that addition is commutative.

What do I have to do to get the type checker to understand that Vector α (m + n) is the same as Vector α (n + m)?

$\endgroup$
4
  • $\begingroup$ The type checker identifies n+0 with n because its by definition of addition, whereas 0+n does not reduce to n. The distinction is that the former equality is definitional, and the latter is semantic. The typechecker cannot decide equality of semantically equal terms, hence also why n+m cannot be identified with m+n. $\endgroup$
    – Couchy
    May 11 at 5:53
  • 2
    $\begingroup$ @Couchy That makes sense, but it's possible to state and prove a theorem that n+m = m+n. Is there any way to use this proof to guide the type checker, for example? $\endgroup$
    – BackusNaur
    May 11 at 15:14
  • $\begingroup$ I believe you can only prove that the two types are propositional equal. Given p of type $n + m = m + n$, the expression congr_arg (Vect \alpha) p will be a proof of that I believe. Unfortunately equality in type theory is more complicated than in informal mathematics. $\endgroup$
    – Merle
    May 11 at 20:15
  • $\begingroup$ @Merle I believe Lean 4 actually has definitional uniqueness of identity proofs (if p : x = x then p = Eq.refl x, definitionally), which sort of annihilates any complications to equality beyond "you have to be explicit about where you substitute equalities". $\endgroup$
    – HTNW
    May 11 at 20:27

1 Answer 1

2
$\begingroup$

Type theories typically have a two notions of equality. There is a "definitional" equality corresponding roughly to syntactic (so "external") equality modulo conversion rules (particularly beta-reduction). There is also a "propositional" equality represented by a type and terms inside the theory (the type family = in Lean). The propositional equality is "really" equality (e.g. you can prove 0 + n = n), and the more restricted definitional equality is what the type checker uses when comparing "expected" and "actual" types (here, it can't show 0 + n is definitionally equal to 0, because the definition of + is such that 0 + n does not reduce/simplify.)

Reflecting propositional equality to definitional equality (i.e. "convincing the type checker" of more equalities) is not possible in Lean, nor most theorem provers, since it makes type checking undecidable. Instead† you have the ability to "rewrite" or "substitute" according to a propositional equality: If you have proved p : x = y and you have a : P x then you can get p ▸ a : P y. That is, you explicitly take your term and "move it" along an equality. The type checker still considers x and y to be different, and p ▸ a is also different from a (unless y is definitionally x and p is definitionally refl, in which case p ▸ a is definitionally a).

Pulling lemmas for 0 + n = n and m + 1 + n = m + n + 1 from the standard library (that these are nontrivial is why the checker isn't trusted with handling them implicitly):

def append : {m : Nat} → Vector α m → Vector α n → Vector α (m + n)
  | 0, nil, ys => Eq.symm (Nat.zero_add n) ▸ ys -- I think ▸ is supposed to handle symming for you when necessary; not sure why it fails here...
  | m + 1, cons x xs, ys => Nat.succ_add m n ▸ cons x (append xs ys) -- outer goal Vector α (m + 1 + n), inner goal Vector α (m + n + 1)

Note that I have to add m to the matching in order to be able to pass it to one of the theorems.

†In actuality you usually have an induction principle for =, which is more general than just substitution. In Lean 4 is a (builtin) macro that uses this induction principle.

$\endgroup$
1
  • $\begingroup$ Thank you, this works and is exactly what I was looking for. The information I was missing was the existence of the rewrite operator. $\endgroup$
    – BackusNaur
    May 13 at 22:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.