Data structures with holes

Research
1

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, then Elt(X) : Ty
  • If A is a finite set in scope, and in context a: A we have T : Ty, then (a : A) -> T : Ty (pi type)
  • If T : Ty and in context t: T we have S: 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 also I : Ty.
  • If I is an interface with field x, and i: I, then i.x : Fin.
  • If H is a hole type with interface I, and i: I, then H(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.