One big motivation I've had for going with dependent types in the first place is the idea of being able to use the same language feature (dependent records) for both modules and data types. This is similar to what is proposed in 1ML, but I would prefer not to jump through the hoops of forcing the language into System Fω, and rather just go straight to dependent types, seeing as they are such a handy tool to have in the first place.
These would be super handy for representing modules. Eg.
Graph (a : Type) = Record {
Node : Type,
Edge : Type,
has-edge : a -> Node -> Node -> Bool,
edges : a -> Node -> List Edge,
}
MyGraph = DArray (Int, Int)
MyGraph-graph : Graph MyGraph
MyGraph-graph = record {
Node = Int,
Edge = (Int, Int),
has-edge = _,
edges = _,
}
This would also allow us to hide the length of length of arrays to get something like Rust's Vec
type:
DArray (a : Type) = Record {
len : U64,
data : Array a len,
};
Relationship with Sigma types
A very simple way of representing dependent records would be to use dependent pairs (sigma types):
Unit : Type
{} : Unit
{e1, e2} : (x : t1) * t2
left : (x : t1) * t2 -> t1
right : (x : t1) * t2 -> t2
Where t1
depends on t2
.
The trouble with this formulation is that labels are not significant when comparing for equality at the type and value level.
Structural vs Nominal
I would kind of prefer to go structural rather than nominal with this, but it seems that most dependently typed languages use nominal records. I'm guessing this is because it makes checking if two record types are compatible much easier. If we went structural we might need to do some complex subtyping and coercions to handle the fact that fields might be mentioned out of order.
In his thesis on Agda, Ulf Norel says:
In practise, however, it is a good idea to let each record declaration introduce a new type. This means that two record types declared to have the same fields will be different, but they will have the same elements. One advantage of this is that it significantly improves the efficiency of checking equality between record types—instead of comparing the types of all the fields, it is enough to compare the names. It is also good programming practise to keep intentionally different types separate in the type system.
Data layout
It would be nice if records were efficiently packed in memory by default, like Rust does it. The unboxed types issue #18 is related.
A potential issue with a non-uniform memory representation is that, as @ollef points out, if you have a record { x : A, y : B x, z : C }
, then the memory offset of z
depends on x
. We might be able to do some size analysis though, and require non-statically known sizes to have a pointer indirection.
If we allow structural types, data layout might become trickier. We might need to have a consistent 'normalized field order' for records. Things would become even more trickier if row polymorphism was brought into the mix.
Other stuff to consider wrt. data layout is struct of array and array of structs. Perhaps our compile time reflection would be powerful enough to auto-derive this, but langs like Jai have this built in.
This paper talks about some interesting ways to parameterise over data layout: https://www.doc.ic.ac.uk/~scd/ShapesOnwards.pdf
Here is a book going through Data Oriented Design.
Row polymorphism
It would be nice to support row polymorphism, but I have no idea how this would look.
Haven't thought much about it. That paper uses subtyping. For row typing you might be able to do like { Γ; Θ={ y₀:B₀; ⋯ yₙ:Bₙ }; Δ[Γ, Θ] }
where Γ and Δ are treated as two separate row variables, Δ depends on Γ and Θ, and Θ is closed with respect to Γ. Not sure though.
First class labels
Labels are also interesting - I've never really liked the 'type level string' nature of record labels, especially once row polymorphism comes into play. Would be nice to have these be namespaced, sort of like how clojure.spec does it. Not sure what the ergonomics would look like though.
Lenses
Would we want to auto-generate these? If we had first class labels and row polymorphism I could see us being generate polymorphic lenses in a library, like how Purescript does it.
References