LSLeary · August 12, 2024 10:29
diff --git a/Sum.hs b/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
	{-# 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