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](https://jozefg.bitbucket.io/posts/2015-01-08-modules.html#signatures)) - OCaml's `with type` ([OCaml Manual](https://ocaml.org/manual/modtypes.html#ss%3Amty-with)) - Rust's `Iterator` - Record patches in CoolTT ([Slides](https://cofree.coffee/~totbwf/slides/WITS-2022.pdf) | [Presentation Recording](https://www.youtube.com/watch?v=1_ZJIYu2BRk)) 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 `Format`s 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!