An implementation of anonymous sums (AKA variants) with O(1) access, without resorting to Typeable or unsafeCoerce.

Sum.hs

{-# LANGUAGE LambdaCase, GADTs #-}

module Sum where

import Data.Type.Equality ((:~:)(..))
import Data.Functor ((<&>))

type f ~> g = forall x. f x -> g x


-- The standard implementation.

{-
data Sum f xs where
  Here  :: f x      -> Sum f (x:xs)
  There :: Sum f xs -> Sum f (x:xs)

-- | O(n)
hmap :: f ~> g -> Sum f xs -> Sum g xs
hmap h = \case
  Here  fx -> Here (h fx)
  There hs -> There (hmap h hs)

class x <: xs where
  -- | O(n). Assumes @x@ does not appear in @xs@ more than once. If this
  --   assumption is violated and an @x@ occupies a position other than the
  --   first, `match` will fail to find it.
  match :: Sum f xs -> Maybe (f x)

instance {-# OVERLAPPING #-} x <: (x:xs) where
  match = \case
    Here  fx -> Just fx
    There _  -> Nothing

instance {-# OVERLAPPABLE #-} x <: xs => x <: (y:xs) where
  match = \case
    Here  _  -> Nothing
    There hs -> match hs
-}


-- An alternative implementation that pulls the data out of the nested
-- structure, allowing O(1) access to speed up some operations.

data Sum f xs where
  Sum :: x <: xs => f x -> Sum f xs

-- | O(1)
hmap :: f ~> g -> Sum f xs -> Sum g xs
hmap h (Sum fx) = Sum (h fx)

data Index x xs where
  IZ ::               Index x (x:xs)
  IS :: Index x xs -> Index x (y:xs)

(===) :: Index x xs -> Index y xs -> Maybe (x :~: y)
IZ    === IZ    = Just Refl
IS i1 === IS i2 = i1 === i2
_     === _     = Nothing
infix 2 ===

class                                    x <:    xs  where index :: Index x xs
instance {-# OVERLAPPING  #-}            x <: (x:xs) where index = IZ
instance {-# OVERLAPPABLE #-} x <: xs => x <: (y:xs) where index = IS index

-- | Still O(n) due to the need to compare the supplied and captured indices.
--   Probably slower than the other @match@.
match :: forall x xs f. x <: xs => Sum f xs -> Maybe (f x)
match (Sum (fy :: f y)) = index @x @xs === index @y @xs <&> \Refl -> fy