Philip Kamenarsky
Philip Kamenarsky

Reputation: 2777

Turn TypeRep into a concrete type representation

I would like to write the following function:

data TypeEnum = IntType | FloatType | BoolType | DateType | StringType
data Schema = Object [Schema] |
              Field TypeEnum |
              Array Schema

schema :: Typeable a => a -> Schema

Now I can get a list of TypeReps for a given constructor, but I can't seem to find a way to convert a TypeRep into a Schema for more complex types:

field :: TypeRep t => t -> Schema
field t | t == typeOf (undefined :: String) = Field StringType
        | t == typeOf (undefined :: Int) = Field IntType
        | t == typeOf (undefined :: ???) = Array ???
        | t == typeOf (undefined :: ???) = Object ???

It works for simple types like Int and String but what about Typeable or [Typeable]?

Upvotes: 3

Views: 288

Answers (2)

Luis Casillas
Luis Casillas

Reputation: 30237

If you have a closed set of types that are the only ones your program will want to reason about, you could consider sidestepping Data.Typeable and just roll your own type representations with GADTs as shown below. The differences between this and the standard Typeable are the following:

  • TypeReps from Data.Typeable don't have a type variable representing the type they stand for, whereas the in the alternative below you get TypeRep a, where a is the type that your TypeRep stands for (e.g., typeOf "foo" :: TypeRep [Char]).
  • However the GADT approach shown below only works for a set of types fixed at compilation time, because your homebrewTypeRep definition needs to list out all the representable types and type constructors.

Why am I suggesting to go this complex route? Because you can use this technique to eliminate the sequence of pattern guards in your definition of field:

data Schema a = ...
              | Field (TypeRep a) -- my TypeRep from below, not the standard one!
              | ...

field :: TypeRep a -> Schema a
field t = Field typeRep

The downside here is that the GADT TypeReps have a type parameter, it's going to require some other approach to handle the case for your Object :: [Schema] -> Schema constructor, because this replaces [Schema] with [Schema a]. Maybe you could try something like this:

{-# LANGUAGE GADTs #-}
data Schema a where 
    Field   :: TypeRep a -> Schema a
    Array   :: Schema a -> Schema (Array a)
    Object2 :: Schema a -> Schema b -> Schema (a, b)
    Object3 :: Schema a -> Schema b -> Schema c -> Schema (a, b, c)
    ...

But I figure that if you study the code below you may find some ideas that you could incorporate into what you're doing—your TypeEnum type is similar to my TypeRep type below, except that mine is able to represent type constructors in addition to atomic types.

So here's the code (which should be easy to modify for your choice of types):

{-# LANGUAGE GADTs #-}

import Control.Applicative

----------------------------------------------------------------
----------------------------------------------------------------
--
-- | Type representations.  If @x :: TypeRep a@, then @x@ is a singleton
-- value that stands in for type @a@.
data TypeRep a where 
    Integer :: TypeRep Integer
    Char    :: TypeRep Char
    Maybe   :: TypeRep a -> TypeRep (Maybe a)
    List    :: TypeRep a -> TypeRep [a]
    Pair    :: TypeRep a -> TypeRep b -> TypeRep (a, b)

-- | Typeclass for types that have a TypeRep
class Representable a where
    typeRep :: TypeRep a

instance Representable Integer where typeRep = Integer
instance Representable Char where typeRep = Char

instance Representable a => Representable (Maybe a) where 
    typeRep = Maybe typeRep

instance Representable a => Representable [a] where 
    typeRep = List typeRep

instance (Representable a, Representable b) => Representable (a,b) where 
    typeRep = Pair typeRep typeRep


typeOf :: Representable a => a -> TypeRep a
typeOf = const typeRep


----------------------------------------------------------------
----------------------------------------------------------------
--
-- | Type equality proofs.
data Equal a b where
    Reflexivity :: Equal a a


-- | Induction rules for type equality proofs for parametric types
induction :: Equal a b -> Equal (f a) (f b)
induction Reflexivity = Reflexivity

induction2 :: Equal a a' -> Equal b b' -> Equal (f a b) (f a' b')
induction2 Reflexivity Reflexivity = Reflexivity

-- | Given two TypeReps, prove or disprove their equality.
matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b)
matchTypes Integer Integer = Just Reflexivity
matchTypes Char Char = Just Reflexivity
matchTypes (List a) (List b) = induction <$> (matchTypes a b)
matchTypes (Maybe a) (Maybe b) = induction <$> (matchTypes a b)
matchTypes (Pair a b) (Pair a' b') = 
    induction2 <$> matchTypes a a' <*> matchTypes b b'
matchTypes _ _ = Nothing


----------------------------------------------------------------
----------------------------------------------------------------
--
-- Example use: type-safe coercions and casts
--

-- | Given a proof that a and b are the same type, you can
-- actually have an a -> b function.
coerce :: Equal a b -> a -> b
coerce Reflexivity x = x

cast :: TypeRep a -> TypeRep b -> a -> Maybe b
cast a b x = coerce <$> (matchTypes a b) <*> pure x


----------------------------------------------------------------
----------------------------------------------------------------
--
-- Example use: dynamic data
--

data Dynamic where
    Dyn :: TypeRep a -> a -> Dynamic

-- | Inject a value of a @Representable@ type into @Dynamic@.
toDynamic :: Representable a => a -> Dynamic
toDynamic = Dyn typeRep

-- | Cast a @Dynamic@ into a @Representable@ type.
fromDynamic :: Representable a => Dynamic -> Maybe a
fromDynamic = fromDynamic' typeRep

fromDynamic' :: TypeRep a -> Dynamic -> Maybe a
fromDynamic' :: TypeRep a -> Dynamic -> Maybe a
fromDynamic' target (Dyn source value) = cast source target value

EDIT: I couldn't help but play some more with the above:

{-# LANGUAGE StandaloneDeriving #-}
import Data.List (intercalate)

--
-- And now, I believe this is very close to what you want...
--
data Schema where
    Field :: TypeRep a -> Schema
    Object :: [Schema] -> Schema
    Array :: Schema -> Schema

deriving instance Show (TypeRep a)
deriving instance Show (Schema)

example :: Schema
example = Object [Field (List Char), Field Integer]

describeSchema :: Schema -> String
describeSchema (Field t) = "Field of type " ++ show t
describeSchema (Array s) = "Array of type " ++ show s
describeSchema (Object schemata) = 
    "an Object with these schemas: " 
        ++ intercalate ", " (map describeSchema schemata)

With that, describeSchema example produces "an Object with these schemas: Field of type List Char, Field of type Integer".

Upvotes: 1

Daniel Wagner
Daniel Wagner

Reputation: 153172

You can get the type of a one-argument type constructor using typeOf1:

> typeOf (undefined :: Array Int Int)
Array Int Int
> typeOf1 (undefined :: Array Int Int)
Array Int
> typeOf2 (undefined :: Array Int Int)
Array
> typeOf2 (undefined :: Array a b)
Array

edit: Sorry, I misunderstood the question. Here's some more helpful advice... You can split a TypeRep into its constituent bits using splitTyConApp and friends:

> splitTyConApp (typeOf (undefined :: Array Int Int))
(Array,[Int,Int])
> let arr = typeRepTyCon (typeOf (undefined :: Array Int Int))
> mkTyConApp arr [] == typeOf2 (undefined :: Array a b)
True

Upvotes: 2

Related Questions