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)

Hackage: <http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness>
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.

Hackage: <http://hackage.haskell.org/cgi-bin/hackage-scripts/package/open-witness>
Source: <http://code.haskell.org/open-witness/>



Witnesses and Open Witnesses

Abstract:
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
<http://semantic.org/stuff/Open-Witnesses.pdf>

--
Ashley Yakeley
Seattle, WA

_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to