My initial motivation for -XDerivingVia
was deriving across
isomorphisms.
Standard type-class encodings of isos turn out to be awkward due to overlap.
class Iso a b where
from :: a -> b
to :: b -> a
There may be many different witnesses to an isomorphism between two types. We must choose between overlap and picking a single, canonical instance. boo
A value-level representation does not suffer from this problem (data a <-> b = Iso (a -> b) (b -> a)
) as the same isomorphism may have
different witnesses (Iso id id::Bool <-> Bool
v Iso not not::Bool <-> Bool
). This is the approach taken by the
lens
library and advocated for by Gabriel Gonzalez in
Scrap your type classes.
This does not work in our case: deriving
relies on type-directed
instance resolution, we cannot pass it values. It needs a type hint.
This hint comes in the form of a tag used to explicitly specify a
witness. The two tags TagId @Bool
and TagNot
witnesses the
isomorphism Bool <-> Bool
:
data a <-> b where
TagId :: a <-> a
TagNot :: Bool <-> Bool
TagComp :: (a <-> b) -> (b <-> c) -> (a <-> c)
-- ...
Then we create a type class indexed by these tags without any overlap
class Iso (tag::a <-> b) where
from :: a -> b
to :: b -> a
instance Iso (TagId::a <-> a) where
from, to :: a -> a
from = id
to = id
instance Iso (TagNot::Bool <-> Bool) where
from, to :: Bool -> Bool
from = not
to = not
instance (Iso iso, Iso iso') => Iso (TagComp iso iso'::a <-> c) where
from :: a -> c
from = from @_ @_ @iso' . from @_ @_ @iso
to :: c -> a
to = to @_ @_ @iso . to @_ @_ @iso'
But we have a problem: the kind a <-> b
is closed / not
extensible. Fortunately there is a trick used by Richard Eisenberg and
Jan Stolarek in the
singletons
library (subsection 4.3.1 The kind ->> of
Promoting Functions to Type Families in Haskell)
that allows faking open kinds: Instead of defining a <-> b
as its
own datatype we define it as a type synonym, ending in Type
type a <-> b = (a, b) -> Type
And we can introduce meaningless type-level constants to witness an isomorphism:
data TagId :: a <-> a
data TagNot :: Bool <-> Bool
data TagComp :: (a <-> b) -> (b <-> c) -> (a <-> c)
The Iso
class and its instances still work, and our isomorphism kind
is extensible, explicit and at the type-level as we want:
data TagSwap :: (a, b) <-> (b, a)
data TagAssoc :: (a, (b, c)) <-> ((a, b), c)
data TagLUnit :: ((), a) <-> a
data TagRUnit :: (a, ()) <-> a
data TagFrom :: (a <-> b) -> (b <-> a)
instance Iso (TagSwap::(a, b) <-> (b, a)) where
from :: (a, b) -> (b, a)
from = swap
to :: (b, a) -> (a, b)
to = swap
instance Iso (TagAssoc::(a, (b, c)) <-> ((a, b), c)) where
from :: (a, (b, c)) -> ((a, b), c)
from (a, (b, c)) = ((a, b), c)
to :: ((a, b), c) -> (a, (b, c))
to ((a, b), c) = (a, (b, c))
instance Iso (TagLUnit::((), a) <-> a) where
from :: ((), a) -> a
from ((), a) = a
to :: a -> ((), a)
to a = ((), a)
instance Iso (TagRUnit::(a, ()) <-> a) where
from :: (a, ()) -> a
from (a, ()) = a
to :: a -> (a, ())
to a = (a, ())
instance Iso iso => Iso (TagFrom iso::b <-> a) where
from :: b -> a
from = to @_ @_ @iso
to :: a -> b
to = from @_ @_ @iso
To derive interesting properties, we need to move from the world of
types (Type
) to the world of type constructors and functors (Type -> Type
) so the encoding of our isomorphism kind becomes:
data Functors :: (Type -> Type) -> (Type -> Type) -> Type
type f <~> g = Functors f g -> Type
type f ~> g = forall xx. f xx -> g xx
class Iso1 (tag1::f <~> g) where
from1 :: f ~> g
to1 :: g ~> f
Allowing us to define an isomorphism between
Representable
functors
f
and functions from their representing object (Rep f
)
class Functor f => Representable f where
type Rep f :: Type
index :: f ~> (Rep f ->)
tabulate :: (Rep f ->) ~> f
data TagRepresentable :: f <~> rep
instance (Representable f, rep ~ (Rep f ->)) => Iso1 (TagRepresentable::f <~> rep) where
from1 :: f ~> (Rep f ->)
from1 = index
to1 :: (Rep f ->) ~> f
to1 = tabulate
Functions have a wealth of instances. If we have a representable functor (functor isomorphic to a function) it means we can derive these instances and more
instance Functor (a ->)
instance Applicative (a ->)
instance Monad (a ->)
instance Distributive (a ->)
instance Monoid a => Comonad (a ->)
-- ..
All we need to do is to define an adapter with a phantom tag,
instances that we want to derive through an Iso1
newtype AsIso1 f (iso1::f <~> f_other) a = AsIso1 (f a)
instance (Iso1 (iso1::f <~> f_other), Functor f_other) => Functor (AsIso1 f iso1) where
fmap :: (a -> a') -> (AsIso1 f iso1 a -> AsIso1 f iso1 a')
fmap f (AsIso1 fa) = AsIso1 (to1 @_ @_ @iso1 (fmap @f_other f (from1 @_ @_ @iso1 fa)))
instance (Iso1 (iso1::f <~> f_other), Applicative f_other) => Applicative (AsIso1 f iso1) where
pure :: a -> AsIso1 f iso1 a
pure a = AsIso1 (to1 @_ @_ @iso1 (pure @f_other a))
(<*>) :: AsIso1 f iso1 (a -> a') -> (AsIso1 f iso1 a -> AsIso1 f iso1 a')
AsIso1 mf <*> AsIso1 mx = AsIso1 (to1 @_ @_ @iso1 (from1 @_ @_ @iso1 mf <*> from1 @_ @_ @iso1 mx))
instance (Iso1 (iso1::f <~> f_other), Monad f_other) => Monad (AsIso1 f iso1) where
-- ...
and wait for -XDerivingVia
to get added to GHC ;-)
data Pair a = a :# a
deriving (Functor, Applicative, Monad, ...)
via (Pair `AsIso1` TagRepresentable)
instance Representable Pair where
type Rep Pair = Bool
index :: Pair ~> (Bool ->)
index (false :# true) = \case
False -> false
True -> true
tabulate :: (Bool ->) ~> Pair
tabulate generate = generate False :# generate True
This works for arbitrarily long chains of arbitrarily complicated isomorphisms, Coercion
s, GHC.Generics
, etc.
Can be made a Category
by forgetting the witness (tag):
type Cat ob = ob -> ob -> Type
data (<==>) :: Cat Type where
SomeIso :: Iso (tag::a <-> b) => Proxy tag -> a <==> b
instance Category (<==>) where
id :: a <==> a
id = SomeIso (Proxy @TagId)
(.) :: (b <==> c) -> (a <==> b) -> (a <==> c)
SomeIso (_ :: Proxy tag') . SomeIso (_ :: Proxy tag) = SomeIso (Proxy :: Proxy (TagComp tag tag'))
This is also ideal to encode Applicative
morphisms: I will write
another blogpost about that.
This may be a good way to define Adjunction
s / Action
s.
I like this