Are there structures in use which are a mix of directed and undirected graphs? I.e. the effective edge-set consists of both directed and undirected vertex pairs.
In the case that the graph is simple, you can maybe use two directed graphs to represent an undirected connection. But in general, if the number of edges counts, that doesn't work.
I'm reading 'Graph Theory - Bondy & Murty' and have two editions two decades apart in front of me. Comparing them, I've noticed that they switched from the definition "Graph := triple $(V,E,\psi)$ with vertices $v,w\in V$, edges $e\in E$ and edge-assignment $\psi(e)=\{u,v\}$ " to "Graph := pair $(V,E)$ with vertices and edges, and with assignment in the context/meta-language". Wikipedia suggest using the triple definition and also names a third definition with a multiset - which is then conceptually different, as the edge set $E$ are merely pairs of vertices themselves, $e=\{u,v\}$. Did they make this change because there is an established notation now? What do papers in the field use as definition? How to theorem provers implement graphs, typically?
This does exist; it's called a mixed graph.
However, I suspect the reason that these graphs are not very common is that in many scenarios, an undirected edge will be equivalent to two directed edges, one going in each direction.