Recursion Schemes and type universes

Stream: general

[Solomon]

Hi. As an exercise I'm trying to do some basic recursion schemes but immediately ran into problems with type universes:

inductive Mu (f : Type u → Type v)  where
  | mkMu : {α : Type u} → (f α → α) → Mu f

def cata {f : Type u → Type v} {α : Type u} : (f α → α) → (Mu f) → α :=
  fun alg (Mu.mkMu f) => f alg

error: application type mismatch
  f alg
argument
  alg
has type
  f✝ α → α : Type (max u v)
but is expected to have type
  f✝ α✝ : Type v

I dont have much experience dealing with type universes. How would I go about fixing this code?

[Timo Carlin-Burns]

This error doesn't seem to have to do with type universes at all! Your code is doing something confusing where you have two variables named f. I'll rename one of them to g and replace all of the universe parameters with just Type so we can talk about this code more easily:

inductive Mu (f : Type → Type)  where
  | mkMu : {α : Type} → (f α → α) → Mu f

def cata {f : Type → Type} {α : Type} : (f α → α) → (Mu f) → α :=
  fun alg (Mu.mkMu g) => g alg

application type mismatch
  g alg
argument
  alg
has type
  f α → α : Type
but is expected to have type
  f α✝ : Type

[Timo Carlin-Burns]

The error is that the expression g alg doesn't make sense because alg is not the right type to be an argument to the function g

[Solomon]

Oh thats silly of me. I made a mistake in my definition of Mu. It should be:

inductive Mu (f : Type u → Type v)  where
  | mkMu : {α : Type u} → ((f α → α) → α) → Mu f

def cata {f : Type u → Type v} {α : Type u} [Functor f] : (f α → α) → Mu f → α :=
  fun alg (Mu.mkMu g) => g alg

Which gives me the following error:

error: application type mismatch
  g alg
argument
  alg
has type
  f α → α : Type (max u v)
but is expected to have type
  f α✝ → α✝ : Type (max v u)

Is this just an issue of Lean not knowing that max is commutative?

[Timo Carlin-Burns]

It's still not about universes :). The important difference here is between α and α✝. I'll explain where α✝ comes from.

When you write fun alg (Mu.mkMu g) => you're pattern matching on the constructor Mu.mkMu which takes three arguments, f, α and g:

#check Mu.mkMu
-- Mu.mkMu.{u, v} {f : Type u → Type v} {α : Type u} (g : (f α → α) → α) : Mu f

g is included in your pattern because it's the only explicit argument, but the first two, f and α are implicit. f is fully determined by the type Mu f, but this value of α that was passed to Mu.mkMu to construct a Mu f could be anything. Since you're not explicitly giving it a name, it enters your local context as an inaccessible variable α✝. You can see the full local context to verify this by replacing your code with an _

def cata {f : Type u → Type v} {α : Type u} [Functor f] : (f α → α) → Mu f → α :=
  fun alg (Mu.mkMu g) => _
-- context:
-- f: Type u → Type v
-- α: Type u
-- inst✝: Functor f
-- alg: f α → α
-- x✝: Mu f
-- α✝: Type u
-- g: (f α✝ → α✝) → α✝
-- ⊢ α

[Solomon]

@Timo Carlin-Burns Thanks for the explanation! It took me a while but I finally made it through this implementation and got it to evaluate:

inductive Mu (f : Type u → Type u) : Type (u + 1)  where
  | mkMu : ((α : Type u) → ((f α → α) → α)) → Mu f

def cata {f : Type u → Type u} {α : Type u} : (f α → α) → Mu f → α :=
  fun alg (Mu.mkMu f) => f α alg

inductive ListF : (α : Type u) → (r : Type u) → Type u where
  | nilF : ListF α r
  | consF (head : α) (tail : r) : ListF α r

def nil (a : Type u) : Mu (ListF α) :=
  Mu.mkMu (λ _ alg => alg ListF.nilF)

def cons : α → Mu (ListF α) → Mu (ListF α) :=
  λ x (Mu.mkMu xs) => Mu.mkMu (λ t alg => alg (ListF.consF x (xs t alg)))

def ex : Mu (ListF Bool) :=
  cons True (cons False (cons True (nil Bool)))

def len_algebra : ListF α Nat → Nat
  | ListF.nilF => 0
  | ListF.consF _ r => 1 + r

def len : Mu (ListF α) → Nat :=
  fun xs => cata len_algebra xs

#eval len ex

This is a lot tricker then in Haskell but I learned a lot.

[Solomon]

I can do Nu and ana easily enough:

inductive Nu (f : Type u → Type u) : Type (u + 1) where
  | mkNu : (α : Type u) → (α → f α) → α → Nu f

def ana {f : Type u → Type u} {α : Type u} : (α → f α) → α → Nu f :=
  fun coalg x => Nu.mkNu α coalg x

def list_coalg : Nat → ListF Nat Nat
  | Nat.zero => ListF.nilF
  | Nat.succ i => ListF.consF i i

def list_builder : Nat → Nu (ListF Nat) :=
  fun n => ana list_coalg n

But then the problem becomes how can I fold Nu f into some other functor (such as List Nat for my list_builder example). Is it possible to write cata for Nu and ana for Mu in this setting? In haskell we take advantage of explicit recursion or a hylomorphism to do that.

And what about Fix? Is it possible to write Fix? I haven't made any progress on it.