implicit arguments

Stream: lean4

[Joseph O]

I am creating a function that returns the average of the elements generated by applying the function to each element of the list. I am having trouble getting all the implicit parameters right. this is what i have so far:

@[inline] def averageBy [Add α] [HDiv α Nat α] [HAdd α α $ outParam α] [Inhabited α] [OfNat α 0] (projection: β → α) : List α → α
  | [] => panic! "invalid argument exception: may not provide empty list"
  | xs =>
    let sum := xs.foldr (fun x y => projection x + projection y) 0
    let length := xs.length
    sum / length

but i have these three errors:

failed to synthesize instance
  HDiv β Nat ?m.1886

failed to synthesize instance
  OfNat β 0

type mismatch
  projection x + projection y
has type
  outParam α : Type ?u.1080
but is expected to have type
  β : Type ?u.1153

any help would be appreciated

[Alexander Bentkamp]

Why is projection of type β → α? If you change it to α → α, it works.

[Joseph O]

Alexander Bentkamp said:

Why is projection of type β → α? If you change it to α → α, it works.

right, but i dont want it to nessacerily take in type a

[Joseph O]

@Alexander Bentkamp I would like to be able to do something like

structure test where
  num : Nat
  letter : Char

def getNum (arg : test) :=
  arg.num

#eval averageBy getNum [{num := 1, letter := 'A'}, {num := 2, letter := 'A'}, {num := 3, letter := 'A'}]

if you see what i mean

[Arthur Paulino]

If you explicit the type of sum as α, the error message will be more insightful:

@[inline] def averageBy
    [Add α] [HDiv α Nat α] [HAdd α α $ outParam α] [Inhabited α] [OfNat α 0]
    (projection: β → α) : List α → α
  | [] => panic! "invalid argument exception: may not provide empty list"
  | xs =>
    let sum : α := xs.foldr (fun x y => (projection x) + (projection y)) 0
    let length := xs.length
    sum / length

[Joseph O]

Ok thanks. I will try it out

[Joseph O]

I was playing around with it a bit but I was not able to fix it

[Siddhartha Gadgil]

Is the following what you want (slight tweak of @Arthur Paulino's code).

@[inline] def averageBy
    [Add α] [HDiv α Nat α] [HAdd α α $ outParam α] [Inhabited α] [OfNat α 0]
    (projection: β → α) : List β  → α
  | [] => panic! "invalid argument exception: may not provide empty list"
  | xs =>
    let sum : α := xs.foldr (fun x y => (projection x) + y) 0
    let length := xs.length
    sum / length

[Arthur Paulino]

Was about to post almost the same thing

[Yakov Pechersky]

Is the inhabited instance being used for panic!?

[Arthur Paulino]

@Joseph O note that if you want to use projection on the elements of xs, then they must be of type β. Hence the return type List β → α.

And the other issue was a misuse of foldr

[Joseph O]

Yakov Pechersky said:

Is the inhabited instance being used for panic!?

Yeah

[Joseph O]

Siddhartha Gadgil said:

Is the following what you want (slight tweak of Arthur Paulino's code).

@[inline] def averageBy
    [Add α] [HDiv α Nat α] [HAdd α α $ outParam α] [Inhabited α] [OfNat α 0]
    (projection: β → α) : List β  → α
  | [] => panic! "invalid argument exception: may not provide empty list"
  | xs =>
    let sum : α := xs.foldr (fun x y => (projection x) + y) 0
    let length := xs.length
    sum / length

well that works. I see what the type mismatches were

[Joseph O]

Small thing, what was wrong with the misuse of foldr? I didn't really understand the fix

[Siddhartha Gadgil]

The type of the result had to be specified, otherwise lean inferred it was β.

[Siddhartha Gadgil]

In the original code, the main mistake was that you were taking a projection of the accumulator for the sum, not only the entries of the list.

[Arthur Paulino]

Yeah, and the accumulator was already of type α

[Joseph O]

Ah I see