inferred Type universe in functors

Stream: new members

[Yakov Pechersky]

Why is there an error in the second definition -- is there some difference in how universes are instantiated using a variables call?

section

def enum_some_core {α : Type*} : ℕ → list (option α) → list (option ℕ)
| _ [] := []
| n (x :: xs) := (functor.map_const n x) :: enum_some_core (option.cases_on x n (λ _, n + 1)) xs

end

section

variable {α : Type*}

def enum_some_core' : ℕ → list (option α) → list (option ℕ)
| _ [] := []
| n (x :: xs) := (functor.map_const n x) :: enum_some_core (option.cases_on x n (λ _, n + 1)) xs
-- error at functor.map_const

end

[Kevin Buzzard]

You might have written alpha : Type* in the first one, but if you #check @enum_some_core you'll see that Lean decided that alpha had type Type. It didn't have the ability to downgrade your alpha in the second one.

[Yakov Pechersky]

I see, the alpha is restricted to be just Type. Why is that?

[Kevin Buzzard]

That's a logic puzzle which I don't immediately know the answer to.

[Kevin Buzzard]

If you change it to alpha : Type 1 you can look at the error you get and try and figure it out. Some internal thing is demanding Type.

[Yakov Pechersky]

The reason I think is because option nat is Type because nat is Type

[Kevin Buzzard]

map_const : Π {α β : Type u}, α → f β → f α -- here alpha and beta need to have the same type. I don't know what any of these objects are so am in no real position to help.

[Yakov Pechersky]

So I just have to avoid the functor instance:

section

def enum_some_core {α : Type*} : ℕ → list (option α) → list (option ℕ)
| _ [] := []
| n (x :: xs) := (functor.map_const n x) :: enum_some_core (option.cases_on x n (λ _, n + 1)) xs

end

section

variable {α : Type*}

def enum_some_core' : ℕ → list (option α) → list (option ℕ)
| _ [] := []
| n (x :: xs) := (x.map (λ _, n)) :: enum_some_core' (option.cases_on x n (λ _, n + 1)) xs

end

/-
⊢ Π {α : Type}, ℕ → list (option α) → list (option ℕ)
-/

#check @enum_some_core
/-
⊢ Π {α : Type u_1}, ℕ → list (option α) → list (option ℕ)
-/

#check @enum_some_core'

[Yakov Pechersky]

Why are functor limited in how they infer universes? I'm trying to now do something like:

import data.list

lemma list.map_comp_map {α β γ : Type*} {l : list α} (f : α → β) (g : β → γ) :
  list.map g ∘ list.map f = list.map (g ∘ f) :=
begin
  convert functor.map_comp_map f g,
end

but the universes don't agree.

[Yakov Pechersky]

A, functor code expects all the input types to be of the same universe. Same issue as before. Why isn't it more polymorphic in universes in core?

[Reid Barton]

How would you make it more polymorphic?

[Reid Barton]

The most polymorphism you can express is what there is already

[Yakov Pechersky]

I am not sure yet, experimenting. But this lemma indicates that it is more powerful for list than it is for a generic functor, and I'm trying to understand why. Haven't gotten there yet.

import data.list

open list

namespace list

lemma comp_map {α β γ : Type*} (l : list α) (g : α → β) (h : β → γ)  :
  map (h ∘ g) l = map h (map g l) := (map_map _ _ _).symm

lemma map_comp_map {α β γ : Type*} (f : α → β) (g : β → γ) :
  map g ∘ map f = map (g ∘ f) :=
by apply funext; intro; rw comp_map

/-
map_comp_map :
  ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ), map g ∘ map f = map (g ∘ f)
-/
-- works over 3 universes

#check @map_comp_map

/-
functor.map_comp_map :
  ∀ {F : Type u_1 → Type u_2} {α β γ : Type u_1} [_inst_1 : functor F] [_inst_2 : is_lawful_functor F]
  (f : α → β) (g : β → γ), functor.map g ∘ functor.map f = functor.map (g ∘ f)
-/
-- input types all in 1 universe

#check @functor.map_comp_map

end list

[Yakov Pechersky]

Where the proof for map_comp_map is tactically the same as the proof for functor.map_comp_map

[Reid Barton]

That's because list has a free universe variable, but once something is the argument of functor it has to be instantiated to a specific universe.

[Yakov Pechersky]

I see. So we can't use the fact that list is a lawful functor to avoid replication of functor-like lemmas.