How to erase type?

Stream: new members

[Jakub Nowak]

I have a type that is used only to provide proof of well-foundness. I was thinking whether it's possible to not store unnecessary data during runtime somehow.

#mwe :

inductive Tree : Type 1 where
| leaf : Tree
| node : {ι : Type} → (ι → Tree) → Tree

def Path : Tree → Type
| .leaf => Unit
| @Tree.node ι f => (i : ι) × Path (f i)

def t {α : Type} : Tree := .node (fun (_ : α) => .leaf)

def ex {α : Type} [Inhabited α] : Path (@t α) := ⟨default, ()⟩

I want to not store (i : ι) in instances of Path. In other words, I would want runtime representation of Path to be similar to that of non-optimized Nat.

I've tried using docs#Erased somehow, but either I'm not using it correctly, or it's not possible.

An actual code is: #new members > Stuck on ManyT in "Functional Programming in Lean" @ 💬. It's not a big deal in this particular case, I was just pondering whether I can get closer to the unsound implementation in #new members > Stuck on ManyT in "Functional Programming in Lean" @ 💬 .

[Mirek Olšák]

You could possibly use Prop instead of Type, that is not passed in computation.

[Mirek Olšák]

A Type can be collapsed into Prop with Nonempty, but I would need to think if it suits your use case.

[Mirek Olšák]

Could this be what you want? It entirely erases any data from Path

inductive Tree : Type 1 where
| leaf : Tree
| node : {ι : Type} → (ι → Tree) → Tree

def Path : Tree → Prop
| .leaf => True
| @Tree.node ι f => ∃ (i : ι), Path (f i)

def t {α : Type} : Tree := .node (fun (_ : α) => .leaf)

def ex {α : Type} [Inhabited α] : Path (@t α) := ⟨default, trivial⟩

[Jakub Nowak]

Hm, but now you made entire Path a Prop. I want Path to still have a runtime representation. As an example, I still want this to be possible:

def Path.length : {t : Tree} → Path t → Nat
| .leaf, _ => 0
| .node .., ⟨_, p⟩ => p.length.succ

[Jakub Nowak]

I kinda want a sigma pair like ∃ (i : ι), Path (f i), or (i : ι) × Path (f i), for which its first component can only eliminate into Prop, while second component can be accessed in Type context too.

[Jakub Nowak]

The problem with Erased I had, was that Lean didn't accept function as computable when the types where noncomputable. Maybe it's a dumb question, but shouldn't this be allowed? Computability is only about compilation, and the types aren't compiled, so this shouldn't be a problem?

[Jakub Nowak]

Oh, wait, it seems like it actually is allowed, and it works in this simple case:

inductive Tree : Type 1 where
| leaf : Tree
| node : {ι : Type} → (ι → Tree) → Tree

noncomputable def Path : Tree → Type
| .leaf => Unit
| @Tree.node ι f => (i : ι) × Path (f i)

def Path.length : {t : Tree} → Path t → Nat
| .leaf, _ => 0
| .node .., ⟨_, p⟩ => p.length.succ

Maybe I'll try with Erased again.

[Jakub Nowak]

Ah, nvm, I think is just the case of Lean being smarter than I think, it looks like it ignores noncomputable attribute, and still looks at the body of the function:

inductive Tree : Type 1 where
| leaf : Tree
| node : {ι : Type} → (ι → Tree) → Tree

noncomputable def Path : Tree → Type
| .leaf => Unit
| @Tree.node ι f => (i : ι) × Path (f i)

def Path' : Tree → Type := Path

[Henrik Böving]

Types are not compileable to begin with, putting a noncomputable annotation on a type definition has no effect.

[Jakub Nowak]

It's kinda hard to grasp what can be computable and what cannot. And the fact that the error

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'

doesn't say which call to Erased.out is a problem doesn't help. :/

E.g. this works perfectly fine:

import Mathlib

namespace Foo

inductive Tree : Type 1 where
| leaf : Tree
| node : {ι : Type} → (Erased ι → Tree) → Tree

def Path : Tree → Type
| .leaf => Unit
| @Tree.node ι f => (i : Erased ι) × Path (f i)

def Path.length : {t : Tree} → Path t → Nat
| .leaf, _ => 0
| .node .., ⟨_, p⟩ => p.length.succ

def t : Tree := .node (fun (b : Erased Bool) => if b.out then .leaf else .leaf)

theorem eq {b : Erased Bool} : Path (if b.out then .leaf else .leaf) = Path .leaf := by
  simp

def ex: Path t := ⟨.mk true, eq ▸ (() : Path .leaf)⟩

end Foo

But when I've tried with this more complicated code:

import Mathlib

inductive VecOrd : Type 1 where
| zero : VecOrd
| succ : VecOrd → VecOrd
| sup : (ι : Type) → (Erased ι → VecOrd) → VecOrd

def VecT (m : Type → Type) (α : Type) : VecOrd → Type
| .zero => Unit
| .succ o => α × m (VecT m α o)
| .sup ι f => (i : Erased ι) ×' m (VecT m α (f i))

structure ManyT (m : Type → Type) (α : Type) : Type 1 where
  { ord : VecOrd }
  val : m (VecT m α ord)

def VecT.none : VecT m α .zero :=
  ()

def ManyT.none [Monad m] : ManyT m α where
  val := pure .none

def VecT.more (x : α) (xs : m (VecT m α o)) : VecT m α o.succ :=
  ⟨x, xs⟩

def ManyT.more' [Monad m] (x : α) (xs : ManyT m α) : ManyT m α where
  val := pure <| .more x xs.val

def ManyT.more [Monad m] (x : m α) (xs : ManyT m α) : ManyT m α where
  val := return .more (← x) xs.val

def VecOrd.add : VecOrd → VecOrd → VecOrd
| zero, o₂ => o₂
| succ o₁, o₂ => succ <| add o₁ o₂
| sup ι f, o₂ => sup ι (fun i ↦ add (f i) o₂)

def VecT.union [Monad m] (xs : VecT m α o₁) (ys : m (VecT m α o₂)) : m (VecT m α (.add o₁ o₂)) :=
match o₁, xs with
| .zero, () => ys
| .succ .., ⟨x, xs⟩ => pure <| more x (do union (← xs) ys)
| .sup .., ⟨i, xs⟩ => pure ⟨i, do union (← xs) ys⟩

def VecOrd.sum : VecOrd → (Erased α → VecOrd) → VecOrd
| zero, _ => zero
| succ o₁, f => sup α (fun x ↦ add (f x) (sum o₁ f))
| sup ι f', f => sup ι (fun i ↦ sum (f' i) f)

def VecT.bind [Monad m] (xs : VecT m α o₁) (f : Erased α → VecOrd) (map : (x : α) → m (VecT m β (f x)))
    : m (VecT m β (.sum o₁ f)) :=
match o₁, xs with
| .zero, () => pure none
| .succ .., ⟨x, xs⟩ => pure ⟨.mk x, do union (← map x) (do bind (← xs) f map)⟩
| .sup .., ⟨i, xs⟩ => pure ⟨i, do bind (← xs) f map⟩

def ManyT.bind [Monad m] (xs : ManyT m α) (map : α → ManyT m β) : ManyT m β where
  val := do VecT.bind (← xs.val) (fun a ↦ (map a.out).ord) (fun a ↦ (map a).val)

now, Lean complains. And I have no idea why. The noncomputable (fun a ↦ (map a.out).ord) function is only ever used to compute m (VecT m β (f x))) and m (VecT m β (.sum o₁ f)) types, so it should work, there's no call to f that needs to be compiled.

[Jakub Nowak]

Ah, nvm, I saw it now. The f x output is passed implicitly to recursive call and it's used in match to decide which branch to take.