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

[Erik Hesselink]

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