This repository was archived by the owner on Nov 3, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 40
Typeability Bug in Reference Implementation #111
Comments
Good catch. This actually is another fall-out from our removal of subtyping. :( (Formerly, unreachable was typed with bottom, such that it was correct to accept this.) |
Oh whoa, I never even realized there had been a bottom value type. (It wasn't mentioned in the overview.) That causes problems as well. |
It was purely a spec-internal type, not expressible in the program itself. I actually mentioned it to you some time ago, and you didn't see any issues. See my presentation from the June '19 F2F meeting for the motivation. |
I understand. There's a difference between a bottom value type and a bottom state/result type. I thought you were referring to the latter concept. Sorry for the misunderstanding. |
Closed via #116. |
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
If I'm reading this code correctly, the reference interpretation incorrectly accepts this invalid instruction sequence:
The issue is that
select
is polymorphic with respect to numeric types only. So while the result type ofselect
afterunreachable
is unknown, it must at least be a numeric type. As such, it cannot be used for any instruction expecting a reference type.The reference interpreter seems to fail to incorporate this reasoning. Instead of using
value_type option
, the reference interpreter seems to need to use an ADT with an additional nullary case that represents only unknown numeric types.The text was updated successfully, but these errors were encountered: