# Zulip Chat Archive

## 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 **di**graph, 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