Zulip Chat Archive

Stream: new members

Topic: How to define a field of a structure to have type class


view this post on Zulip Rui Liu (Dec 13 2020 at 01:09):

Can I somehow define a field of a structure to have particular type class(es)?

view this post on Zulip Alex J. Best (Dec 13 2020 at 02:09):

Can you give an example of what you want? I'm not sure what you mean

view this post on Zulip Rui Liu (Dec 13 2020 at 12:54):

Here's an example:

structure T :=
    mk :: (a: Type) (b : a)

def f {t: T}: bool := ite (t.b = t.b) tt ff

This code fails to compile and we need to explicitly decorate with type class decidable_eq.

structure T :=
    mk :: (a: Type) (b : a)

def f {t: T} [h: decidable_eq t.a]: bool := ite (t.b = t.b) tt ff

This is a lot of boilerplate if you have a lot of functions and you need to decorate all of them. What I want is something like this that decorates the field a as a type with decidable_eq class globally:

structure T :=
    mk :: (a: Type) [h: decidable_eq a] (b : a)

def f {t: T} : bool := ite (t.b = t.b) tt ff

However this doesn't compile, so what's the correct way to do it?

view this post on Zulip Kevin Buzzard (Dec 13 2020 at 15:02):

Add the missing instance after the definition of the structure

view this post on Zulip Kevin Buzzard (Dec 13 2020 at 15:03):

Unrelated -- it's hard to imagine the unifier ever being able to figure out t -- maybe round brackets would be better

view this post on Zulip Rui Liu (Dec 13 2020 at 20:39):

That works!

view this post on Zulip Eric Wieser (Dec 13 2020 at 20:58):

Shorter to write attribute [instance] T.h, which I think also works


Last updated: May 13 2021 at 17:42 UTC