how to annotate type in `instance : Functor ...`

Stream: new members

[Shen Weihao]

截屏2024-10-28 21.58.26.png
截屏2024-10-28 21.57.25.png

I found that I can only annotate the type to inferred to let it work. what's the right way to annotate it properly?

[Eric Wieser]

Can you post a #mwe in #backticks, rather than a screenshot?

[Shen Weihao]

ok

inductive Parser (a : Type u) where
  | P (_ : String -> List (a × String))

def Parser.parse : Parser a -> String -> List (a × String)
  | .P p => fun input => p input

instance : Functor Parser where
  map (g : _) (p : _) : _ :=
  .P (fun input => (p.parse input).map (fun (v, out) => (g v, out)))

[Shen Weihao]

is this the right way?

[Shen Weihao]

and I thought I need to annotate as Functor definition like

inductive Parser (a : Type u) where
  | P (_ : String -> List (a × String))

def Parser.parse : Parser a -> String -> List (a × String)
  | .P p => fun input => p input

instance : Functor Parser where
  map (g : a -> b) (p : Parser a) : (Parser b) :=
  .P (fun input => (p.parse input).map (fun (v, out) => (g v, out)))

but it shows a and b is "unknown identifier"

[Shen Weihao]

never mind, I found this definition works

inductive Parser (a : Type u) where
  | P (_ : String -> List (a × String))

def Parser.parse : Parser a -> String -> List (a × String)
  | .P p => fun input => p input

instance : Functor.{u} Parser where
  map {a b : Type u} (g : a -> b) (p : Parser a) : (Parser b) :=
  .P (fun input => (p.parse input).map (fun (v, out) => (g v, out)))

maybe I need to learn something to know why u needs to be annotated and why it is annotated in Functor.{u}

[Kyle Miller]

There's a rule that new universe levels cannot occur inside a definition. By putting it on one of the types in the signature, you can use it inside the definition.

You can use level metavariables to solve this issue:

instance : Functor Parser where
  map {a b : Type _} (g : a -> b) (p : Parser a) : (Parser b) :=
  .P (fun input => (p.parse input).map (fun (v, out) => (g v, out)))

Or, even easier, you can simply omit all the type ascriptions, since they are determined by Functor Parser.

instance : Functor Parser where
  map g p := .P (fun input => (p.parse input).map (fun (v, out) => (g v, out)))

[Shen Weihao]

let the type of arguments to be also inferred, right? thanks for explaining.
And I saw the docs mentioned that

"Lean is based on a version of dependent type theory known as the Calculus of Constructions, with a countable hierarchy of non-cumulative universes and inductive types."

is there any recommended resource about it? I mean the theory part

[Daniel Weber]

There's #tpil, and for a formal treatment of Lean itself there's The type theory of lean by Mario Carneiro

[Kyle Miller]

Shen Weihao said:

let the type of arguments to be also inferred, right?

The where map g p := ... syntax is short for where map := fun g p => .... In

instance : Functor Parser where
  map := fun g p => .P (fun input => (p.parse input).map (fun (v, out) => (g v, out)))

if you move your cursor before fun, by looking at the expected type you can see that the type of map is completely known.

[Shen Weihao]

yeah, I agree, it's known.
I use "inferred" to mean that the compiler does things like annotating type for each value under given context, rather than annotating all things by programmers.
If my expression is inappropriate, feel free to correct me. :smiling_face:

[Shen Weihao]

Daniel Weber 发言道：

There's #tpil, and for a formal treatment of Lean itself there's The type theory of lean by Mario Carneiro

thanks!

[Kyle Miller]

There are many indirect kinds of ways that information is inferred in Lean, and here I wanted to point out that this is not like a normal function definition, since you are providing a value of a specific already-known type.

[Kyle Miller]

The map g p := ... notation makes it feel like a normal function definition, where you are supposed to provide types (like in your earlier map (g : _) (p : _) : _), but it is a structure field, not a normal function definition.

[Shen Weihao]

oh, I learned from other language to use "_" to let compiler infer that thing, so I used here. didn't realize that I can just put arguments here