Type specialization & boxing

Stream: lean4

[Mac Malone]

A fun little discrepancy I noticed with how the runtime representation of types is determined:

/-- i.e., `Subtype` -/
structure Generic {α : Type u} (P : α → Prop) where
  val : α
  property : P val

/-
def irrelevant : ◾ :=
  ret ◾
-/
set_option trace.compiler.ir.result true in
def irrelevant : Generic (fun _ : Type u => True) :=
  ⟨PUnit, .intro⟩

structure Specialized (P : Type u → Prop) where
  val : Type u
  property : P val

/-
def boxed : obj :=
  let x_1 : obj := ctor_0[Specialized.mk];
  ret x_1
-/
set_option trace.compiler.ir.result true in
def boxed : Specialized (fun _ : Type u => True) :=
  ⟨PUnit, .intro⟩

As Specialized is simply a specialization of Generic one might expect them to receive the same representation, but they do not. In fact, Generic arguably receives the better (more efficient) one.

[Mario Carneiro]

I don't think this is documented at ffi.md

[Mac Malone]

Yeah, I suspect it might be a bug (though I am not sure in which direction).

[Mario Carneiro]

lol, there is at least one almost-certainly-a-bug documented there

[Mario Carneiro]

I suspect in this particular case that they are getting the same repr though

[Mario Carneiro]

it might not be the same in more nested situations?

[Mac Malone]

Mario Carneiro said:

I suspect in this particular case that they are getting the same repr though

What do you mean?

[Mac Malone]

In the above example, they are definitely behaving differently.

[Mario Carneiro]

are you sure? Both ◾ and ctor_0[Specialized.mk] will be represented as lean_box(0)

[Mario Carneiro]

i.e if another part of the code decided that actually Specialized should be getting the same repr as Generic, there would not be an ABI mismatch

[Mac Malone]

They can be both lean_box(0), but they do not always have the same properities. Parameters of type ◾ will be erased for FFI (whereas the boxed version will not) and the IR will delete operations on objects of ◾ if can (whereas it will perserve the boxed versions).

[Mac Malone]

For an example of how this causes different behavior:

-- Stub just for show
def IsNat := fun _ : Type => True

def GNat := Generic IsNat
instance : Nonempty GNat := ⟨PUnit, .intro⟩

opaque GNat.ofNat (n : Nat) : GNat := unsafe unsafeCast n
opaque GNat.toNat (n : GNat) : Nat := unsafe unsafeCast n

instance : Repr GNat where
  reprPrec n prec := reprPrec n.toNat prec

/-- info: 0 -/
#guard_msgs in #eval GNat.ofNat 3

def SNat := Specialized IsNat
instance : Nonempty SNat := ⟨PUnit, .intro⟩

opaque SNat.ofNat (n : Nat) : SNat := unsafe unsafeCast n
opaque SNat.toNat (n : SNat) : Nat := unsafe unsafeCast n

instance : Repr SNat where
  reprPrec n prec := reprPrec n.toNat prec

/-- info: 3 -/
#guard_msgs in #eval SNat.ofNat 3