Zulip Chat Archive

Stream: new members

Topic: inferred Type universe in functors


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Nov 17 2020 at 16:38):

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

view this post on Zulip Kevin Buzzard (Nov 17 2020 at 16:38):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Nov 17 2020 at 16:40):

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

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 17 2020 at 22:21):

How would you make it more polymorphic?

view this post on Zulip Reid Barton (Nov 17 2020 at 22:23):

The most polymorphism you can express is what there is already

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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