failed to compile: could not prove that type is nonempty

Stream: new members

[JJ]

I've got a little implementation of the untyped lambda calculus w/ de Bruijn indices here. I am getting an error I really don't understand: for some reason, Lean is worried about the type of my eval function being uninhabited. What does this mean, and how can I resolve this error?

-- import NbE.Stack
-- Some helper definitions / notation to make backward indexing into Arrays a little easier.
namespace Array
  def teg (a : Array α) (n : Fin a.size) : α :=
    a[a.size - n - 1]
  notation a "[^" n "]" => teg a n

  -- We must explicitly check n < a.size as subtraction on Nat bottoms out.
  def teg? (a : Array α) (n : Nat) : Option α :=
    if n < a.size then a[a.size - n - 1]? else none
  notation a "[^" n "]?" => teg? a n
end Array

-- A declaration of the Stack type, and exposed associated methods.
def Stack := Array
namespace Stack
  def push (s : Stack α) (x : α) : Stack α := Array.push s x
  def peek? (s : Stack α) : Option α := Array.back? s
  def peekn? (s : Stack α) (n : Nat) : Option α := Array.teg? s n
end Stack

def Index := Nat
deriving ToString, BEq
instance : OfNat Index n := ⟨n⟩

-- The untyped lambda calculus, with lookups by de Bruijn indices.
inductive Expr where
| abs (body : Expr)
| app (func arg : Expr)
| var (idx : Index)
deriving BEq

instance : ToString Expr := ⟨toString⟩
where toString
| .abs body => s!"(λ {toString body})"
| .app func arg => s!"{toString func} {toString arg}"
| .var idx => s!"{idx}"

mutual
  inductive Value where
  | clos (body : Expr) (env : Array Value)
  | ntrl (neutral : Neutral)
  deriving BEq

  inductive Neutral where
  | nvar (idx : Index)
  | napp (func : Neutral) (arg : Value)
  deriving BEq
end

mutual
  def toString_Value : Value -> String
  | .clos body _ => s!"λ {body}"
  | .ntrl neutral => toString_Neutral neutral
  def toString_Neutral : Neutral -> String
  | .nvar idx => s!"{idx}"
  | .napp func arg => s!"{toString_Neutral func} {toString_Value arg}"
end

instance : ToString Value := ⟨toString_Value⟩
instance : ToString Neutral := ⟨toString_Neutral⟩

-- The environment is a stack of values, bound up the call stack.
-- These values are looked up by de Bruijn indices.
def Env := Stack Value

-- Error: failed to compile 'partial' definition 'eval.eval'
--  could not prove that the type Expr -> Env -> Value is nonempty
partial def eval expr := eval expr #[]
where eval (expr : Expr) (env : Env) : Value :=
  let apply func arg :=
    match func with
    | .clos body env => eval body (env.push arg)
    | .ntrl neutral => Value.ntrl (.napp neutral arg)
  match expr with
  | .abs body => Value.clos body env
  | .app func arg => apply (eval func env) (eval arg env)
  | .var idx => env[^idx]?.getD <| Value.ntrl (.nvar idx)

namespace examples
  local notation "λ" body => Expr.abs body
  local notation func arg => Expr.app func arg
  instance : OfNat Expr n := ⟨Expr.var n⟩
  def a : Expr := λ (λ 1 (λ 1)) (λ 2 1)
  def b : Expr := Expr.abs <| .app (.abs <| .app (.var 1) (.abs (.var 1))) (.abs <| .app (.var 2) (.var 1))
  #eval eval a
  #eval a == b
end examples

(feedback on code style would be appreciated, too. i have a separate searchable topic at #new members > nice way to implement instances on mutually defined types? for a particularly ugly part.)

[Aaron Liu]

What is the type of your eval function? It's not obvious just looking from the code.

[Johannes Tantow]

Add

instance : Inhabited Value where
  default := .ntrl (Neutral.nvar Nat.zero)

[JJ]

Aaron Liu said:

What is the type of your eval function? It's not obvious just looking from the code.

It's Expr -> Value, but the issue is in the where eval function, which is Expr -> Env -> Value.

Johannes Tantow said:

Add

instance : Inhabited Value where
  default := .ntrl (Neutral.nvar Nat.zero)

Thanks, this worked! Would you mind explaining what the issue was?

[JJ]

I don't see any place where I need the type system to provide a default Value.

[Aaron Liu]

consider

partial def whoops (n : Nat) : Empty := whoops (n + 1)

[Aaron Liu]

clearly this is unsound

[JJ]

Hm. But in every case but one (apply invocation into eval) I'm returning a new constructed Value, so I don't know why the compiler is having trouble.

[JJ]

It does look like the problem is specifically .clos body env => eval body (env.push arg). That's weird. It's operating on the destructured components body and arg, so idk the problem exactly. Mostly though idk why providing a default value with inhabited is useful?

[Aaron Liu]

JJ said:

Hm. But in every case but one (apply invocation into eval) I'm returning a new constructed Value, so I don't know why the compiler is having trouble.

inductive InfiniteList (α : Type u) where
  | cons (x : α) (xs : InfiniteList α) : InfiniteList α

partial def natsFrom (n : Nat) : InfiniteList Nat := .cons n (natsFrom (n + 1))

theorem InfiniteList.false {α : Type u} (xs : InfiniteList α) : False := by
  induction xs with
  | cons _ _ ih => exact ih

[Aaron Liu]

you are providing a new constructed value each time

[Aaron Liu]

but it's still unsound

[JJ]

Damn, Lean lets you write that inductive??

[JJ]

Huh. Interesting, thanks.

[Violeta Hernández]

JJ said:

Damn, Lean lets you write that inductive??

It's the smallest type closed under all the constructors, which is of course the empty type.

[Ruben Van de Velde]

Empty types are not forbidden :)

[JJ]

Sorry, I'm still really confused by this, I think.

[JJ]

The inductive Value is obviously inhabited. The simplest way to show this is that Value.ntrl (Neutral.nvar 0) is a term of type Value, which I guess we're doing with the Inhabited typeclass instance. But even adding an extra Value.x constructor still gives the same error on the eval function... I guess because it wants the type Expr -> Env -> Value to be nonempty?

And why can't Value be Empty? What'd be wrong with that? This is in a partial def, after all.

[Kyle Miller]

Here's a rule-of-thumb with Lean's inductive types: data is built from smaller data (more specifically, for recursive types). It's not possible to construct anything for InfiniteList because if you look at it, you could only have infinite lists, so cons would be storing a list of the same size as the list it's building, which isn't possible — it needs to be smaller.

[Kyle Miller]

The reason Value is not allowed to be empty is that when you define a partial definition, it's basically adding an axiom to the environment, and Lean wants to be sure you're not adding a contradiction to the environment. (It's not actually an axiom, but an opaque definition, which needs proof that the type isn't empty.)

[Kyle Miller]

If you try doing

opaque bad : Empty

you can see that lean complains that it can't synthesize Inhabited Empty. That's a safeguard that axiom bad : Empty doesn't do.

[Kyle Miller]

While partial definitions can't be unfolded, they're still values that "exist" mathematically, so you need to be sure that the value really could exist, otherwise you can prove false things.

[Kyle Miller]

Since your eval is partial, it's worth pointing out that this is not a definition you can prove anything about, in case matters to you. You can still #eval it of course.

[Kyle Miller]

Just to reiterate the key point: if you make a partial definition, theorems are allowed to refer to it, so it had better not be a definition whose type is an empty type. That's a contradiction.

[Kyle Miller]

It's possible to prove some things about partial definitions. Lean assumes that, mathematically, every function terminates, so even though we've got this non-terminating foo, after it "runs forever" it will "return" some definite value. (This is all in quotes because nothing's actually being run. We're in math land.)

The value of foo n is evidence that the return type is nonempty. Lean insists on a proof ahead of time that the return type is nonempty, that way this evidence of nonemptiness is not new information.

instance : Inhabited { m : Nat // m = 1 } := ⟨⟨1, rfl⟩⟩

partial def foo (n : Nat) : { m : Nat // m = 1 } := foo (n + 1)

example (n : Nat) : (foo n).val = 1 := by
  cases foo n
  simp_all