[Haskell-cafe] Question about constraining functions to particular ADT constructors

[Alexander Vieth]

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?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150611/241b7ff1/attachment.html>