On Tue, Aug 31, 2010 at 08:24, strejon
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