Using a promoted data constructor as a phantom parameter

Question

In Maguire's Thinking with Types, p. 29, there's an example of how to use a promoted data constructor as a phantom parameter. Here's a module that I wrote based on the example in the book.

{-# LANGUAGE DataKinds #-}
module Main where

import           Data.Maybe
import           Data.Proxy

-- | The only purpose of this constructor is to give us access to its
--   promoted data constructors.
data UserType = DummyUser | Admin

-- | Give some users an administration token.
data User = User
  { userAdminToken :: Maybe (Proxy 'Admin),
    name           :: String
  }

doSensitiveThings :: Proxy 'Admin -> IO ()
doSensitiveThings _ = putStrLn "you did something sensitive"

trustedUser :: User
trustedUser = User (Just (Proxy :: Proxy Admin)) "Trust me"

main = do
    doSensitiveThings (fromJust . userAdminToken $ trustedUser)

I understand that this makes it impossible to call doSensitiveThings without an administration token. But I feel I'm missing something important. How is the code above better than the code below?

module Main where

import           Data.Maybe

data Admin = Admin

data User a = User String

doSensitiveThings :: User Admin -> IO ()
doSensitiveThings _ = putStrLn "you did something sensitive"

trustedUser :: User Admin
trustedUser = User "Trust me"

untrustedUser :: User ()
untrustedUser = User "Don't trust me"

main = do
    doSensitiveThings trustedUser
    -- doSensitiveThings untrustedUser -- won't compile

Encompass

I don't like the original code. If we used trustedUser = User Nothing "Do not trust me" it would still make the code compile and even run the "sensible" part! Your code is better, IMO. I'd still write data User (a :: UserType) = User String so to completely prevent User (), which now becomes a kind error. – Mulciber

The big thing about a phantom type is that it should be visible but not affect runt time representation. Your User example kind of does neither of those. – Metropolis

In your second version, you should use a role annotation to protect the phantom from safe corrections. Enable {-# RoleAnnotations #-} and then add type role User nominal where you define your type. Now Data.Coerce.coerce :: User a -> User Admin won't type-check. – Landeros

s/corrections/coercions in my last comment. – Landeros

What is DummyUser doing in the first example? It isn't mentioned anywhere else; is that on purpose? – Harod

This toy example is so trivial that its difficult to argue based on the pragmaticism of either one. Purely from this standpoint, both are useless in terms of preventing unauthorized access to doSensitiveThings. Furthermore, neither method is strictly more general than the other, and they are not equivalent, so it isn't "better" or "worse", rather just "different". – Joslin

Answer 1

Well, now there's no such thing as "a User". A User Admin and a User () now have different types, so you cannot treat them the same as e.g. elements of a list:

users :: [User] -- ill-kinded!
users = [User "untrusted" :: User (), User "trusted" :: User Admin] -- ill-typed!

You also can no longer branch based on whether a user is an admin or not (remember that Haskell is type-erased!):

displayActions :: User a -> [String]
displayActions (User name) =
    ["Delete My Account (" ++ name ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])
isAdmin :: User a -> Bool -- this function can take either User Admin or User ()...
isAdmin = ??? -- ...but how's it supposed to branch on that?

So maybe try

data SomeUser = SomeAdmin (User Admin) | SomeNormalUser (User ())

But now we're basically doing the same thing in your first example (where User Admin becomes the token type instead of Proxy Admin) except it's just worse. There's just a lot code noise.

name :: SomeUser -> String -- having to write your own accessor functions over pattern matching/record fields; ew
name (SomeAdmin (User x)) = x
name (SomeNormalUser (User x)) = x -- ugly pattern matching and same code twice; ew
isAdmin :: SomeUser -> Bool
isAdmin (SomeAdmin _) = True
isAdmin _ = False

displayActions :: SomeUser -> [String] -- having both SomeUser and User instead of just one type and having to know which one to use in any given situation; ew
displayActions u =
    ["Delete My Account (" ++ name u ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])

I do see something wrong with the original, and I believe it's what confused you. The "only" "good thing" in the original code is the existence of the token type. Using Proxy with a type parameter to construct the token type instead of doing

data AdminToken = AdminToken

is (IMO) pointless and confusing (both for understanding the technique and also in the resulting code). The type parameter is irrelevant to what makes the idea good, and you gain nothing by keeping the type parameter and not the token. I consider the following to be an actual improvement to the original while keeping its good idea.

data User = { userAdminToken :: Maybe AdminToken; userName :: String }
isAdmin :: User -> Bool
isAdmin = isJust . userAdminToken

displayActions :: User -> [String]
displayActions u
    ["Delete My Account (" ++ userName u ++ ")"] ++ (if isAdmin u then ["Delete Someone Else's Account"] else [])

Breckenridge

Answer 2

With the original code, you can write:

trustedUser = User (Just Proxy) "trusted"
untrustedUser = User Nothing "untrusted"

twoUsers :: [User] -- or Map Username User or whatever
twoUsers = [trustedUser, untrustedUser]

You can't make a similar twoUsers list with the second code snippet, because your trusted and untrusted users have different types.

Harod