Question about constraining functions to particular ADT constructors
Hello there, I've been thinking on different approaches to constraint particular functions to a particular constructor of an ADT in order to reduce representation of invalid states. Say for example I've this types: data Address = Address { ... } newtype Email = Email String data Package = Package { ... } data EmailMsg = EmailMsg { ... } data User = RealUser Address | VirtualUser Email And I would like to implement two functions: deliverPackage :: User -> Package -> IO Bool sendEmail :: User -> EmailMsg -> IO () I would like to constraint both deliverPackage and sendEmail to receive only the semantically correct constructor of User. I know of an approach I could use, that is wrapping each constructor in it's own newtype, and create some smart constructor that way, that approach works, but I find it rather verbose. Is there any other well known approach to deal with this scenarios?
You could use DataKinds with GADTs like so {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} data UserType = RealUser | VirtualUser data User (userType :: UserType) where MkRealUser :: Address -> User RealUser MkVirtualUser :: Email -> User VirtualUser deliverPackage :: User RealUser -> Package -> IO Bool deliverPackage user = case user of -- This is the only valid pattern, since MkVritualUser would imply -- the type User VirtualUser. MkRealUser address -> ... sendEmail :: User VirtualUser -> EmailMsg -> IO () sendEmail user = case user of MkVritualUser email -> ... Alex Hello there, I've been thinking on different approaches to constraint particular functions to a particular constructor of an ADT in order to reduce representation of invalid states. Say for example I've this types: data Address = Address { ... } newtype Email = Email String data Package = Package { ... } data EmailMsg = EmailMsg { ... } data User = RealUser Address | VirtualUser Email And I would like to implement two functions: deliverPackage :: User -> Package -> IO Bool sendEmail :: User -> EmailMsg -> IO () I would like to constraint both deliverPackage and sendEmail to receive only the semantically correct constructor of User. I know of an approach I could use, that is wrapping each constructor in it's own newtype, and create some smart constructor that way, that approach works, but I find it rather verbose. Is there any other well known approach to deal with this scenarios?
Hi Román,
Why not just pass Address to deliverPackage and Email to sendEmail,
instead of passing a user? That way each function gets exactly the
information it needs, and there's no need to muck with GADTs and
DataKinds.
Erik
On Thu, Jun 11, 2015 at 6:54 PM, Román González
Hello there,
I've been thinking on different approaches to constraint particular functions to a particular constructor of an ADT in order to reduce representation of invalid states. Say for example I've this types:
data Address = Address { ... } newtype Email = Email String data Package = Package { ... } data EmailMsg = EmailMsg { ... }
data User = RealUser Address | VirtualUser Email
And I would like to implement two functions:
deliverPackage :: User -> Package -> IO Bool sendEmail :: User -> EmailMsg -> IO ()
I would like to constraint both deliverPackage and sendEmail to receive only the semantically correct constructor of User.
I know of an approach I could use, that is wrapping each constructor in it's own newtype, and create some smart constructor that way, that approach works, but I find it rather verbose.
Is there any other well known approach to deal with this scenarios?
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
participants (3)
-
Alexander Vieth -
Erik Hesselink -
Román González