## Stream: new members

### Topic: inferred Type universe in functors

#### Yakov Pechersky (Nov 17 2020 at 16:35):

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 (Nov 17 2020 at 16:37):

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 (Nov 17 2020 at 16:38):

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

#### Kevin Buzzard (Nov 17 2020 at 16:38):

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

#### Kevin Buzzard (Nov 17 2020 at 16:39):

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 (Nov 17 2020 at 16:40):

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

#### Kevin Buzzard (Nov 17 2020 at 16:40):

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 (Nov 17 2020 at 16:43):

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 (Nov 17 2020 at 22:14):

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 (Nov 17 2020 at 22:18):

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 (Nov 17 2020 at 22:21):

How would you make it more polymorphic?

#### Reid Barton (Nov 17 2020 at 22:23):

The most polymorphism you can express is what there is already

#### Yakov Pechersky (Nov 17 2020 at 22:30):

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 (Nov 17 2020 at 22:30):

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

#### Reid Barton (Nov 17 2020 at 22:31):

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 (Nov 17 2020 at 22:32):

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

Last updated: May 15 2021 at 00:39 UTC