Changes between Initial Version and Version 1 of Ticket #13358


Ignore:
Timestamp:
Mar 1, 2017 8:33:39 AM (3 years ago)
Author:
ezyang
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #13358 – Description

    initial v1  
    1414
    1515{{{
    16 type app  role T representational
    17 type proj role T representational
     16type role T representational..representational
    1817newtype T a = MkT a
    1918-- T a ~R T b implies a ~R b
    2019
    21 type app  role T nominal
    22 type proj role T representational
    23 -- NB: type proj role T nominal is NOT ALLOWED
     20type role T nominal..representational -- NB: nominal..nominal illegal!
    2421newtype T a = MkT a
    2522-- T a ~R T b implies a ~R b, BUT
    2623-- a ~R b is insufficient to prove T a ~R T b (you need a ~N b)
    2724
    28 type app role T nominal
    29 type proj role T phantom -- (representational and nominal not allowed)
     25type role T nominal..phantom -- NB: nominal..representational illegal!
    3026newtype T a = MkT Int
    3127-- T a ~R T b implies a ~P b (i.e. we don't learn anything)