Universe Polymorphic `Meta.evalExpr`

Stream: Is there code for X?

[Paul Mure]

Is there a universe-polymorphic version of the MetaM monad? I would like to use Meta.evalExpr on an Expr that lives in a higher universe level.

[Robin Arnez]

Since you're already in unsafe, might as well use unsafeCast:

import Lean
import Qq

inductive HighUniverse : Type 20 where
  | hi
  | there
deriving Repr

open Lean Meta Qq
def test (e : Expr) : MetaM Unit := unsafe do
  let val ← evalExpr NonScalar q(HighUniverse) e
  let val : HighUniverse := unsafeCast val
  Lean.logInfo m!"This thing is: {repr val}"

#eval test q(HighUniverse.hi)

[Kyle Miller]

I'm not sure unsafe means having a license to do anything unsafe — would you mind justifying why this unsafe cast is OK? Also, could you help us understand why NonScalar is the correct dummy type to use here?

Is there any sort of API available to determine what dummy type to use?

[Robin Arnez]

Yeah, you're right; evalExpr doesn't really care about the type you input so anything is fine that isn't a fixed width integer or a floating point value; NonScalar should work just as well as Nat or Int (just needs to be a tobj) but the intention is a bit clearer with NonScalar; then the unsafeCast is basically what evalExpr does anyways but explicitly.

[Kyle Miller]

I take it that NonScalar works even though HighUniverse is represented by a u8 because it's using the polymorphic evalExpr, which works with a boxed result?

[Robin Arnez]

Yeah, equivalent code is produced whether you use UInt8 or NonScalar and then apply the cast.

[Robin Arnez]

The only thing you need to make sure is that it doesn't unbox the result, as when specifying UInt8

[Eric Wieser]

Is there any chance of lean4#3010 going through which would make it possible to build a manual version of a universe-polymorphic MetaM downstream without repeating absolutely everything?

[Kim Morrison]

Can you explain somewhere what this is about? Someone manually building a copy of MetaM downstream seems undesirable?

[Eric Wieser]

Are you asking for this from Paul or me, or both?

[Kim Morrison]

@Eric Wieser, although anyone with a really important use case could answer! :-)

[Eric Wieser]

Here's an argument for universe-polymorphic IO:

class MyInterface (α) where
  foo : α → Nat
  bar : α → α

-- implementations
instance : MyInterface Nat where
  foo x := x
  bar x := x * x

instance : MyInterface Int where
  foo x := x.natAbs
  bar x := x + x

--wrapper type for polymorphism
structure MyInterface.Bundled where
  {α : Type}
  [inst : MyInterface α]
  a : α

-- initial register handlers
def initVal : List (MyInterface.Bundled) := [⟨(1 : Nat)⟩, ⟨(1 : Int)⟩]

-- doesn't work with IO.ref :(
initialize x : List (MyInterface.Bundled) ← initVal

[Eric Wieser]

My understanding is that the MyInterface.Bundled example there is a fairly common pattern (probably with bad names), and essentially implements the mechanism behind a C++ vtable and virtual methods

[Eric Wieser]

(we get a lot of users asking about heterogenous lists, and this is one of the strategies I've seen answered with)

[Kim Morrison]

I'm really hoping here for a bigger picture use case: i.e. some project or potential project that isn't happening or is significantly hobbled by this. I understand that some code doesn't compile with the current IO and MetaM. :-)

The vtable pointer is helpful. But is this something that anyone in the Lean world is actually missing?

[Eric Wieser]

Any such code can ultimately use unsafeCast so I think significant hobbling is not going to happen here.

[Eric Wieser]

I guess in that regard the example I give above can be solved with an UnsafeUDrop x type that puts something in lower universe, which I think I've seem somewhere.

[Eric Wieser]

(if someone remembers what I'm thinking of, we should add it to the docstring for docs#ULift)

[Eric Wieser]

Here's a prototype that is probably dangerous:

/-- Squash any type to `Type 0` so that it can be used with IO. -/
unsafe structure USquash! (α : Type u) : Type where
  private rawDown ::
    private rawUp : NonScalar

unsafe def USquash!.up (x : USquash! α) : α := unsafeCast x.rawUp
unsafe def USquash!.down (x : α) : USquash! α := USquash!.rawDown (unsafeCast x)

(edit: as discussed at #lean4 > universe polymorphic IO @ 💬 )

[Paul Mure]

@Kim Morrison I'm working on a compiler project where I would like to turn an untyped AST of a DSL into an intrinsically-typed PHOAS version. The details gets a bit complicated; but roughly, this allows me to get type-checking and some type-inference for free using Lean's mvar unification during elaboration.

The problem is that the resulting the PHOAS representation lives in Type 1. I think I can work around this by having a command that inserts a def containing the thing I want. Then calling whatever function I need to call on the resulting definition in meta-lean. But it would be better if I can just have an IO monad returning the Type 1 PHOAS syntax directly.