
On 31 aug 2010, at 08:24, strejon 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?
Yes. Introduce a wrapper datatype, ValidCertificate. Create a module and export only the wrapper datatype and a way to construct ValidCertificates in a safe way:
module ValidateCertificate ( ValidCertificate, fromValidCertificate, createValidCertificate ) where
data ValidCertificate = ValidCertificate {fromValidCertificate :: Certificate}
createValidCertificate :: Certificate -> Maybe ValidCertificate createValidCertificate c | is_valid c = Just (ValidCertificate c) | otherwise = Nothing
is_valid :: Certificate -> Bool is_valid = isJust . user_name . certificate_subject
The trick is not to export the constructor, but only a verified way to construct values of ValidCertificate. -chris