how to implement toProxy? (universe polymorphism problem)

Stream: lean4

[Serhii Khoma (srghma)]

I am trying to implement https://github.com/jwiegley/coq-pipes/blob/ec4e7884dc2d2c1a55ee075103c964b4f65c7be6/src/Pipes/Extras.v#L27

i've made s explicit

inductive Proxy.{u} (a' a b' b : Type u) (m : Type u → Type u) (r : Type u) : Type (u+1)
  | Request : a' → (a → Proxy a' a b' b m r) → Proxy a' a b' b m r
  | Respond : b → (b' → Proxy a' a b' b m r) → Proxy a' a b' b m r
  | M       {x : Type u} (op : m x) (cont : x → Proxy a' a b' b m r) : Proxy a' a b' b m r
  | Pure    : r → Proxy a' a b' b m r


abbrev CProxy (a' a b' b : Type u) (m : Type u → Type u) (r : Type u) : Type (u+1) :=
  ∀ (s : Type u),
    (a' → (a → s) → s) →       -- Handle Request
    (b → (b' → s) → s) →       -- Handle Respond
    (∀ x, (x → s) → m x → s) → -- Handle
    (r → s) →                  -- Handle Pure
    s

-- Convert inductive Proxy into Church-encoded CProxy
def fromProxy (p : Proxy a' a b' b m r) : CProxy a' a b' b m r :=
  match p with
  /- | .Request xa' k => CProxy.Request xa' (fun a => fromProxy (k a)) -/
  /- | .Respond xb k  => CProxy.Respond xb  (fun b' => fromProxy (k b')) -/
  | .Request xa' k => fun s ka kb km kp => ka xa' (fun xa => fromProxy (k xa) s ka kb km kp)
  | .Respond xb k  => fun s ka kb km kp => kb xb (fun b' => fromProxy (k b') s ka kb km kp)
  | .M mx k        => fun s ka kb km kp => km _ (fun x => fromProxy (k x) s ka kb km kp) mx
  | .Pure xr       => fun _s _ka _kb _km kp => kp xr


def toProxy (p : CProxy.{u} a' a b' b m r) : Proxy.{u} a' a b' b m r :=
  p (Proxy a' a b' b m r)
    (fun a' k => Proxy.Request a' (fun a => toProxy (k a)))
    (fun b k => Proxy.Respond b (fun b' => toProxy (k b')))
    (fun _ k mx => Proxy.M mx (fun x => toProxy (k x)))
    Proxy.Pure

but the toProxy throws error

Application type mismatch: In the application
  p (Proxy a' a b' b m r)
the argument
  Proxy a' a b' b m r
has type
  Type (u + 1) : Type (u + 2)
but is expected to have type
  Type u : Type (u + 1)

I'm stuck and dont know how to go from here

I've heard there is a universe bump problem with Church-encoding. Probably that's it. How to overcome it?

[Quang Dao]

Try changing universe level of CProxy to u + 1 for p?

[Serhii Khoma (srghma)]

Quang Dao said:

Try changing universe level of CProxy to u + 1 for p?

like this ? this works

inductive Proxy.{u} (r : Type u) : Type (u+1)
  | Pure    : r → Proxy r


abbrev CProxy.{u} (r : Type u) : Type (u+2) :=
  ∀ {s : Type (u+1)},
    (r → s) →                  -- Handle Pure
    s

-- Convert inductive Proxy into Church-encoded CProxy
def fromProxy (p : Proxy r) : CProxy r :=
  match p with
  | .Pure xr       => fun kp => kp xr


def toProxy (p : CProxy.{u} r) : Proxy.{u} r :=
  p Proxy.Pure

this works too

inductive Proxy.{u} (r : Type u) : Type (u+1)
  | Pure    : r → Proxy r


abbrev CProxy.{u} (r : Type u) : Type (u+2) :=
  ∀ (s : Type (u+1)),
    (r → s) →                  -- Handle Pure
    s

-- Convert inductive Proxy into Church-encoded CProxy
def fromProxy (p : Proxy r) : CProxy r :=
  match p with
  | .Pure xr       => fun _s kp => kp xr


def toProxy (p : CProxy.{u} r) : Proxy.{u} r :=
  p (Proxy.{u} r) Proxy.Pure

this works too

inductive Proxy.{u} (a' a b' b : Type u) (m : Type u → Type u) (r : Type u) : Type (u+1)
  | Request : a' → (a → Proxy a' a b' b m r) → Proxy a' a b' b m r
  | Respond : b → (b' → Proxy a' a b' b m r) → Proxy a' a b' b m r
  | M       {x : Type u} (op : m x) (cont : x → Proxy a' a b' b m r) : Proxy a' a b' b m r
  | Pure    : r → Proxy a' a b' b m r


abbrev CProxy.{u} (a' a b' b : Type u) (m : Type u → Type u) (r : Type u) : Type (u+2) :=
  ∀ (s : Type (u+1)),
    (a' → (a → s) → s) →       -- Handle Request
    (b → (b' → s) → s) →       -- Handle Respond
    (∀ x, (x → s) → m x → s) → -- Handle
    (r → s) →                  -- Handle Pure
    s

-- Convert inductive Proxy into Church-encoded CProxy
def fromProxy (p : Proxy a' a b' b m r) : CProxy a' a b' b m r :=
  match p with
  /- | .Request xa' k => CProxy.Request xa' (fun a => fromProxy (k a)) -/
  /- | .Respond xb k  => CProxy.Respond xb  (fun b' => fromProxy (k b')) -/
  | .Request xa' k => fun s ka kb km kp => ka xa' (fun xa => fromProxy (k xa) s ka kb km kp)
  | .Respond xb k  => fun s ka kb km kp => kb xb (fun b' => fromProxy (k b') s ka kb km kp)
  | .M mx k        => fun s ka kb km kp => km _ (fun x => fromProxy (k x) s ka kb km kp) mx
  | .Pure xr       => fun _s _ka _kb _km kp => kp xr


def toProxy (p : CProxy.{u} a' a b' b m r) : Proxy.{u} a' a b' b m r :=
  p (Proxy a' a b' b m r)
    (fun xa' xk => Proxy.Request xa' xk)
    (fun xb xk => Proxy.Respond xb xk)
    (fun _ xk mx => Proxy.M mx xk)
    Proxy.Pure

-- but it broke

abbrev CProxy.runEffect {m : Type u → Type u} {a b' r : Type u} [Monad m] (eff : CProxy.{u} PEmpty a b' PEmpty m r) : m r :=
  eff (m r)
    (fun x _ => PEmpty.elim x) -- Handle Request (impossible)
    (fun x _ => PEmpty.elim x) -- Handle Respond (impossible)
    (fun _ f mt => mt >>= f)   -- Handle M
    pure                       -- Handle Pure

worked with this definition https://github.com/sergeynordicresults/lean-pipes/blob/b4f9dc7f7ae49dac0eb026566f7055dbac89426e/pipes/Pipes/Extra/ChurchPipes/Internal.lean#L2

what's left is to prove this theorem https://github.com/sergeynordicresults/lean-pipes/blob/b4f9dc7f7ae49dac0eb026566f7055dbac89426e/pipes/Pipes/Extra/ChurchPipes/FromTo.lean#L62 but even coq version uses axioms, so wont do it now

tnx