Are there any languages that can decouple logical representation from physical representation in this way? The only language I can think of that might be able to do it is ATS, but I don’t know ATS. Can I write an inductive GADT that is represented as a packed array in ATS?
Conversation
I have often thought about this - about ways to decouple the declarative structure from the physical representation. I want to be able to declare my inductive type, but also have multiple ways of translating that into some target memory layout in a way that's not too onerous.
1
3
Kind of reminds me a little of the SoA and AoS layout polymorphism stuff. There was this paper: ”You Can Have It All: Abstraction and Good Cache Performance” jupvfranco.github.io/papers/2017/on
2
2
I'd also be interested in how datatype description stuff like levitation fits in here: jupvfranco.github.io/papers/2017/on - perhaps one could use it as a way to decouple the datatype description from different instantiations of it… I dunno, I'm not super knowledgeable on it. cc.
1
This Tweet is from a suspended account. Learn more
Oh cool! I’ve been hoping to use something like that in Pikelet (although in probably a less rigorous form). Currently trying to learn about how multistage programming fits in. Seems kind if handy for offline partial evaluation I think?
2
You could then have some user-defined struct/union packing algorithms that could run at compile time on datatype descriptions, that could figure out how to lay things out, and assign tag bits, etc.
1
and I were discussing similar ideas, seeing if the modality in twitter.com/dannygratzer/s might work for this kind of staging. Unfortunately con_nat [pg9] is not very staging-friendly, and it's not clear how to rule it out in a reasonable way.
Quote Tweet
I'll be talking about Implementing a Modal Dependent Type Theory, looking forward to seeing people there!
preprint: jozefg.github.io/papers/2019-im
Show this thread
1
András had some other ideas based on universe levels, the naive version of which had the problem of not being able to distinguish compile-time from runtime booleans (e.g.); I don't remember if the more sophisticated attempts had better success.
1
Since then there's this: arxiv.org/pdf/1908.02035 I haven't read it, seems a bit syntax-heavy and probably a different flavor (more MetaOCaml-like) than what I'd like to have.
1
Yeah, I saw that one! They had a talk on it at POPL: youtube.com/watch?v=gCsb1a Thought the cross-stage persistence and quoting/unquoting seemed pretty neat and useful! What do you mean by 'syntax-heavy'? Curious about what you would want to do differently and why.
It'd be nice to have a small algebraic notion of model, like in arxiv.org/abs/1804.05236. I'd be content to not have any quoting/unquoting, just to have guaranteed static evaluation for a stage, and some sufficiently nice algebraic presentation.
