Changes between Version 6 and Version 7 of ImpredicativePolymorphism/Impredicative-2015


Ignore:
Timestamp:
Jul 9, 2015 9:02:52 PM (4 years ago)
Author:
heisenbug
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ImpredicativePolymorphism/Impredicative-2015

    v6 v7  
    166166=== Design choice: `InstanceOf` and `->` ===
    167167
    168 In the designed proposed above, `->` is treated as any other type constructor. That means that if we are canonicalizing `InstanceOf (sigma3 -> sigma4) (sigma1 -> sigma2), the result is `sigma1 ~ sigma3 /\ sigma2 ~ sigma4`. That is, `->` is treated invariantly in both arguments. Other possible design choices are:
     168In the designed proposed above, `->` is treated as any other type constructor. That means that if we are canonicalizing `InstanceOf (sigma3 -> sigma4) (sigma1 -> sigma2)`, the result is `sigma1 ~ sigma3 /\ sigma2 ~ sigma4`. That is, `->` is treated invariantly in both arguments. Other possible design choices are:
    169169
    170170* `->` treated co- and contravariantly, leading to `InstanceOf sigma3 sigma1 /\ InstanceOf sigma2 sigma4`.
    171 * Treat inly the co-domain covariantly, leading to `sigma1 ~ sigma3 /\ InstanceOf sigma2 sigma4`.
     171* Treat only the co-domain covariantly, leading to `sigma1 ~ sigma3 /\ InstanceOf sigma2 sigma4`.
    172172
    173173Which are the the benefits of each option?