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.
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?
This Tweet is from a suspended account. Learn more
Yeah, I’m still unsure how one might handle the multiple forms of modal necessity that you might want in a single systems lang. Like usage count, stage, free variables, etc. Trying to learn how Granule does it 🤔
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
Show replies