Variables and class inference

Stream: general

[Meow]

Can variables or parameters inside a section be used in class inference? For example, the following code will report an error:

section sec1
class cl1 := (s : nat)
parameter [x : cl1]
open cl1
def y := s + 1
end sec1

[Yaël Dillies]

Does

section sec1
class cl1 := (s : nat)
parameter [x : cl1]
open cl1
def y := x.s + 1
end sec1

do what you want?

[Kyle Miller]

I'm not sure why parameter doesn't work, but if you do variable instead and make sure to include it (which ensures it always is included in an argument list) then it works:

section sec1

class cl1 := (s : nat)
open cl1

variable [x : cl1]
include x

def y := s + 1
end sec1

[Meow]

Yaël Dillies said:

Does

section sec1
class cl1 := (s : nat)
parameter [x : cl1]
open cl1
def y := x.s + 1
end sec1

do what you want?

Yes, it really does. But in real situation, the class will have many (about 10) records, not just only s. So adding all x. will make the code mode complex.

[Meow]

Kyle Miller said:

I'm not sure why parameter doesn't work, but if you do variable instead and make sure to include it (which ensures it always is included in an argument list) then it works:

section sec1

class cl1 := (s : nat)
open cl1

variable [x : cl1]
include x

def y := s + 1
end sec1

Thanks!

[Meow]

And parameter also works.

[Yaël Dillies]

In Lean 3, parameter is buggy and you should avoid it. Unnamed typeclass arguments are automatically added to the context, sovariable [cli] will do the same as variable [x : cl1] include x

[Meow]

Thanks! By the way, what is the bugs of parameter?

[Meow]

A trick for avoid parameter is, for example when you need parameter n : nat, you can write a class enclosing n as a record, such as class cl1 := (n : nat), and use variable [cl1] then open cl1 in a section.

[Meow]

Then every term in the section that uses n will be considered as using cl1.n _inst_1, and every function you defined will adds Π [_inst_1 : cl1]. When a function that defined later in the section uses it, the class inference will give the correct result.

[Yaël Dillies]

I don't understand the bug in parameter, but the result is that it's hardly usable.

[Martin Dvořák]

This is precisely the conclusion I reached a few months ago as well.