(usefully, i mean ... we could have a string type family indexed by a boolean predicates over bytestrings, but that seems not very helpful)
Conversation
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
1
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
IR is good at managing superficial data descriptions with a forgetful map to semantic data representations, in the presence of data dependency. Because if that ain’t respecting the semantics, you have bigger troubles.
1
1
Ohhhh so yeah I'm pretty sure my representation operation is defined inductive-recursively with the data descriptions. Pretty close to what is described in the Power of Pi, and looking at the Gentle art of Levitation at the end of last year I think there are similarities?
1
I was attempting for longer than I'll admit to trying to do some horrific subtyping thing with descriptions being supertypes of their representations and it was a world of pain.
2
I think starting off with "The Next 700 Data Description Languages" got me confused, as they use a type-like-syntax for their data descriptions. Which only really works if you are really careful I think?
Yes. Lovely stuff, but encoding it by hacking up a fancy notion of datatype behind the scenes is defo cheating. We can absorb…
1
1
Could you elaborate on why you think it is cheating? Because they aren't using a more general datatype definition thing to encode the data descriptions? Or is it that they don't preserve the data dependencies in the representation types? Or something else?
1
Show replies