suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

update rosette notes about Constant subtyping rule(s)

Browse Source
This commit is contained in:
Stephen Chang 2016-09-08 11:30:36 -04:00
parent 6ff4410841
commit 3495584667
1 changed files with 14 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
turnstile/examples/rosette/rosette-notes.txt
View File

@ -1,6 +1,6 @@
2016-09-08
Typed Rosette tricky subtyping examples
Typed Rosette tricky subtyping examples:
) Both these should be true:
@ -21,7 +21,19 @@ But then, (U (Constant Int)) <: (U Int), which should *not* hold.
Bad alternative: lift Constant out of U
Con: non-constant values, eg (if b i1 i2) will be recognized as "constant"
Current solution: disallow first case
*Current design choice*: disallow first case
Another alternative: get rid of Constant altogether?
SUMMARY:
Here are the above two cases in canonical form:
(Constant* (U* CInt)) <: (U* (Constant* (U* CInt)) (Constant* (U* CBool)))
(Constant* (U* CInt)) <: (U* CInt)
The problem is that each case requires a different rule but the outer type
constructors are insufficient for determining which rule use.
2016-09-02 --------------------