Encoding Overlapping, Extensible Isomorphisms

ExtensibleIsomorphisms.markdown

• Continued in Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms

Reddit discussion

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

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)

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

Actually interesting applications

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:

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 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, Coercions, GHC.Generics, etc.

Addendum

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 Adjunctions / Actions.

Specialized classes for isomorphisms like Data.Metrology.Quantity.Quantity can be written and integrated into a chain of isomorphisms.

data Iso_Quantity :: quantity <-> a

instance (Quantity a, QuantityQu a ~ quantity) => Iso (Iso_Quantity :: quantity <-> a) where
  from :: quantity -> a
  from = fromQuantity

  to   :: a -> quantity
  to = toQuantity