Universe issues with polymorphic types

Stream: new members

[Calvin Lee]

Hello! I'm having a bit of some trouble with universes and polymorphism
I would like to have a continuation-based type with a polymorphic answer type. In particular I am implementing the "LogicT" monad transformer, which uses this. My current formulation from the Logic paper, using success and failure continuations is as follows:

def FK (ans : Type u) : Type u := ans
def SK (ans : Type u) (a : Type u) : Type u := a -> FK ans -> ans

def LogicT (m : Type u -> Type u) (a : Type u) : Type (u + 1) :=
  {ans : Type u} -> SK (m ans) a -> FK (m ans) -> m ans

Unfortunately due to the polymorphism, I have to raise the universe level at the very end. This is fine, but it starts to create issues when I have to do things like LogicT m X where X contains some other instance of a LogicT m a
Is there any way to get around this or am I going down the wrong path?

[Yakov Pechersky]

Would this work?

universes u v

def FK (ans : Type*) : Type* := ans
def SK (ans : Type*) (a : Type*) : Type* := a -> FK ans -> ans

def LogicT (m : Type u -> Type v) (a : Type u) {ans : Type u} : Type (max u v) :=
  SK (m ans) a -> FK (m ans) -> m ans

[Yakov Pechersky]

It can be generalized to more universes it seems:

def FK (ans : Type*) : Type* := ans
def SK (ans : Type*) (a : Type*) : Type* := a -> FK ans -> ans

def LogicT (m : Type* -> Type*) (a : Type*) {ans : Type*} : Type* :=
  SK (m ans) a -> FK (m ans) -> m ans

#check LogicT

[Calvin Lee]

What is Type*? It doesn't seem to work for me, probably because I'm using lean4.

But the issue with putting {ans : Type u} in the definition is that I can no longer instantiate classes for it
For example I have this definition

instance [Monad m] : Monad (LogicT m) := ...

Which if I add ans as an optional argument complains

application type mismatch
  Monad (LogicT m)
argument
  LogicT m
has type
  Type ?u.247 → {ans : Type ?u.247} → Type (max ?u.247 ?u.246)
but is expected to have type
  Type ?u.252 → Type ?u.251

[Yakov Pechersky]

Use Type _ instead: https://leanprover.github.io/lean4/doc/typeobjs.html?highlight=type*

[Yakov Pechersky]

def FK (ans : Type _) : Type _ := ans
def SK (ans : Type _) (a : Type _) : Type _ := a -> FK ans -> ans

def LogicT (m : Type _ -> Type _) (a : Type _) : Type _ :=
  Π {ans : Type _}, SK (m ans) a -> FK (m ans) -> m ans

#check LogicT

Yes you get the increase in universes unfortunately.

[Calvin Lee]

Hm, is there any way to nest them then? Possibly with a function that increases the universe by a level?

[Yakov Pechersky]

def FK (ans : Type _) : Type _ := ans
def SK (ans : Type _) (a : Type _) : Type _ := a -> FK ans -> ans

def LogicT (m : Type _ -> Type _) (a : Type _) : Type _ :=
  Π {ans : Type _}, SK (m ans) a -> FK (m ans) -> m ans

instance {m} [monad m] : monad (LogicT m) :=
{ map := _,
  map_const := _,
  pure := _,
  seq := _,
  seq_left := _,
  seq_right := _,
  bind := _ }

[Yakov Pechersky]

Can you fill those in Lean 3?

[Calvin Lee]

I just did pure & bind, since that seems to compile just fine

def FK (ans : Type*) : Type* := ans
def SK (ans : Type*) (a : Type*) : Type* := a -> FK ans -> ans

def LogicT (m : Type* -> Type*) (a : Type*) : Type* :=
  Π {ans : Type*}, SK (m ans) a -> FK (m ans) -> m ans

def logicPure {m a} [monad m] (x : a) : LogicT m a := fun _ sk fk, sk x fk
def logicBind {m a b} [monad m] (x : LogicT m a)  (f : a -> LogicT m b) : LogicT m b :=
  λ _ sk,  x (λ  a, (f a) sk)

instance {m} [monad m] : monad (LogicT m) :=
{ pure := λ _ , logicPure,
  bind := λ _ _, logicBind,
}

[Yakov Pechersky]

Great, so will that work in Lean 4?

[Calvin Lee]

Yes! the bindings for monads and such work great. The issue is this (arguably important) function from the paper

def msplit {m a} (x : LogicT m a) : LogicT m (Maybe (a , LogicT m a)) := _

which is used to create "fairness" results and reading of one result at a time even with a strict monad m

[Yakov Pechersky]

Option is Lean4 for Maybe, but I'm sure you know that

[Calvin Lee]

Oh that's helpful, I thought there wasn't a Maybe so I created it myself....