Open AshleyYakeley opened 2 years ago
map @T: (a -> b) -> T a -> T b
map @T: (a -> b) -> T {-x,+a} -> T {-x,+b}
contramap @T: (a -> b) -> T b -> T a
contramap @T: (a -> b) -> T {-b,+x} -> T {-a,+x}
Given type T +w {-x,+y} -z:
T +w {-x,+y} -z
map @T: (a -> b) -> T a {-x,+y} z -> T b {-x,+y} z
contramap @(T w): (a -> b) -> T w {-b,+y} z -> T w {-a,+y} z
map @(T w): (a -> b) -> T w {-x,+a} z -> T b {-x,+b} z
contramap @(T w {-x,+y}): (a -> b) -> T w {-x,+y} b -> T w {-x,+y} a
Note that this is the only time we have partially-applied ground types, which might be awkward.
map @T: (a -> b) -> T a -> T bmap @T: (a -> b) -> T {-x,+a} -> T {-x,+b}contramap @T: (a -> b) -> T b -> T acontramap @T: (a -> b) -> T {-b,+x} -> T {-a,+x}Given type
T +w {-x,+y} -z:map @T: (a -> b) -> T a {-x,+y} z -> T b {-x,+y} zcontramap @(T w): (a -> b) -> T w {-b,+y} z -> T w {-a,+y} zmap @(T w): (a -> b) -> T w {-x,+a} z -> T b {-x,+b} zcontramap @(T w {-x,+y}): (a -> b) -> T w {-x,+y} b -> T w {-x,+y} aNote that this is the only time we have partially-applied ground types, which might be awkward.