Follow
Hey @joey, what's your opinion on the fully abstract embedding criterion that these guys proposed? https://iris-project.org/pdfs/2021-popl-fae-gradual-final.pdf
It's surely tough to scale to e.g. python, but it also surely seems like the criterion one may want to have.
@dasnacl I think it's pretty important, you want static equivalences to be respected in your gradual language, so that if you refactor some static code you don't suddenly get changes in behaviour. Proving it is definitely tricky to scale to e.g. python, but I'm not aware of any barriers to it holding in general.
The ICFP19 paper doesn't have this property, e.g. because it compared types using definitional equality at run time, some statically-safe refactorings could trigger gradual errors.
The ICFP22 paper fixes this by not using definitional equality at run time, though I haven't yet proved that all static equivalences are respected.