%include lhs2TeX.fmt
%include WKlhs.sty
\section{Type Combinators}

%{-# OPTIONS_GHC -fglasgow-exts #-}  taken out for lhs2tex
\begin{code}
module TypeCombinators where

import Data.Typeable
\end{code}

\begin{code}
type GenEQ f = forall a b . f a -> f b -> Bool

class GenEq (f :: * -> *) where genEq :: GenEQ f
\end{code}

%{{{ I
Since |Control.Monad.Identity.Identity| has no |Typeable| instance,
and also because of its verbosity,
we define our own identity type constructor:

\begin{code}
newtype I a = I {unI :: a}   deriving (Eq, Ord, Typeable)

instance Functor   I where  fmap f (I a) = I (f a)
instance Monad     I where
  return = I
  I x >>= f  =  f x
  fail = error
\end{code}
%}}}

%{{{ K
\begin{code}
newtype K a b = K {unK :: a}   deriving (Eq, Typeable)

instance Functor   (K a) where  fmap f (K a) = K a

instance Ord a => Ord (K a b) where
  compare (K x) (K y) = compare x y
  K x <= K y = x <= y
\end{code}
%}}}

%{{{ Flip
For |Flip| and the following combinators,
it is not possible (with GHC-6.4) to use
|deriving Typeable| since the argument |f :: * -> *|
has higher kind.

\begin{code}
newtype Flip f a b = Flip {unFlip :: f b a}   deriving (Eq, Ord)

tcFlip = mkTyCon "TIUtils.Flip"
instance (Typeable2 f) => Typeable2 (Flip f) where
  typeOf2 (_ :: Flip f a b) = mkTyConApp tcFlip
     [typeOf2 (undefined :: f b a)
     ]
\end{code}
%}}}

%{{{ Flip_1_0
\begin{code}
newtype Flip_1_0 f a (c :: * -> *) = Flip_1_0 {unFlip_1_0 :: f c a}   deriving (Eq, Ord)
\end{code}
%}}}

%{{{ Flip_2_0
\begin{code}
newtype Flip_2_0 f a (c :: * -> * -> *) = Flip_2_0 {unFlip_2_0 :: f c a}   deriving (Eq, Ord)
\end{code}
%}}}

%{{{ B
\begin{code}
newtype B f g a = B {unB :: f (g a)}    deriving (Eq, Ord)

tcB = mkTyCon "TIUtils.B"
instance (Typeable1 f, Typeable1 g) => Typeable1 (B f g) where
  typeOf1 (_ :: B f g a) = mkTyConApp tcB
     [typeOf1 (undefined :: f (g a))
     ,typeOf1 (undefined :: g a)
     ]
\end{code}
%}}}

%{{{ B_1
\begin{code}
newtype B_1 f g (c :: * -> *) = B_1 {unB_1 :: f (g c)}    deriving (Eq, Ord)
\end{code}
%}}}

%{{{ B_2_0
\begin{code}
newtype B_2_0 f (g :: * -> * -> *) a = B_2_0 {unB_2_0 :: f (g a)}    deriving (Eq, Ord)
\end{code}
%}}}

%{{{ B1
\begin{code}
newtype B1 f g a b = B1 {unB1 :: f (g a b)}    deriving (Eq, Ord)

tcB1 = mkTyCon "TIUtils.B1"
instance (Typeable1 f, Typeable2 g) => Typeable2 (B1 f g) where
  typeOf2 (_ :: B1 f g a b) = mkTyConApp tcB
     [typeOf1 (undefined :: f (g a b))
     ,typeOf2 (undefined :: g a b)
     ]
\end{code}
%}}}

%{{{ Rot_1_0_0
\begin{code}
newtype Rot_1_0_0 f a b (c :: * -> *) = Rot_1_0_0 {unRot_1_0_0 :: f c a b}   deriving (Eq, Ord)
newtype Rot_2_0_0 f a b (c :: * -> * -> *) = Rot_2_0_0 {unRot_2_0_0 :: f c a b}   deriving (Eq, Ord)
\end{code}
%}}}

%{{{ S
\begin{code}
newtype S f g a = S {unS :: f a (g a)}    deriving (Eq, Ord)

tcS = mkTyCon "TypeCombinators.S"
instance (Typeable2 f, Typeable1 g) => Typeable1 (S f g) where
  typeOf1 (_ :: S f g a) = mkTyConApp tcS
     [typeOf2 (undefined :: f a (g a))
     ,typeOf1 (undefined :: g a)
     ]
\end{code}
%}}}

%{{{ EMACS lv
% Local Variables:
% folded-file: t
% fold-internal-margins: 0
% eval: (fold-set-marks "%{{{ " "%}}}")
% eval: (fold-whole-buffer)
% end:
%}}}