On Tue, Aug 31, 2010 at 08:24, strejon <strej...@yahoo.com> wrote:
>
> Hello. I'm using Haskell to write a specification for some software. The
> software uses certificates (standard X.509 certificates) and stores user
> name information in the Subject's CommonName field.
>
> The X.509 standard doesn't actually require the presence of a CommonName
> field so the contents of the Subject section (with the rest of the fields
> omitted) are just represented by a Maybe User_Name.
>
>> import Data.List (find, concat)
>> import Data.Maybe (fromJust, isJust)
>>
>> type User_Name = String
>> type Public_Key = Integer
>> data Subject_Name = Subject_Name (Maybe User_Name) deriving (Show, Eq)
>>
>> data Certificate = Certificate {
>> certificate_subject :: Subject_Name,
>> certificate_key :: Public_Key,
>> certificate_issuer :: String,
>> certificate_serial :: Integer
>> } deriving (Show, Eq)
>
> This is all well and good, but the problem is that the validity of
> certificates isn't tracked statically and I have to use the following
> as guards on all functions that only expect valid certificates (and
> inevitably handle cases that I know can't actually happen but
> have to be handled in pattern matching and the like, bloating
> the specification):
>
>> user_name :: Subject_Name -> Maybe User_Name
>> user_name (Subject_Name name) = name
>>
>> is_valid :: Certificate -> Bool
>> is_valid = isJust . user_name . certificate_subject
>
> 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?
If you want to use types instead of modules and hiding as Chris
suggested, you can use a type index like this:
{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures #-}
data Nothing
data Just a
data Subject :: * -> * where
NoName :: Subject Nothing
Name :: String -> Subject (Just String)
data Certificate a = Certificate
{ subject :: Subject a }
validate :: Certificate a -> Maybe (Certificate (Just String))
validate c =
case subject c of
NoName -> Nothing
Name n -> Just c
A "Certificate (Just String)" now always holds a name, and a
"Certificate Nothing" doesn't. A "Certificate a" can hold either.
Erik
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
