Tomasz Zielonka <tomasz.zielonka(a)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}
