%include lhs2TeX.fmt
%include WKlhs.sty
\section{Home-made |Typeable|}

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

import TI
import NatNum
import TypeCombinators
import Control.Monad (liftM )
\end{code}

This module is currently happily restricting itself to Glasgow Haskell.
Many things that are done in a more portable way in |Data.Typeable|
are done in a more concise, but GHC-specific way here.

For the tyme being, we only go to |Typeable3|,
while |Data.Typeable| goes all the way to |Typeable7|.

\begin{code}
class Typeable  a where typeIndex  ::       a -> TI a
class Typeable1 t where typeIndex1 ::     t a -> TI1 t
class Typeable2 t where typeIndex2 ::   t a b -> TI2 t
class Typeable3 t where typeIndex3 :: t a b c -> TI3 t
\end{code}

At the core of Tomasz Zielonka's GADT-based implementation
of typesafe cast are two cast functions
(corresponding to |tiCast| and |tiGCast|)
that take type indices for the involved types as parameters.
We generalise this here to higher kinds,
following the organisation of |TI|.
(Tomasz Zielonka uses the |MonadZero| in |MonadPlus|;
 I use the |MonadZero| in |Monad|.)

\begin{code}
tiCast :: Monad m => TI a -> TI b -> a -> m b
tiCast ta tb x  = liftM unI $ tiGCast ta tb $ I x
\end{code}

\begin{code}
tiGCast :: Monad m => TI a -> TI b -> f a -> m (f b)
tiGCast Triv        Triv          x = return x
tiGCast Bool        Bool          x = return x
tiGCast Char        Char          x = return x
tiGCast Nat         Nat           x = return x
tiGCast Int         Int           x = return x
tiGCast Integer     Integer       x = return x
tiGCast Float       Float         x = return x
tiGCast Double      Double        x = return x
tiGCast (Apply_0 t a) (Apply_0 t' a') x = do
  x' <- liftM unFlip_1_0 (tiGCast_0 t t' (Flip_1_0 (B x)))
  liftM unB (tiGCast a a' x')
tiGCast (Apply_1 t c) (Apply_1 t' c') x = do
  x' <- tiGCast_1 t t' x
  liftM unB_1 (tiGCast_0 c c' (B_1 x'))
tiGCast _         _               _ = fail "tiGCast"
\end{code}

While Tomasz Zielonka leaves type constructors
in inner positions in his |Wrapper*| types,
we expose them into last position,
which makes the following functions also useful
for the case of higher-kinded constructors,
see the |Apply_1| case above.

\begin{code}
tiGCast_0 :: Monad m => TI_0 t -> TI_0 u -> f t -> m (f u)
tiGCast_0 Maybe Maybe x = return x
tiGCast_0 List  List  x = return x
tiGCast_0 (Apply_0_0 t a) (Apply_0_0 t' a') x = do
  x' <- liftM unFlip_2_0 $ tiGCast_0_0 t t' $ Flip_2_0 $ B_2_0 x
  liftM unB_2_0 (tiGCast a a' x')
tiGCast_0 _         _               _ = fail "tiGCast_0"
\end{code}

\begin{code}
tiGCast_0_0 :: Monad m => TI_0_0 t -> TI_0_0 u -> f t -> m (f u)
tiGCast_0_0 Either Either x = return x
tiGCast_0_0 Pair   Pair   x = return x
tiGCast_0_0 Fct    Fct    x = return x
tiGCast_0_0 _      _      _ = fail "tiGCast_0_0"
\end{code}

\begin{code}
tiGCast_1 :: Monad m => TI_1 t -> TI_1 u -> f (t c) -> m (f (u c))
tiGCast_1 Fix Fix x = return x
-- |tiGCast_1 _   _   _ = fail "tiGCast_1"|      -- currently not needed
\end{code}

We shamelessly use scoped type variables
to abbreviate the |cast| and |gcast| definitions,
(|Data.Typeable| uses more portable ways.)

\begin{code}
cast :: (Typeable a, Typeable b) => a -> Maybe b
cast a :: Maybe b = tiCast (typeIndex a) (typeIndex (undefined :: b)) a
\end{code}

\begin{code}
gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b)
gcast (x :: c a) :: Maybe (c' b)  tiGCast (typeIndex (undefined :: a)) (typeIndex (undefined :: b)) x
\end{code}

\begin{code}
gcast1 :: (Typeable1 t, Typeable1 t') => c (t a) -> Maybe (c (t' a))
gcast1 (x :: c (t a)) :: Maybe (c' (t' a'))   liftM (unB . unFlip_1_0) $
  tiGCast_0 (typeIndex1 (undefined :: t  a))
            (typeIndex1 (undefined :: t' a)) $ Flip_1_0 $ B x
\end{code}

\begin{code}
gcast2 :: (Typeable2 t, Typeable2 t') => c (t a b) -> Maybe (c (t' a b))
gcast2 (x :: c (t a b)) :: Maybe (c' (t' a' b'))   liftM (unB1 . unRot_2_0_0)  $
  tiGCast_0_0 (typeIndex2 (undefined :: t  a b))
              (typeIndex2 (undefined :: t' a b)) $ Rot_2_0_0 $ B1 x
\end{code}

%{{{ automatic instances
For the automatic instances, the machinery from |Data.Typeable|
can easily be adapted.

\begin{code}
instance (Typeable1 s, Typeable a) => Typeable (s a) where typeIndex = typeIndexDefault
instance (Typeable2 s, Typeable a) => Typeable1 (s a) where typeIndex1 = typeIndex1Default
instance (Typeable3 s, Typeable a) => Typeable2 (s a) where typeIndex2 = typeIndex2Default
\end{code}

\begin{code}
-- | For defining a 'Typeable' instance from any 'Typeable1' instance.
typeIndexDefault :: (Typeable1 t, Typeable a) => t a -> TI (t a)
typeIndexDefault (x :: t a) = typeIndex1 x `Apply_0` typeIndex (undefined :: a)

-- | For defining a 'Typeable1' instance from any 'Typeable2' instance.
typeIndex1Default :: (Typeable2 t, Typeable a) => t a b -> TI_0 (t a)
typeIndex1Default (x :: t a b) = typeIndex2 x `Apply_0_0` typeIndex (undefined :: a)

-- | For defining a 'Typeable2' instance from any 'Typeable3' instance.
typeIndex2Default :: (Typeable3 t, Typeable a) => t a b c -> (TI_0_0 (t a))
typeIndex2Default (x :: t a b c) = typeIndex3 x `Apply_0_0_0` typeIndex (undefined :: a)
\end{code}
%}}}

%{{{ standard library instances
With our standard library instances
we are obviously restricted to the types covered by |TI|.

\begin{code}
instance Typeable ()      where typeIndex _ = Triv
instance Typeable Bool    where typeIndex _ = Bool
instance Typeable Char    where typeIndex _ = Char
instance Typeable Nat     where typeIndex _ = Nat
instance Typeable Int     where typeIndex _ = Int
instance Typeable Integer where typeIndex _ = Integer
instance Typeable Float   where typeIndex _ = Float
instance Typeable Double  where typeIndex _ = Double

instance Typeable1 Maybe  where typeIndex1 _ = Maybe
instance Typeable1 []     where typeIndex1 _ = List

instance Typeable2 Either where typeIndex2 _ = Either
instance Typeable2 (,)    where typeIndex2 _ = Pair
instance Typeable2 (->)   where typeIndex2 _ = Fct
\end{code}
%}}}

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