Type System & PL Twitter question:
What is a good name for the opposite of 'elaboration'? Ie. going from the core language back to the surface language. Some ideas:
- resugaring
- delaboration
- co-elaboration (collaboration? 🤪)
Conversation
Replying to
resugaring probably. are you thinking about the possibility of doing this in a structure preserving way or just making a morphism of this at all?
1
Hmm, not sure about what it would look like to do either of those. I wouldn't require `resugar(elaborate(concrete)) == concrete`, but I _would_ require `elaborate(resugar(core)) == core`, if that's what you're talking about?
1
Show replies
Replying to
I say delaboration only bc that's what it's called in the Idris compiler. I'm willing to spell it differently though. (de-elaboration, maybe?)
Resugaring is only a specific kind of delaboration, so I don't think that should be the overall opposite of elaboration.
1
2
Hehe, neat! I liked 'delaboration' because of the symmetry, and it was cute - nice to know that was thinking similarly. :3
1
1
Show replies
Replying to
Definitely not resugaring, because elaboration is typically more involved than desugaring.
1
4
Yeah, I used to use 'resugar' in another type checker, but that was before I had a proper elaborator, and really was just doing desugaring between the concrete and core languages, and type checking on the core.
Replying to
How about 'summarize'? Sounds a bit wacky to my ears, but does kinda' work as the opposite of 'elaborate' in plain English.
1
Replying to
I really like `delaboration` but for some reason `surfacing` stuck in my brain just now.
2
5
oooh I like that better than delaboration
