Difference between revisions of "Type witness"
m (fmt) |
|||
(5 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 |
+ | 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 < |
+ | 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: |
+ | <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: |
||
+ | <haskell> |
||
− | + | data Witness a where |
|
⚫ | |||
− | + | IntWitness :: Witness Int |
|
− | + | BoolWitness :: Witness Bool |
|
⚫ | |||
− | + | dynamicCast IntWitness IntWitness pa = Just pa |
|
− | + | dynamicCast BoolWitness BoolWitness pa = Just pa |
|
− | + | dynamicCast CharWitness CharWitness pa = Just pa |
|
− | + | dynamicCast _ _ _ = Nothing |
|
+ | </haskell> |
||
− | If we wish to add type |
+ | If we wish to add [[type constructor]]s such as the list constructor, that can be done by composing type constructors: |
+ | <haskell> |
||
− | + | data Witness a where |
|
− | IntWitness :: Witness Int |
||
− | + | IntWitness :: Witness Int |
|
− | + | BoolWitness :: Witness Bool |
|
− | + | CharWitness :: Witness Char |
|
+ | ListWitness :: Witness a -> Witness [a] |
||
− | + | data Compose p q a = MkCompose (p (q a)) |
|
− | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
⚫ | |||
+ | </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. |
||
[[Category:Idioms]] |
[[Category:Idioms]] |
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.
Types a and b may or may not be the same type. We wish to perform the cast a -> Maybe b
, or more generally, p a -> Maybe (p b)
for any 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.