what is α

Stream: new members

[J. O.]

so i have this code:

def maxList (list: List Nat) : Option Nat :=
    List.maximum? list

def callMaxList (list: α) :=
    maxList list

this code gives the error

application type mismatch
  maxList list
argument
  list
has type
  α : Sort ?u.63
but is expected to have type
  List Nat : Type

what is α exactly? i thought it was like some generic type, but im starting to reconsider

[Yaël Dillies]

Yes, precisely. It is a generic type, and you gave it somewhere where Nat was expected.

[Yaël Dillies]

A generic type is usually not Nat!

[J. O.]

then what is it?

[Reid Barton]

More importantly, a general type is not a list

[J. O.]

why isnt the generic type doing its job

[Yaël Dillies]

It doesn't try to unify, if that's what you mean.

[J. O.]

Reid Barton said:

More importantly, a general type is not a list

what do you mean?

[Reid Barton]

The actual definition of callMaxList is something like def callMaxList {α : Type} (list: α) := maxList list. α is a variable that can be provided by the user of your function callMaxList, and they could choose something like α = Bool. In that case list : Bool and so maxList list doesn't make sense.

[Yaël Dillies]

α : Type means that you can replace α with any type after you've defined your function. But you're trying to do the opposite, make Lean replace α with Nat.

[Reid Barton]

What you maybe want is not an actual variable list: α but a metavariable list: _, meaning "Lean please figure out what should go here".

[Reid Barton]

Although, it would usually be better to just say what should go there.

[J. O.]

Yaël Dillies said:

α : Type means that you can replace α with any type after you've defined your function. But you're trying to do the opposite, make Lean replace α with Nat.

ah i see

[Kyle Miller]

I know you're familiar with f#, and I think you can think of your second definition as doing let callMaxList<'a> (list : List<a>) := maxList list (I probably got the syntax wrong). This is a type error since maxList expects a List<Nat>, not a generic List<a>.

[Yaël Dillies]

Nor a generic <a>!

[J. O.]

Kyle Miller said:

I know you're familiar with f#, and I think you can think of your second definition as doing let callMaxList<'a> (list : List<a>) := maxList list (I probably got the syntax wrong). This is a type error since maxList expects a List<Nat>, not a generic List<a>.

that makes sense

[J. O.]

you would have to give the type

[J. O.]

i have another type related question. so I was reading the manual, and came across

def p1 (a b c d : Nat) : Prop :=
  (a + b)^c ≤ d

def p2 (i j k : Int) : Prop :=
  i % (j * k) = 0

why are the return types of these two functions Prop instead of Bool?

[Yaël Dillies]

because that would require them to be decidable, which is more information

[Yaël Dillies]

but they could have been

[J. O.]

what do you mean by "decidable"? and what does Prop do to the return type?

[Kyle Miller]

A handwavey answer: a Prop is like a Bool that knows what it is that's supposed to be true or false.

[J. O.]

why is that useful?

[J. O.]

especially in these two functions?

[J. O.]

and why is it in numbers and not booleans image.png