# Type witness

### From HaskellWiki

(Difference between revisions)

BrettGiles (Talk | contribs) m (Adding link to new type page, placeholder links to constructor page) |

## Revision as of 20:03, 16 March 2006

A **type witness** is a value that represents one of a range of possible types. When implemented as generalised algebraic datatypes (GADTs), type witness can be used to perform dynamic casts.

`a`and

`b`may or may not be the same type. We wish to perform the cast

a -> Maybe b

p a -> Maybe (p b)

`p`, depending on whether

`a`and

`b`are the same type. This can be done with GADTs if we have "witnesses" for the two types:

dynamicCast :: Witness a -> Witness b -> p a -> Maybe (p b)

A simple witness type might be defined over the Int, Bool and Char types like so:

data Witness a where IntWitness :: Witness Int BoolWitness :: Witness Bool CharWitness :: Witness Char dynamicCast IntWitness IntWitness pa = Just pa dynamicCast BoolWitness BoolWitness pa = Just pa dynamicCast CharWitness CharWitness pa = Just pa dynamicCast _ _ _ = Nothing

If we wish to add type constructors such as the list constructor, that can be done by composing type constructors:

data Witness a where IntWitness :: Witness Int BoolWitness :: Witness Bool CharWitness :: Witness Char ListWitness :: Witness a -> Witness [a] data Compose p q a = MkCompose (p (q a)) dynamicCast IntWitness IntWitness pa = Just pa dynamicCast BoolWitness BoolWitness pa = Just pa dynamicCast CharWitness CharWitness pa = Just pa dynamicCast (ListWitness wa) (ListWitness wb) pla = do MkCompose plb <- dynamicCast wa wb (MkCompose pla) return plb dynamicCast _ _ _ = Nothing

By using more complex composition types in addition to `Compose`, it is possible for witnesses to allow type constructors of more complex kinds.