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

[Chris Eidhof]

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