I’m coming at this problem of serialization/nested acsets/whatever from both sides; from “what seems nice mathematically” and from “what would be usable as a computer product”. Currently, where I’m at is this syntax for declaring a wiring diagram.
interface DPorts {
In : Fin
Out : Fin
}
data WD(DPorts) {
hole Content(DPorts)
} = MkWd {
Box : Fin
Ports : Box -> DPorts
Wire : Fin
src : Wire -> ((b: Elt(Box), Elt(Ports(b).Out)) + In)
tgt : Wire -> ((b: Elt(Box), Elt(Ports(b).In)) + Out)
content : (b: Box) -> Content(Ports(b))
}
An interface consists of a collection of finite sets. Then we can declare a data type based on an interface. This data type has some number of internal “abstract hole types”; here we just have the Content
hole. We then define a number of members. The collection of types Ty
for members are generated by the following operations.
-
Fin : Ty
(primitive) - Integers, strings, etc.
- If
X : Fin
, thenElt(X) : Ty
- If
A
is a finite set in scope, and in contexta: A
we haveT : Ty
, then(a : A) -> T : Ty
(pi type) - If
T : Ty
and in contextt: T
we haveS: Ty
, then(t: T, S) : Ty
(sigma type). This captures both record types and also sum types via syntactic sugar. - If
I
is an interface, then alsoI : Ty
. - If
I
is an interface with fieldx
, andi: I
, theni.x : Fin
. - If
H
is a hole type with interfaceI
, andi: I
, thenH(i) : Ty
This last thing is the weird part. The idea here is that an instance of WD
knows about the places where you could attach things, and tells you what the interface that those things need to satisfy is. But you don’t necessarily know what type of things those are! They could be other wiring diagrams, they could be systems. You should be able to serialize a wiring diagram separately from what goes in the holes.
The key thing here that distinguishes this from the dependent lambda calculus is that we only allow finite sets in the domain of pi types. This means that data is always serializable.
I don’t know if what I have written here is formalizable, but I hope that what I end up coming up with will at least be similar in spirit to this.