An observation from my Haskell effect system project: inductive data structures are awesome, but as soon as you want your inductive data structure to be represented in memory as something other than a linked list, all of Haskell’s nice type system features go out the window.
Conversation
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?
16
3
36
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.
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
Show replies