[Fwd: Re: [Haskell-cafe] Typeclasses and GADT [Was: Regular Expressions without GADTs]]

[kahl at cas.mcmaster.ca]

Tomasz Zielonka <tomasz.zielonka at gmail.com> wrote
Wed, 26 Oct 2005 13:37:29 +0200:
 >
 > Speaking about casts, I was playing with using GADTs to create a
 > non-extensible version of Data.Typeable and Data.Dynamic.
 > I wonder if it's possible to write such a thing without GADTs (and
 > unsafeCoerce, which is used in Data.Dynamic, IIRC).

It is possible to get even closer to Typeable by using
the same interface --- which is sufficient for some applications.

Otherwise, what I did recently is essentially equivalent
to the ``non-Dynamic part'' of Tomasz code
(and adding Dyn would of course work in the same way):

    Thomasz'           -->   attached modules
    -------------------------------------------------------
    data Type          -->   data TI.TI*

    class Typed        -->   class Typeable.Typeable*

    newtype Wrapper*   -->   replaced by the ``*''s above ;-)



Wolfram


--[[application/octet-stream
Content-Disposition: attachment; filename="TI.lhs"][quoted-printable]]
%include lhs2TeX.fmt
%include WKlhs.sty
\section{Type Indices}

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

import NatNum
\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}

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

\begin{code}
eqTI :: TI a -> TI b -> Bool
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
\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:
%}}}
--[[application/octet-stream
Content-Disposition: attachment; filename="Typeable.lhs"][quoted-printable]]
%include lhs2TeX.fmt
%include WKlhs.sty
\section{Home-made |Typeable|}

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

import NatNum
import TI
import GHC.Base ( unsafeCoerce# )
\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.

The following function is GHC-specific:
\begin{code}
unsafeCoerce :: a -> b
unsafeCoerce = unsafeCoerce#
\end{code}

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}

We shamelessly use scoped type variables
to abbreviate the |cast| and |gcast| definitions,
which otherwise correspond directly to those from |Data.Typeable|.

\begin{code}
cast :: (Typeable a, Typeable b) => a -> Maybe b
cast x :: Maybe b = if typeIndex x `eqTI` typeIndex (undefined :: b)
                    then Just $ unsafeCoerce x
	            else Nothing
\end{code}

\begin{code}
gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b)
gcast (x :: c a) :: Maybe (c' b) =
  if typeIndex (undefined :: a) `eqTI` typeIndex (undefined :: b)
        then Just $ unsafeCoerce x
        else Nothing
\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')) =
  if typeIndex1 (undefined :: t a) `eqTI_0` typeIndex1 (undefined :: t' a)
  then Just $ unsafeCoerce x
  else Nothing
\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')) =
  if typeIndex2 (undefined :: t a b) `eqTI_0_0` typeIndex2 (undefined :: t' a b)
  then Just $ unsafeCoerce x
  else Nothing
\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:
%}}}
--[[application/octet-stream
Content-Disposition: attachment; filename="GCast.lhs"][quoted-printable]]
%include lhs2TeX.fmt
%include WKlhs.sty
\section{Minimal Interface Providing Generic Cast}

This module provides a minimal interface to |gcast|
since this is all that is really required by many applications
of |Typeable| and friends.

Isolating this interface
makes it easier to switch between different implementations.

%{-# OPTIONS_GHC -fglasgow-exts #-}  taken out for lhs2tex
\begin{code}
module GCast
 ( Typeable()
 , Typeable1()
 , Typeable2()
 , Typeable3()
 , cast
 , gcast
 , gcast1
 , gcast2
 ) where

-- import Data.Typeable
import Typeable
\end{code}

%{{{ EMACS lv
% Local Variables:
% folded-file: t
% fold-internal-margins: 0
% eval: (fold-set-marks "%{{{ " "%}}}")
% eval: (fold-whole-buffer)
% end:
%}}}
--[[application/octet-stream
Content-Disposition: attachment; filename="NatNum.lhs"][quoted-printable]]
\section{Inductive Definition of Natural Numbers}

\begin{code}
module NatNum where
import Data.Typeable

data Nat = Zero | Succ
  deriving Typeable
\end{code}