bsum.hs

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}

import Data.Kind (Type)

data Tree a
  = Empty
  | Node a (Tree a) (Tree a)

data BSum :: Tree Type -> Type where
  End :: x -> BSum (Node x l r)
  Zero :: BSum t -> BSum (Node x t r)
  One :: BSum t -> BSum (Node x l t)

-- ex falso quodlibet
-- you can't construct a value of type BSum Empty
-- so if you have one, you can produce whatever you like
impossibleBSum :: BSum Empty -> a
impossibleBSum = \case

data Void

-- same as impossibleBSum, for void
impossibleVoid :: Void -> a
impossibleVoid = \case

type Leaf t = Node t Empty Empty

type Either' a b =
  BSum
    (Node Void
      (Leaf a)
      (Leaf b))

-- constructors
left :: a -> Either' a b
left = Zero . End

right :: b -> Either' a b
right = One . End

-- eliminator
either' :: (a -> c) -> (b -> c) -> Either' a b -> c
either' f g = \case
  End x -> impossibleVoid x
  Zero bt -> case bt of
     End x -> f x
     Zero l -> impossibleBSum l
     One r -> impossibleBSum r
  One bt -> case bt of
    End x -> g x
    Zero l -> impossibleBSum l
    One r -> impossibleBSum r

data FourAlt a b c d
  = A a
  | B b
  | C c
  | D d

type FourAlt' a b c d =
  BSum
    (Node Void
      (Node a
        Empty
        (Leaf c))
      (Node b
        Empty
        (Leaf d)))

-- constructors
injA :: a -> FourAlt' a b c d
injA = Zero . End

injB :: b -> FourAlt' a b c d
injB = One . End

injC :: c -> FourAlt' a b c d
injC = Zero . One . End

injD :: d -> FourAlt' a b c d
injD = One . One . End

-- eliminator
fourAlt' :: (a -> e) -> (b -> e) -> (c -> e) -> (d -> e) -> FourAlt' a b c d -> e
fourAlt' fa fb fc fd = \case
   End x -> impossibleVoid x
   Zero bt -> case bt of
      End x -> fa x
      Zero bt1 -> impossibleBSum bt1
      One bt1 -> case bt1 of
         End x -> fc x
         Zero bt2 -> impossibleBSum bt2
         One bt2 -> impossibleBSum bt2
   One bt -> case bt of
      End x -> fb x
      Zero bt1 -> impossibleBSum bt1
      One bt1 -> case bt1 of
         End x -> fd x
         Zero bt2 -> impossibleBSum bt2
         One bt2 -> impossibleBSum bt2