not all strings are valid, and that's beautiful
1
25
Conversation
thinking about dependently typed strings
2
14
Types of serialised data? 🤔
2
2
yeah, something like that
1
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?
2
3
(usefully, i mean ... we could have a string type family indexed by a boolean predicates over bytestrings, but that seems not very helpful)
1
but also, viewing types semantically (and practically) as representations of prefix-free languages on bytestrings
1
1
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.
1
1
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.
1
2
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.
1
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
And yeah I'm worried about those operational concerns leaking into the more declarative descriptions that I was hoping for, and it's all tricky gah
2
Sorry for probably missing the point of your question I'll try to think about it more and get back to you.