Tomasz Zielonka 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}