story
const post = {
id: 123,
content: "...",
published: true,
}
// TS infers the type of `post` to be an unnamed "map-ish" type:
// { id: number, content: string, published: boolean }
JS objects are map-like, and this one is "heterogenous" in that the values are of different types (unlike most maps in statically typed langs, which need to be uniform). this just "structural typing", the easier way to do stuff like this.now, dependent types allow you to express pretty much arbitrary shapes of data, so you can do heterogenous collections as well. i haven't read about it enough to do a map, but a list of tuples (equivalent if you squint) is "easy" enough:
[
("id", 123),
("content", "..."),
("published", True),
]
in Idris, you could type it as something like this: -- a function describing what type the values of each key are
postKeyValue : String -> Type
postKeyValue k =
case k of
"id" -> Int
"content" -> String
"published" -> Bool
_ -> Void -- i.e. "no other keys allowed"
-- now we're gonna use postKeyValue *at the type level*.
type Post = List (k : String ** postKeyValue k)
-- "a Post is a list of pairs `(key, val)` where the type of each `val` is given by applying `postKeyValue` to `key`.
-- (read `**` like a weird comma, indicating that this is a "dependent pair")
more on dependent pairs:
https://docs.idris-lang.org/en/latest/tutorial/typesfuns.htm...in general if you want to learn more about DT's, i'd probably recommend looking at a language like Idris with "native support" for them. backporting DT's onto an existing typesystem usually makes them much harder to read/understand that they actually are (and don't get me wrong, they're mindbending enough on their own).
if you don't want to bother with that, i'd look at Typescript - it's combination of "literal types", "type guards" and "function overloads" can get you some of the power of DT's. see this article for some examples: https://www.javiercasas.com/articles/typescript-dependent-ty...