Coercible
Just use quantified constraints
2021/12/12
Coercible
redesign
I want to get rid of “roles” as a hardcoded feature. I donʼt know of anyone proposing a solid theory of higher-order roles yet. But itʼs not necessary, in any case: itʼs much better to use quantified constraints.
tl;dr:
Coercible
then is also generated using transitivity and reflexivity and application: Coercible f g => forall a. Coercible (f a) (g a)
Some notes on what I was trying in Haskell: https://gist.github.com/MonoidMusician/30813fb645abe0cef9cc5ec6efe16b10
so I was thinking about what evidence you actually get from a role, within the system, and I think it’s literally just quantified constraints, and this will basically give us higher order roles when we need it (especially for things like monad transformers) if you declare a single-parameter functor to have a role, this is the evidence you get:
type Phantom f = forall a b. Coercible (f a) (f b)
type Representational f = forall a b. Coercible a b => Coercible (f a) (f b)
type Nominal f = forall a b. a ~ b => Coercible (f a) (f b)
roles are used for setting up what coercible instances there are, but within the system, you cannot actually distinguish between a particular role and these quantified constraints, I believe
then the idea is that for representational types, the instances are like … the simplest thing
you can read it right off the datatype
for data CoEnvT x m a = Single x | Higher (m a)
the instance is (Coercible x y, Coercible (m a) (n b)) => Coercible (CoEnvT x m a) (CoEnvT y n b)
you just coerce all the corresponding fields, and you don’t have to reduce the Coercible constraints at all: you don’t have to guess if m
and n
have to have representational or not
this might require the other thing I was saying where instances need to be bi-implications: it would be great if Coercible (CoEnvT x m a) (CoEnvT y n b)
would also imply Coercible (m a) (n b)
for example
things are a little trickier for recursive things: data Free f a = Pure a | Wrap (f (Free f a))
mechanically would have instance (Coercible a b, Coercible (f (Free f a)) (g (Free g b))) => Coercible (Free f a) (Free g b)
, but I think for representational f
and g
there might be problems with infinite instances … but note that you can reduce it to (Coercible a b, (forall x y. Coercible x y => Coercible (f x) (g y))) => Coercible (Free f a) (Free g b)
to break the cycle
(this might not be a problem in Haskell, but I would definitely worry about it in PureScript)
this eliminates a weird thing where newtypes and data worked differently wrt coercibility: it was always the case that newtype App f a = App (f a)
effectively has instance Coercible (f a) (g b) => Coercible (App f a) (App g b)
by transitivity of Coercible; namely, unwrapping and rewrapping
so I would like that for all datatypes
and also helps out with the whole discussion around monad/functor coercing, yeah
Coercible and polymorphic subsumption donʼt play well together?
lmap :: forall p a b. (FunctorOf Op ((->) ~> (->)) p) => (a -> b) -> forall x. p b x -> p a x
= coerce (map @_ @_ @p (Op f)) lmap f
• Couldn't match representation of type: forall x1.
p b x1 -> p a x1
with that of: p b x -> p a x
arising from a use of ‘coerce’