Safe Haskell | Safe |
---|---|

Language | Haskell98 |

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 ->"

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

- 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"

- data TypeRep
- typeOf :: Typeable a => a -> TypeRep
- splitTyConApp :: TypeRep -> (TyCon, [TypeRep])
- mkTyConApp :: TyCon -> [TypeRep] -> TypeRep
- isInstanceOf :: TypeRep -> TypeRep -> Either TypeError ()
- funResultTy :: TypeRep -> TypeRep -> Either TypeError TypeRep
- type TypeError = String
- data TypVar a
- data Zero
- data Succ a
- type V0 = Zero
- type V1 = Succ V0
- type V2 = Succ V1
- type V3 = Succ V2
- type V4 = Succ V3
- type V5 = Succ V4
- type V6 = Succ V5
- type V7 = Succ V6
- type V8 = Succ V7
- type V9 = Succ V8
- type ANY = TypVar V0
- type ANY1 = TypVar V1
- type ANY2 = TypVar V2
- type ANY3 = TypVar V3
- type ANY4 = TypVar V4
- type ANY5 = TypVar V5
- type ANY6 = TypVar V6
- type ANY7 = TypVar V7
- type ANY8 = TypVar V8
- type ANY9 = TypVar V9
- class Typeable k a

# Basic types

Dynamic type representation with support for rank-1 types

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

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

mkTyConApp :: TyCon -> [TypeRep] -> TypeRep Source #

Inverse of `splitTyConApp`

# Operations on type representations

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

`t1 `

checks if `isInstanceOf`

t2`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