Stream: new members

Topic: Understanding Type Classes

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:

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) α] :=

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'"?

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.

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.

Eric Wieser (Dec 27 2020 at 13:03):

Worth also mentioning there is a #graph theory stream

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.

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?

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

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.

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"?

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.

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