Implementation of end charts in Idris

I would like to implement finite directed graphs in Idris. Also I want to work with vertex maps f : V -> X

from a set of vertices to some other type / set. Which one would be the most natural?

One option is to always select Fin n

for a set of vertices. Thus, a graph can be directly implemented as its adjacency matrix, i.e. Graph n = Vect n (Vect n Bool)

, and any vertex mapping as a type vector Vect n a

.

On the other hand, I like the idea of ​​a definition Graph a = SortedMap (a, a) Bool

. In this way, several designs seem to be simpler, for example. product of a graph type Graph a -> Graph b -> Graph (a, b)

.

But then you can build malicious instances of the graph, where, for example, (x, y)

is a key g

, but is (y, x)

not. Also, if I want to write a function that takes a graph and a compatible vertex map, I don't know how to specify that the domains of both objects must match. Perhaps f : (g : Graph a) -> (m : SortedMap a b) -> {auto p : vertexList g = keys m} -> ...

where the functions vertexList

and keys

must be written first?

The third definition would be Graph a = (a, a) -> Bool

where there a

should be some final type of Fin n

or (Fin m, Fin n)

. Then the vertex maps would just be of type a -> b

.