Constrained representation types

[brendanzab]

It it might eventually be useful to be able to ‘constrain’ representation types using something like Format { Repr = ... } (this popped up in other approaches to figuring out the font tables).

This could allow us to write formats like:

• join16 : fun (len : U16) (A : Type) -> Array16 len (Format { Repr = A }) -> Format { Repr = Array16 len A }

As Fathom is based on intensional type theory implementing such a construct could require a bit of thought – I'm not entirely clear on what the interactions and difficulties are, or if there are ways to simplify this.

A weird connection to module systems and associated types

---

This reminds me a bit of a limited form of:

• where type in Standard ML (A Crash Course on ML Modules)
• OCaml's with type (OCaml Manual)
• Rust's Iterator<Item = T>
• Record patches in CoolTT (Slides | Presentation Recording)

This kind of makes sense if you imagine a Format to be a builtin/hard-coded module type:

let Format = {
    Repr : Type,
    decode : Decoder Repr,
    encode : Encoder Repr,
};

You could imagine extending this 'module' to support sizes too:

let Format = {
    Repr : Type,
    size : Size,
    decode : Decoder Repr size,
    encode : Encoder Repr size,
};

Note: I'm absolutely not recommending we implement Formats in this way - I just find it an interesting perspective!

---

[mikeday]

I'm having trouble understanding, what exactly does join16 do?

[brendanzab]

It parses an array of format descriptions that have a common representation, resulting in an array of that common representation type. It popped up back when I had the links to font_tables inside the table_records. It's less useful if you don't also have a way to map over format descriptions (say if not all the format representations were the same).

We might come up against some better motivating examples though, so I kind of just wanted to note this down in case.

[mikeday]

Oh right I see, so that input array is an array of formats... tricky to construct such a beast!