% Extensible sum types
% [Public domain]

\input birdstyle

\birdleftrule=1pt
\emergencystretch=1em

\def\hugebreak{\penalty-600\vskip 30pt plus 8pt minus 4pt\relax}
\newcount\chapno
\def\: #1.{\advance\chapno by 1\relax\hugebreak{\bf\S\the\chapno. #1. }}

\: Introduction. This module implements extensible sum types, which means
you can do something like a datatype where you can add additional
constructors even in other modules.

> {-# LANGUAGE FunctionalDependencies, GADTs, RankNTypes, TypeFamilies #-}
> {-# LANGUAGE MultiParamTypeClasses, DeriveDataTypeable #-}

> module Data.Extensible.Sum (
>   ExtSum(..), ExtSumC(..), SumSelector(..), callExtSum, nextExtSum,
>   castExtSum, selectExtSum, lensExtSum
> ) where {

> import Control.Applicative;
> import Control.Monad;
> import Data.Lens.Common;
> import Data.Typeable;
> import GHC.Exts (Any);
> import Unsafe.Coerce;

\: Implementation. This implementation is based on a constrained dependent
sum type; there is a tag and then the value it corresponds to which is set
up by the instances of that class.

> data ExtSum s where {
>   ExtSum :: forall s x. ExtSumC s x => x -> ExtSumF x -> ExtSum s;
> } deriving Typeable;

There are no special laws that need to be satisfied with instances of this
class.

> class (Eq x, Typeable x) => ExtSumC s x | x -> s where {
>   type ExtSumF x :: *;
>   accessExtSum :: x -> ExtSumF x -> (s, s -> x);
> };

This type is used for selectors. A selector is used to convert a value of
one of the choices for an extensible sum into a value of a single type.

> data SumSelector s v where {
>   (:+?) :: forall s x v. ExtSumC s x =>
>    x -> (ExtSumF x -> v) -> SumSelector s v;
> };

> infix 0 :+?;

\: Functions.

{\tt callExtSum}: Can access the value of the single type which it
corresponds to. This type might even be an extensible product type.

> callExtSum :: ExtSum s -> s;
> callExtSum (ExtSum x y) = fst (accessExtSum x y);

{\tt nextExtSum}: Make a change in the selector. This is not generally a
functor.

> nextExtSum :: (s -> s) -> ExtSum s -> ExtSum s;
> nextExtSum f (ExtSum x y) = let { (a, b) = accessExtSum x y; } in
>  ExtSum (b $ f a) y;

{\tt castExtSum}: Ask the constructor, and will make the value if that is
the one which is active.

> castExtSum :: ExtSumC s x => ExtSum s -> x -> Maybe (ExtSumF x);
> castExtSum (ExtSum x y) t = unsafeCoerce y
>  <$ guard (typeOf x == typeOf t && x == unsafeCoerce t);

{\tt selectExtSum}: Given a list of selectors, take the value selected
from the extensible sum value, and apply the selector.

> selectExtSum :: [SumSelector s v] -> ExtSum s -> Maybe v;
> selectExtSum [] _ = Nothing;
> selectExtSum ((n :+? f) : t) x = (f <$> castExtSum x n)
>  <|> selectExtSum t x;

{\tt lensExtSum}: Make a lens of an extensible sum type.

> lensExtSum :: Lens (ExtSum s) s;
> lensExtSum = lens callExtSum $ nextExtSum . const;

% End of document (final "}" is suppressed from printout)
\medskip\centerline{The End}
\toks0={{

> } -- }\bye