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

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

import NatNum
import TypeCombinators
\end{code}

For each ground type |a| constructed only from supported type constructors,
there is exactly one \emph{type index} in |TI a|.
In that respect,
an element of |TI a|
is similar to the satisfaction of the constraint |Typeable a|.

The important difference between |TI a| and |Typeable a|
is that structural induction over the structure of a type
documented by a |TI a| contains references to the constituent types
\emph{at the type level},
while structural induction over |TypeRep| representations of
type structure made accessible by |Typeable a|
has no connection to the type level at all.

\begin{code}
data TI :: * -> * where
  Triv :: TI ()
  Bool :: TI Bool
  Char :: TI Char
  Nat  :: TI Nat
  Int  :: TI Int
  Integer :: TI Integer
  Float :: TI Float
  Double :: TI Double
  Apply_0 :: TI_0 t -> TI a -> TI (t a)
  Apply_1 :: TI_1 t -> TI_0 a -> TI (t a)
\end{code}

Since one of the limitations of |Data.Typeable|
is its naming scheme that does not accommodate higher-kinded type constructors,
we use a naming scheme that is at least somewhat open in that direction,
and provide
alternative names following the scheme of |Data.Typeable| as type synonyms.

\begin{code}
type TI1 = TI_0
type TI2 = TI_0_0
type TI3 = TI_0_0_0
\end{code}

\begin{code}
data TI_0 :: (* -> *) -> * where
  Maybe :: TI_0 Maybe
  List :: TI_0 []
  Apply_0_0 :: TI_0_0 t -> TI a -> TI_0 (t a)
\end{code}

\begin{code}
data TI_0_0 :: (* -> * -> *) -> * where
  Either :: TI_0_0 Either
  Pair :: TI_0_0 (,)
  Fct :: TI_0_0 (->)
  Apply_0_0_0 :: TI_0_0_0 t -> TI a -> TI_0_0 (t a)
\end{code}

\begin{code}
data TI_0_0_0 :: (* -> * -> * -> *) -> * where
  Tup3 :: TI_0_0_0 (,,)
\end{code}

Just to demonstrate a higher-order kind in this context,
we define the datatype recursion type constructor.

\begin{code}
data TI_1 :: ((* -> *) -> *) -> * where
  Fix :: TI_1 DFix

data DFix f = DFix (f (DFix f))
\end{code}

We intentionally do not currently include the type combinators
from |TypeCombinators|
to show that they only serve in a supporting r\^ole in our implementation
of |cast| in |Typeable|.

\medskip
Defining type index equality without requiring identical types
makes the implementation of the cast functions much easier.

\begin{code}
instance GenEq TI where genEq = eqTI

eqTI :: GenEQ TI
eqTI  Triv Triv = True
eqTI  Bool Bool = True
eqTI  Char Char = True
eqTI  Nat Nat = True
eqTI  Int Int = True
eqTI  Integer Integer = True
eqTI  Float Float = True
eqTI  Double Double = True
eqTI (Apply_0 t a) (Apply_0 t' a') = eqTI_0 t t' && eqTI a a'
eqTI (Apply_1 t a) (Apply_1 t' a') = eqTI_1 t t' && eqTI_0 a a'
eqTI _ _ = False
\end{code}

\begin{code}
eqTI_0 :: TI_0 t -> TI_0 t' -> Bool
eqTI_0 Maybe Maybe = True
eqTI_0 List List = True
eqTI_0 (Apply_0_0 t a) (Apply_0_0 t' a') = eqTI_0_0 t t' && eqTI a a'
eqTI_0 _ _ = False
\end{code}

\begin{code}
eqTI_1 :: TI_1 t -> TI_1 t' -> Bool
eqTI_1 Fix Fix = True
-- |eqTI_1 _ _ = False|      -- currently not needed
\end{code}

\begin{code}
eqTI_0_0 :: TI_0_0 t -> TI_0_0 t' -> Bool
eqTI_0_0 Either Either = True
eqTI_0_0 Pair Pair = True
eqTI_0_0 Fct Fct = True
eqTI_0_0 _ _ = False
\end{code}


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