Statically tracking "validity" - suggestions?
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? -- View this message in context: http://old.nabble.com/Statically-tracking-%22validity%22---suggestions--tp29... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
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
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
Erik Hesselink wrote:
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
Thanks, both of you. The GADT version seems slightly easier to work with in our case. -- View this message in context: http://old.nabble.com/Statically-tracking-%22validity%22---suggestions--tp29... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
I have a description of the design pattern you need, appropriately
named: http://lukepalmer.wordpress.com/2009/03/24/certificate-design-pattern/
On Tue, Aug 31, 2010 at 12:24 AM, 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? -- View this message in context: http://old.nabble.com/Statically-tracking-%22validity%22---suggestions--tp29... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Luke Palmer wrote:
I have a description of the design pattern you need, appropriately named: http://lukepalmer.wordpress.com/2009/03/24/certificate-design-pattern/
Mmm, I like that. There are two small problems: * In my web browser, some of the code snippets get the right-hand edge chopped off. * Double-precision floating-point arithmetic is inexact, so half your code won't actually work in the real world. (But obviously, it's only supposed to be an example for illustration purposes.) With regard to the second, does anybody know of anything on Hackage for testing whether two values are "approximately equal"? It must be a common programming problem, and it's more tricky than you think to solve it well.
2010/8/31 Andrew Coppin
Luke Palmer wrote:
I have a description of the design pattern you need, appropriately named: http://lukepalmer.wordpress.com/2009/03/24/certificate-design-pattern/
Mmm, I like that.
There are two small problems:
* In my web browser, some of the code snippets get the right-hand edge chopped off.
* Double-precision floating-point arithmetic is inexact, so half your code won't actually work in the real world. (But obviously, it's only supposed to be an example for illustration purposes.)
With regard to the second, does anybody know of anything on Hackage for testing whether two values are "approximately equal"? It must be a common programming problem, and it's more tricky than you think to solve it well.
I think something has been added to Hackage recently about that. There is this one, but I don't know if it is the one I was thinking about. http://hackage.haskell.org/package/ieee Cheers, Thu
does anybody know of anything on Hackage for testing whether two values are "approximately equal"?
http://hackage.haskell.org/package/approximate-equality -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)
On Mon, Aug 30, 2010 at 11:24:06PM -0700, strejon wrote:
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?
Yup. just do it just like you say :) declare your certificate like so (note: a is not used in the body)
data Certificate a = Certificate { .. }
then the valid data type
data Valid
There is no need for a Possibly_Valid type as it can be represented by just leaving the type unbound. so you will have validate :: forall a . Certificate a -> Maybe (Certificate Valid) so validate will take any certificate, and perhaps return a validated one. Then just use (Certificate Valid) in the types of functions that require valid certificates. This also means your functions are polymorphic in their validity by default, like
mapName :: (String -> String) -> Certificate a -> Certificate a
will work on valid or invalid certificates. Just note that when changing a phantom type you need to reconstruct the type fully. so for
data A data B data Foo a = Foo Int conv :: Foo A -> Foo B
you can't write
conv x = x
you need to write
conv (Foo x) = Foo x
since the argument is changing type. John -- John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/
participants (8)
-
Andrew Coppin -
Chris Eidhof -
Erik Hesselink -
John Meacham -
Luke Palmer -
Sebastian Fischer -
strejon -
Vo Minh Thu