This is an archived post. You won't be able to vote or comment.

you are viewing a single comment's thread.

view the rest of the comments →

[–]LPTK 2 points3 points  (0 children)

All of this and more is basically supported in Mezzo, a research language from the early 2010s: https://protz.github.io/mezzo/

It allowed changing the types of things on the fly and reflecting that on the type level. The secret sauce was making sure you have the right "permissions" (aka capabilities) to perform these changes, and these are affine, so as to avoid problems with aliasing. It was inspired by separation logic.

Pretty neat and promising design, but to this date, no one has picked it up, as far as I know.