
18 Mar
2016
18 Mar
'16
5:25 p.m.
At present, currying and uncurrying at the type level doesn't seem to work terribly well. In particular, the kinds (a, b) -> c and a -> b -> c aren't really isomorphic, because (a, b) can be stuck. This makes some things (like expressing Atkey-style indexed functors in terms of McBride-style ones) rather awkward, and difficult or impossible to really get quite right. The thought came to me that maybe we could allow unlifted tuples to be promoted. Then something of the kind (# a, b #) would unconditionally unify with '(# a, b #). The restrictions on how values of unlifted tuple types can be used would presumably translate directly to restrictions on how types of unlifted tuple kind can be used. David Feuer