Design question

Stream: lean4

[Juan Pablo Romero]

Say I have a type like this:

inductive GADT: Type -> Type 1 where
  | c1 (v: A)   (id: Option Nat := none) : GADT A
  | c2 (i: Int) (id: Option Nat := none) : GADT Int

def GADT.setId (gadt: GADT A) (id: Nat): GADT A :=
  match gadt with
    | c1 v _ => c1 v id
    | c2 i _ => c2 i id

where each constructor has an optional id that is intended to be generated randomly at runtime like so:

do
  let r <- IO.rand 0 100000000
  let gadt <- gadt.setId r

Ideally this operation would be defined in a function, for example:

def GADT.ensureId (gadt: GADT A): IO (GADT A) := do
  let r <- IO.rand 0 100000000
  return gadt.setId r

I know that IO has type : Type -> Type so the above function doesn't compile.

I wonder if people have ideas on how to overcome this issue?

One option would be to store the ids as IO.Ref Nat, but maybe there's a better way?

[James Gallicchio]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO this might be worth reading?