Zulip Chat Archive

Stream: new members

Topic: accessing typeclass member fails


view this post on Zulip Chris M (Nov 03 2020 at 15:23):

I just wrote this for a quick test, and it gives me an unexpected error:

class FinT (T:Type*)  :=
(n:nat) (emb:T  nat) (embinv:nat  T) (finite: t, emb t < n) (bijective:  t, embinv (emb t) = t)

set_option trace.eqn_compiler.elim_match true

def summation (T:Type*) (f:(T  Prop)  nat) [h:FinT T]: T  nat := fun t:T,
let n:nat := ((h.emb) t) in
match n with
| (nat.succ k) := 1
| zero := 0
end

gives me the error:

invalid field notation, function 'FinT.emb' does not have explicit argument with type (FinT ...)

What is weird is that if I replace the let statement with the following, it doesn't give any errors:

let embbbb:T  nat := h.emb in
let n:nat := ((embbbb) t) in

view this post on Zulip Johan Commelin (Nov 03 2020 at 15:24):

Replacing h.emb with FinT.emb should work.

view this post on Zulip Johan Commelin (Nov 03 2020 at 15:24):

typeclass arguments are implicit, so you typically can't use them with projection notation.

view this post on Zulip Chris M (Nov 03 2020 at 15:32):

thanks :)

view this post on Zulip Chris M (Nov 03 2020 at 15:52):

Actually a related weird problem :

open nat

section FinT
class FinT (T:Type*)  :=
(n:nat) (emb:T  nat) (embinv:nat  T) (finite: t, emb t < n) (bijective:  t, embinv (emb t) = t)
end FinT

open FinT

def summation (T:Type*) (f:(T  Prop)  nat) [h:FinT T]: T  nat := fun t:T,
let n:nat := (emb t) in
match n with
| (succ k) := 3
| zero := 4
end


def summeasure (f:nat  nat) : nat  nat
| (succ k) := f(succ k) + summeasure k
| zero     := f zero

open decidable
def pred_to_count {T:Type*} (f:T  Prop) [h:t, decidable (f t)]: T  nat := fun t:T, if h:(f t) then 1 else 0

def sumprednat (P:nat  Prop) [h:t, decidable (P t)] : nat  nat := fun n:nat, summeasure (pred_to_count P) n

def sumpred {T:Type*}[FinT T] (P:T  Prop) [h:t, decidable (P t)] : nat  nat :=
let Q := (fun n:nat, P (FinT.embinv T n)) in
fun n:nat, summeasure (pred_to_count Q) n

What is surprising to me about this, is that in the last definition, I have to write (FinT.embinv T n) instead of (FinT.embinv n) for it to type check. If I don't add it, I get the error

type mismatch at application
  embinv n
term
  n
has type
   : Type
but is expected to have type
  Type ? : Type (?+1)

Why is this, given that typeclasses are supposed to be implicit, and given that the same is not needed for let n:nat := (emb t) in in the earlier definition of summation?

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:53):

typeclasses are implicit, but the types are not (necessarily)

view this post on Zulip Mario Carneiro (Nov 03 2020 at 15:54):

if you want FinT.embinv to take T as implicit, write the field as (embinv {} : nat → T)

view this post on Zulip Chris M (Nov 03 2020 at 15:58):

ok that makes sense, thanks.


Last updated: May 09 2021 at 18:17 UTC