Conversation

yeah, something like that

putting words to my vague thoughts: we have lots of different types of strings but they're very ad hoc, e.g. "utf8 string", "ascii string", "bytestring", "valid identifier", "valid json string". these are all one-offs. is there a "string type family" that unifies all of these?

(usefully, i mean ... we could have a string type family indexed by a boolean predicates over bytestrings, but that seems not very helpful)

but also, viewing types semantically (and practically) as representations of prefix-free languages on bytestrings

Politicians' Ties Observe Our Pusillanimity

Currently my main interest in this stuff is binary data descriptions. Currently maessing around with a DSL that's kind of inspired by the Power of Pi and Pads/DDC but not sure about the approach.

@PTOOP

Is induction-recursion in your toolchain? Choosing a particular encoding of a type will tend to involve more information than specifying what the type is, even if you don’t want it to.

I am not sure tbh! 😳 I was thinking I would try to avoid exposing an eliminator of the format descriptions to users. Like, I have introductions for the format descriptions, and a primitive that gets the representation of the data descriptions, for data-dependent formats.

Thing I've been wondering about is stuff like escape hatches, and different ways of parsing - like sometimes you want to be able to stream stuff, sometimes you want to use the format like a random access database with caching… sometimes a combination