# Type witness

### From HaskellWiki

(Difference between revisions)

m |
m (fmt) |
||

(2 intermediate revisions by 2 users not shown) | |||

Line 1: | Line 1: | ||

− | A '''type witness''' is a value that represents one of a range of possible types. When implemented as [[generalised algebraic datatype]]s (GADTs), type witness can be used to perform dynamic casts. |
+ | A '''type witness''' is a value that represents one of a range of possible [[type]]s. When implemented as [[generalised algebraic datatype]]s (GADTs), type witness can be used to perform dynamic casts. |

− | Types <tt>a</tt> and <tt>b</tt> may or may not be the same type. We wish to perform the cast <tt>a -> Maybe b</tt>, or more generally, <tt>p a -> Maybe (p b)</tt> for any <tt>p</tt>, depending on whether <tt>a</tt> and <tt>b</tt> are the same type. This can be done with GADTs if we have "witnesses" for the two types: |
+ | Types <tt>a</tt> and <tt>b</tt> may or may not be the same [[type]]. We wish to perform the cast <hask>a -> Maybe b</hask>, or more generally, <hask>p a -> Maybe (p b)</hask> for any <tt>p</tt>, depending on whether <tt>a</tt> and <tt>b</tt> 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) |
+ | <haskell> |

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

+ | </haskell> |
||

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

− | data Witness a where |
+ | <haskell> |

− | IntWitness :: Witness Int |
+ | data Witness a where |

− | BoolWitness :: Witness Bool |
+ | IntWitness :: Witness Int |

− | CharWitness :: Witness Char |
+ | BoolWitness :: Witness Bool |

+ | CharWitness :: Witness Char |
||

− | dynamicCast IntWitness IntWitness pa = Just pa |
+ | dynamicCast IntWitness IntWitness pa = Just pa |

− | dynamicCast BoolWitness BoolWitness pa = Just pa |
+ | dynamicCast BoolWitness BoolWitness pa = Just pa |

− | dynamicCast CharWitness CharWitness pa = Just pa |
+ | dynamicCast CharWitness CharWitness pa = Just pa |

− | dynamicCast _ _ _ = Nothing |
+ | dynamicCast _ _ _ = Nothing |

+ | </haskell> |
||

− | If we wish to add type constructors such as the list constructor, that can be done by composing type constructors: |
+ | If we wish to add [[type constructor]]s such as the list constructor, that can be done by composing type constructors: |

− | data Witness a where |
+ | <haskell> |

− | IntWitness :: Witness Int |
+ | data Witness a where |

− | BoolWitness :: Witness Bool |
+ | IntWitness :: Witness Int |

− | CharWitness :: Witness Char |
+ | BoolWitness :: Witness Bool |

− | ListWitness :: Witness a -> Witness [a] |
+ | CharWitness :: Witness Char |

+ | ListWitness :: Witness a -> Witness [a] |
||

− | data Compose p q a = MkCompose (p (q a)) |
+ | data Compose p q a = MkCompose (p (q a)) |

− | dynamicCast IntWitness IntWitness pa = Just pa |
+ | dynamicCast IntWitness IntWitness pa = Just pa |

− | dynamicCast BoolWitness BoolWitness pa = Just pa |
+ | dynamicCast BoolWitness BoolWitness pa = Just pa |

− | dynamicCast CharWitness CharWitness pa = Just pa |
+ | dynamicCast CharWitness CharWitness pa = Just pa |

− | dynamicCast (ListWitness wa) (ListWitness wb) pla = do |
+ | dynamicCast (ListWitness wa) (ListWitness wb) pla = do |

− | MkCompose plb <- dynamicCast wa wb (MkCompose pla) |
+ | MkCompose plb <- dynamicCast wa wb (MkCompose pla) |

− | return plb |
+ | return plb |

− | dynamicCast _ _ _ = Nothing |
+ | dynamicCast _ _ _ = Nothing |

+ | </haskell> |
||

By using more complex composition types in addition to <tt>Compose</tt>, it is possible for witnesses to allow type constructors of more complex [[kind]]s. |
By using more complex composition types in addition to <tt>Compose</tt>, it is possible for witnesses to allow type constructors of more complex [[kind]]s. |

## Latest 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.