[Haskell] ANN: witness 0.1, open-witness 0.1, "Witnesses and Open Witnesses"

Ashley Yakeley 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.

witness 0.1
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)

Source: <http://code.haskell.org/witness/>

open-witness 0.1
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.

Source: <http://code.haskell.org/open-witness/>

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 
implementation fuss.

draft, rejected from the Haskell Symposium 2008

Ashley Yakeley
Seattle, WA

More information about the Haskell mailing list