My initial motivation for
-XDerivingVia was deriving across
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
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
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
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
data ISO k :: k -> k -> Type type a <-> b = ISO Type 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)
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
Actually interesting applications
To derive interesting properties, we need to move from the world of
Type) to the world of type constructors and functors (
Type -> Type) so the encoding of our isomorphism kind becomes:
type f <~> g = ISO (Type -> Type) 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
f and functions from their representing object (
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
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,
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