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.
Conversation
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?
1
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?
Oh, the usual excusable cheating. The semantics is done offstage. They let you write data descriptions in a language whose meaning is baked in. That’s a whole other game from defining both descriptions and their meanings at object level.
Bedtime for me.
2