rank1dynamic-0.2.0.1: Like Data.Dynamic/Data.Typeable but with support for rank-1 polymorphic types

Safe HaskellNone
LanguageHaskell98

Data.Rank1Typeable

Contents

Description

Runtime type representation of terms with support for rank-1 polymorphic types with type variables of kind *.

The essence of this module is that we use the standard Typeable representation of Data.Typeable but we introduce a special (empty) data type TypVar which represents type variables. TypVar is indexed by an arbitrary other data type, giving you an unbounded number of type variables; for convenience, we define ANY, ANY1, .., ANY9.

Examples of isInstanceOf
-- We CANNOT use a term of type 'Int -> Bool' as 'Int -> Int'
> typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: Int -> Bool)
Left "Cannot unify Int and Bool"

-- We CAN use a term of type 'forall a. a -> Int' as 'Int -> Int'
> typeOf (undefined :: Int -> Int) `isInstanceOf` typeOf (undefined :: ANY -> Int)
Right ()

-- We CAN use a term of type 'forall a b. a -> b' as 'forall a. a -> a'
> typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY1)
Right ()

-- We CANNOT use a term of type 'forall a. a -> a' as 'forall a b. a -> b'
> typeOf (undefined :: ANY -> ANY1) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
Left "Cannot unify Succ and Zero"

-- We CAN use a term of type 'forall a. a' as 'forall a. a -> a'
> typeOf (undefined :: ANY -> ANY) `isInstanceOf` typeOf (undefined :: ANY)
Right ()

-- We CANNOT use a term of type 'forall a. a -> a' as 'forall a. a'
> typeOf (undefined :: ANY) `isInstanceOf` typeOf (undefined :: ANY -> ANY)
Left "Cannot unify Skolem and ->"

-- We CAN use a term of type 'forall a. a -> m a' as 'Int -> Maybe Int'
> typeOf (undefined :: Int -> Maybe Int)
    `isInstanceOf` typeOf (undefined :: ANY1 -> ANY ANY1)
Left "Cannot unify Skolem and ->"

-- We CAN use a term of type 'forall a. Monad a => a -> m a' as 'Int -> Maybe Int'
-- 'Dict' comes from "Data.Constraint" in the package "constraints".
> typeOf ((\Dict -> return) :: Dict (Monad Maybe) -> Int -> Maybe Int)
    `isInstanceOf` typeOf ((\Dict -> return) :: Dict (Monad ANY) -> ANY1 -> ANY ANY1)
Right ()

(Admittedly, the quality of the type errors could be improved.)

When using -XPolyKinds, the type signatures with higher-kinded variables need to be given as

(\Dict -> return) `asTypeOf` (undefined :: Dict (Monad ANY) -> ANY1 -> ANY ANY1)

or

(\Dict -> return) :: Dict (Monad ANY) -> ANY1 -> ANY (ANY1 :: *)

Please, see tests/test.hs for examples of how to write the higher-kinded cases in ghc versions earlier than 7.8.3.

Examples of funResultTy
-- Apply fn of type (forall a. a -> a) to arg of type Bool gives Bool
> funResultTy (typeOf (undefined :: ANY -> ANY)) (typeOf (undefined :: Bool))
Right Bool

-- Apply fn of type (forall a b. a -> b -> a) to arg of type Bool gives forall a. a -> Bool
> funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: Bool))
Right (ANY -> Bool) -- forall a. a -> Bool

-- Apply fn of type (forall a. (Bool -> a) -> a) to argument of type (forall a. a -> a) gives Bool
> funResultTy (typeOf (undefined :: (Bool -> ANY) -> ANY)) (typeOf (undefined :: ANY -> ANY))
Right Bool

-- Apply fn of type (forall a b. a -> b -> a) to arg of type (forall a. a -> a) gives (forall a b. a -> b -> b)
> funResultTy (typeOf (undefined :: ANY -> ANY1 -> ANY)) (typeOf (undefined :: ANY1 -> ANY1))
Right (ANY -> ANY1 -> ANY1)

-- Cannot apply function of type (forall a. (a -> a) -> a -> a) to arg of type (Int -> Bool)
> funResultTy (typeOf (undefined :: (ANY -> ANY) -> (ANY -> ANY))) (typeOf (undefined :: Int -> Bool))
Left "Cannot unify Int and Bool"

Synopsis

Basic types

data TypeRep Source

Dynamic type representation with support for rank-1 types

Instances

Eq TypeRep

Compare two type representations

For base >= 4.6 this compares fingerprints, but older versions of base have a bug in the fingerprint construction (http://hackage.haskell.org/trac/ghc/ticket/5962)

Show TypeRep 
Binary TypeRep 

typeOf :: Typeable a => a -> TypeRep Source

The type representation of any Typeable term

splitTyConApp :: TypeRep -> (TyCon, [TypeRep]) Source

Split a type representation into the application of a type constructor and its argument

underlyingTypeRep :: TypeRep -> TypeRep Source

Return the underlying standard (Data.Typeable) type representation

Operations on type representations

isInstanceOf :: TypeRep -> TypeRep -> Either TypeError () Source

t1 isInstanceOf t2 checks if t1 is an instance of t2

funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep Source

funResultTy t1 t2 is the type of the result when applying a function of type t1 to an argument of type t2

type TypeError = String Source

If isInstanceOf fails it returns a type error

Type variables

type TypVar = Any T Source

data Zero Source

Instances

data Succ a Source

Instances

Typeable (* -> *) Succ 

type V0 = Zero Source

type V1 = Succ V0 Source

type V2 = Succ V1 Source

type V3 = Succ V2 Source

type V4 = Succ V3 Source

type V5 = Succ V4 Source

type V6 = Succ V5 Source

type V7 = Succ V6 Source

type V8 = Succ V7 Source

type V9 = Succ V8 Source

Re-exports from Typeable

class Typeable a

The class Typeable allows a concrete representation of a type to be calculated.

Minimal complete definition

typeRep#

Instances

Typeable * Bool 
Typeable * Char 
Typeable * Double 
Typeable * Float 
Typeable * Int 
Typeable * Integer 
Typeable * Ordering 
Typeable * RealWorld 
Typeable * Word 
Typeable * Word8 
Typeable * Word16 
Typeable * Word32 
Typeable * Word64 
Typeable * () 
Typeable * SpecConstrAnnotation 
Typeable * TypeRep 
Typeable * TyCon 
Typeable * Zero 
Typeable k (Any k) 
(Typeable (k1 -> k) s, Typeable k1 a) => Typeable k (s a)

Kind-polymorphic Typeable instance for type application

Typeable ((* -> *) -> Constraint) Alternative 
Typeable ((* -> *) -> Constraint) Applicative 
Typeable (* -> * -> * -> * -> * -> * -> * -> *) (,,,,,,) 
Typeable (* -> * -> * -> * -> * -> * -> *) (,,,,,) 
Typeable (* -> * -> * -> * -> * -> *) (,,,,) 
Typeable (* -> * -> * -> * -> *) (,,,) 
Typeable (* -> * -> * -> *) (,,) 
Typeable (* -> * -> * -> *) STArray 
Typeable (* -> * -> *) (->) 
Typeable (* -> * -> *) Either 
Typeable (* -> * -> *) (,) 
Typeable (* -> * -> *) ST 
Typeable (* -> * -> *) Array 
Typeable (* -> * -> *) STRef 
Typeable (* -> *) [] 
Typeable (* -> *) Ratio 
Typeable (* -> *) IO 
Typeable (* -> *) Ptr 
Typeable (* -> *) FunPtr 
Typeable (* -> *) Maybe 
Typeable (* -> *) Succ 
Typeable (k -> *) (Proxy k) 
Typeable (k -> k -> *) (Coercion k) 
Typeable (k -> k -> *) ((:~:) k)