Personal tools

Type witness

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (Adding link to new type page, placeholder links to constructor page)
Current revision (20:03, 16 March 2006) (edit) (undo)
m (fmt)
 
(One intermediate revision not shown.)
Line 1: Line 1:
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.
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]] [[constructor]]s 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.
[[Category:Idioms]]
[[Category:Idioms]]

Current revision

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.

Retrieved from "http://www.haskell.org/haskellwiki/Type_witness"

Category: Idioms