search

sweirich / trellys

Automatically exported from code.google.com/p/trellys
45 stars 6 forks source link

Update typing rules to be modal and #24

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Make sure the type system incorporates all the improvements from the "modal" 
stuff. Some of the new rules are already implemented, but we should make sure 
we get all of them.

Original issue reported on code.google.com by vilhelm....@gmail.com on 4 Jul 2011 at 10:45

GoogleCodeExporter commented 9 years ago 
In particular, the rule that requires a value restriction

G |-P v : A
-------------
G |-L v : A @ P

should be eased to allow the argument to be "valuable"

G |-P a : A     G |-L b : a terminates
---------------------------------------
G |-L a : A

Original comment by stephanie.weirich on 4 Jul 2011 at 11:00

GoogleCodeExporter commented 9 years ago

Original comment by stephanie.weirich on 4 Jul 2011 at 11:00