Understanding Type Classes

Stream: new members

[Marcus Rossel]

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]

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]

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]

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]

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]

Worth also mentioning there is a #graph theory stream

[Eric Wieser]

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]

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]

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

[Marcus Rossel]

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]

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

[Marcus Rossel]

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]

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