True isomorphisms in Haskell

Question

Are the following assertions true:

1. The only real isomorphism, accessible programatically to the user, verified by Haskell type system, and that the Haskell compiler is/can be made aware of, is between:

   • the set of values of a Haskell datatype
   • the set of values of types those required by its constructors

2. Even generic programming can't produce "true" isomorphism, whose composition results at run time in an identity (thus staged-sop - and similarly in Ocaml)

3. Haskell itself is the only producing isomorphism, Coercible, but those isomorphism are restricted to the identity isomorphism

By "real isomorphism, accessible programatically to the user, verified by Haskell type system, and that the Haskell compiler is/can be made aware of" I mean a pair of function u : a -> b and v : b -> a such that Haskell knows (by being informed or otherwise) that u.v=id and v.u=id. Just like it knows (at compile time) how to rewrite some code to do "fold fusion", which is akin to, at once, recognize and apply it.

Answer 1

Look into Homotopy Type Theory/Cubical Agda where an "equality is isomorphism". I am not familiar enough with it to know what happens operationally, even if Agda knows isomorphic types are equal I still think your "true isomorphism" (i.e. with a proof and fusion) is too tall of an order.

In GHC it is possible to derive via "isomorphisms" but we need to wait for dependent types to properly verify isomorphisms in the type system. Even so they can be used to produce bone fide code even if you have to do some work operationally.

---

You already mentioned "representational equality" (Coercible) but it is worth discussing it. It underpins the two coerce-based deriving strategies: GeneralizedNewtypeDeriving and DerivingVia which generalizes GND.

GND is the simplest way to turn an isomorphism (Coercible USD Int) into code:

type    USD :: Type
newtype USD = MkUSD Int
  deriving
  newtype (Eq, Ord, Show, Num)

Operationally coerce is zero-cost at so they incur no cost at run-time. This is the only way you will get what you want in Haskell.

---

Isomorphisms can also be done through user-defined type classes.

An instance of Representable f means f is (naturally) isomorphic to functions from its representing object (Rep f ->). The newtype Co uses this isomorphism to derive function instances for representable functor. A Pair a of two values is represented by Bool, and is thus isomorphic to Bool -> a.

This isomorphism lets Pair derive Functor, Applicative and Monad by roundtripping through (Bool ->):

type Pair :: Type -> Type
data Pair a = a :# a
  deriving (Functor, Applicative, Monad)
  via Co Pair

instance Distributive Pair where
  distribute :: Functor f => f (Pair a) -> Pair (f a)
  distribute = distributeRep

instance Representable Pair where
  type Rep Pair = Bool

  index :: Pair a -> (Bool -> a)
  index (false :# true) = \case
    False -> false
    True  -> true

  tabulate :: (Bool -> a) -> Pair a
  tabulate make = make False :# make True

---

When you derive Generic/Generic1 the compiler generates an isomorphism between a generic type and its generic representation Rep/Rep1 (not to be confused with the representing object Rep from the above example).

The class laws state that to/from and to1/from1 witness that isomorphism. The type system does not enforce these laws but if you derive them they should hold.

They are the main way to define generic implementations in Haskell. I recently introduced two newtypes Generically and Generically1 to base, as standard names for generic behaviour (use generic-data until the next GHC release). You can derive a generic isomorphism and programmatically use it in the next line without leaving the data declaration:

type Lists :: Type -> Type
data Lists a = Lists [a] [a] [a]
  deriving
  stock (Show, Generic, Generic1)

  deriving (Semigroup, Monoid)
  via Generically (Lists a)

  deriving (Functor, Applicative, Alternative)
  via Generically1 Lists

>> mempty @(Lists _)
Lists [] [] []
>> empty @Lists
Lists [] [] []
>> Lists "a" "b" "c" <> Lists "!" "." "?"
Lists "a!" "b." "c?"
>> pure @Lists 'a'
Lists "a" "a" "a"

You will however have to pay for the converstion cost, it's not as simple as adding {-# Rules "to/from" to . from = id #-} because the actual instances will appear with intermediate terms like to (from a <> from b). Even your "true isomorphisms" GHC could not fuse away the conversion since it's not of the form to . from.

---

There is also a library iso-deriving (blog) that allows deriving via arbitrary isomorphisms.