[Haskell] ANN: witness 0.1, open-witness 0.1,
"Witnesses and Open Witnesses"
ashley at semantic.org
Mon Aug 18 04:27:46 EDT 2008
Two packages, and the draft paper on which they are based. Both packages
are "proof of concept"; I'm open to ideas and repainting of bike-sheds.
A witness is a value that witnesses some sort of constraint on some list
of type variables. This library provides support for simple witnesses,
that constrain a type variable to a single type, and equality witnesses,
that constrain two type variables to be the same type. The library also
provides classes for representatives, which are values that represent types.
For example, the equality witness type:
data EqualType a b where
MkEqualType :: EqualType t t
If two simple witness values are the same, then their types are the same:
class SimpleWitness w where
matchWitness :: w a -> w b -> Maybe (EqualType a b)
Open witnesses (type IOWitness) are simple witnesses that can witness to
any type. However, they cannot be constructed, they can only be
generated in certain monads:
newIOWitness :: IO (IOWitness a)
We can also create fully heterogenous dictionaries that use open
witnesses as keys. This would work as the state in an ST monad.
If we had a "top-level" monad, or some other way of declaring unique
IOWitness values at top level, we could straightforwardly and safely
solve the expression problem (see below). In lieu of that, there's an
unsafe function to construct them:
unsafeIOWitnessFromString :: String -> IOWitness a
This release includes an example re-implementation of ST/STRef, and a
sound approximation of Typeable/Dynamic.
Witnesses and Open Witnesses
We review witnesses, an emerging Haskell idiom, and suggest some
terminology. We then introduce open witnesses as a library, and propose
an extension to allow the creation of them at top-level. We show how
this solves the expression problem, all with relatively little
draft, rejected from the Haskell Symposium 2008
More information about the Haskell