Zulip Chat Archive

Stream: new members

Topic: Understanding Type Classes


view this post on Zulip Marcus Rossel (Dec 27 2020 at 12:19):

Hi :wave: I've been having problems understanding type classes and how to use them.
I need to implement a digraph type which is generic over the type of its edges. My plan was to do something along the lines of:

-- The type returned by `ε` is the actual edge-type, which depends on the `nodes`.
-- The digraph's nodes (of type `α`) need to be accessible by index, which is why `nodes : ι → α`.
structure digraph (ι α : Type*) (ε : (ι  α)  Type*) :=
  (nodes : ι  α)
  (edges : finset (ε nodes))

Since it's supposed to be a digraph, I then wanted to enforce the edge-type to have a src : α and dst : α field. So I added this type class:

-- Type `ε` is a `digraph.edge`-type over `α`, if any instance of it can produce a `src` and `dst` element of type `α`.
class digraph.edge (ε α : Type*) :=
  (src : ε  α)
  (dst : ε  α)

What I can't figure out now, is how to combine this with the digraph type.
I want to constrain the type that is returned by (ε : (ι → α) → Type*) to be a digraph.edge.

How is this possible? Am I approaching this all wrong?
Thanks :pray:

view this post on Zulip Eric Wieser (Dec 27 2020 at 12:21):

I'm not sure it's a good idea, but you can achieve that with structure digraph (ι α : Type*) (ε : (ι → α) → Type*) [∀ f, digraph.edge (ε f) α] :=

view this post on Zulip Marcus Rossel (Dec 27 2020 at 12:25):

Eric Wieser said:

I'm not sure it's a good idea, but you can achieve that with structure digraph (ι α : Type*) (ε : (ι → α) → Type*) [∀ f, digraph.edge (ε f) α] :=

Would that mean that I require that for any instance of underlying nodes (called f here), it has to be possible to create an instance of type digraph.edge (ε f) α?


And now if I wanted to use this fact that ε nodes is "digraph.edge-able", how would I go about that? E.g. if I wanted to define the following:

def digraph.has_edge_from_to {ι α : Type*} (ε : (ι  α)  Type*) [ f, digraph.edge (ε f) α] (g : digraph ι α ε) (a a' : α) : Prop :=
     e  g.edges , e.src = a  e.dst = a'

... then I get errors on the terms e.src and e.dst, because:

invalid field notation, type is not of the form (C ...) where C is a constant
   e
has type
  ?m_1

How would I state this proposition "there exists and edge in the graph where the src is a and the dst is a'"?

view this post on Zulip Eric Wieser (Dec 27 2020 at 13:02):

You need to use digraph.edge.src e instead of e.src. e.src works if e has type foo and there is a definition foo.src. In your case, e is an unspecified type, so this does not work.

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

What is a digraph mathematically? All I know so far is that ε seems to be being used for two things. One should set it up properly first. Eric saying "this is probably a bad idea but here's a way to do it" doesn't strike me as being the best foundations for making a new type.

view this post on Zulip Eric Wieser (Dec 27 2020 at 13:03):

Worth also mentioning there is a #graph theory stream

view this post on Zulip Eric Wieser (Dec 27 2020 at 13:05):

Marcus Rossel said:

Eric Wieser said:

I'm not sure it's a good idea, but you can achieve that with structure digraph (ι α : Type*) (ε : (ι → α) → Type*) [∀ f, digraph.edge (ε f) α] :=

Would that mean that I require that for any instance of underlying nodes (called f here), it has to be possible to create an instance of type digraph.edge (ε f) α?

Yes, that's exactly how to read that.

view this post on Zulip Marcus Rossel (Dec 27 2020 at 13:34):

Eric Wieser said:

You need to use digraph.edge.src e instead of e.src. e.src works if e has type foo and there is a definition foo.src. In your case, e is an unspecified type, so this does not work.

Thanks that works :)
How is it that one can just write digraph.edge.src e without needing to specify digraph.edge's ε and α explicitly?

view this post on Zulip Eric Wieser (Dec 27 2020 at 13:35):

α is deduced from the a on the RHS of = in your theorem, while ε is deduced from the argument e

view this post on Zulip Marcus Rossel (Dec 27 2020 at 13:40):

Kevin Buzzard said:

What is a digraph mathematically? All I know so far is that ε seems to be being used for two things. One should set it up properly first. Eric saying "this is probably a bad idea but here's a way to do it" doesn't strike me as being the best foundations for making a new type.

Yes exactly, ε is being used for multiple things here. The reason (in my specific use case) is that I need to be able to attach some additional information to the edges, so I can't just have them be of type α × α. And the type of information that I can attach needs to be flexible. That's why I tried to define digraph in a way that allows the user to specify an own edge-type (with the constraint that it still needs to have a src and dst).
I'm not sure if this is approach is perhaps too computer science-ish (because that is my background) and doesn't fare well in the realm of mathematical definitions.

view this post on Zulip Eric Wieser (Dec 27 2020 at 13:44):

In your specific use case, can there be multiple edges between nodes A and B with distinct values of "additional information"?

view this post on Zulip Marcus Rossel (Dec 27 2020 at 13:45):

Eric Wieser said:

In your specific use case, can there be multiple edges between nodes A and B with distinct values of "additional information"?

Yes, precisely.

view this post on Zulip Eric Wieser (Dec 27 2020 at 13:46):

I think a more typical formulation would be α × α → set your_extra_data, but I understand why you're trying the approach you are


Last updated: May 14 2021 at 21:11 UTC