[Haskell-cafe] Statically tracking "validity" - suggestions?

[John Meacham]

On Mon, Aug 30, 2010 at 11:24:06PM -0700, strejon wrote:
> I'm aware of phantom types and the like, but I've been unable to
> work out how to use them (or another type system extension)
> to properly track "validity" on the type level. I'd want something
> like:
> 
> validate :: Certificate Possibly_Valid -> Maybe (Certificate Valid)
> 
> With later functions only accepting values of type "Certificate Valid".
> 
> Is there a simple way to do this?

Yup. just do it just like you say :)

declare your certificate like so (note: a is not used in the body)

> data Certificate a = Certificate { .. }

then the valid data type

> data Valid

There is no need for a Possibly_Valid type as it can be represented by
just leaving the type unbound. so you will have

validate :: forall a . Certificate a -> Maybe (Certificate Valid)

so validate will take any certificate, and perhaps return a validated
one. Then just use (Certificate Valid) in the types of functions that
require valid certificates.

This also means your functions are polymorphic in their validity by
default, like

> mapName :: (String -> String) -> Certificate a -> Certificate a

will work on valid or invalid certificates.

Just note that when changing a phantom type you need to reconstruct the
type fully. so for 

> data A
> data B
> data Foo a = Foo Int
> conv :: Foo A -> Foo B

you can't write

> conv x = x

you need to write

> conv (Foo x) = Foo x

since the argument is changing type.


        John






-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/