keywords: open union, extensible union, extensible datatypes

extensible-union-test.hs

{-# LANGUAGE RankNTypes, KindSignatures, TypeOperators, GADTs, ScopedTypeVariables,
             FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverlappingInstances #-}

import Data.Functor
import Control.Applicative -- for several functor instances

-- open union
infixr 1 :>
data (a :: * -> *) :> b

data Union r v where
  Inl :: Functor t => Union b v -> Union (t :> b) v
  Inr :: Functor t => t v -> Union (t :> b) v

instance (Show (t v), Show (Union b v)) => Show (Union (t :> b) v) where
  show (Inl u) = "Inl " ++ show u
  show (Inr tv) = "Inr " ++ show tv

instance Functor (Union r) where
  fmap f (Inl u) = Inl (fmap f u)
  fmap f (Inr x) = Inr (fmap f x)

class Member t r where
  inj :: Functor t => t v -> Union r v
  prj :: Functor t => Union r v -> Maybe (t v)

instance Member t (t :> r) where
  -- inj :: t v -> Union (t :> r) v
  inj tv = Inr tv
  -- prj :: Union (t :> r) v -> Maybe (t v)
  prj (Inr tv) = Just tv
  prj (Inl _)  = Nothing

instance (Functor t', Member t r) => Member t (t' :> r) where
  -- inj :: Member t r => t v -> Union (t' :> r) v
  inj tv = Inl (inj tv)
  -- prj :: Member t r => Union (t' :> r) v -> Maybe (t v)
  prj (Inr _) = Nothing
  prj (Inl u) = prj u

decomp :: Functor t => Union (t :> r) v -> Either (Union r v) (t v)
decomp (Inl u) = Left u
decomp (Inr tv) = Right tv

-- helper definitions

newtype Func a = Func a
data Void -- for the bottom of the `:>` chain, similar to `nil`

instance Show (Union Void a) where
  show _ = undefined

instance Functor Func where
  fmap f (Func x) = Func (f x)

instance Show a => Show (Func a) where
  show (Func a) = show a

unTrue :: Union (Maybe :> Either Char :> Func :> Void) Bool
unTrue = inj (Func True)

unFalse :: Union (Maybe :> Either Char :> Func :> Void) Bool
unFalse = inj (Just False)

un2 :: Union (Maybe :> Func :> Either Char :> Func :> Void) Int
un2 = inj (Func 5)

fr2 :: Maybe (Func Int)
fr2 = prj un2

frTrue :: Maybe (Func Bool)
frTrue = prj unTrue

frFalse1 :: Maybe (Func Bool)
frFalse1 = prj unFalse

frFalse2 :: Maybe (Maybe Bool)
frFalse2 = prj unFalse