GHC compiler not complaining about incorrect code paths

Question

I'm approaching Haskell with a view of converting runtime errors to compile-time errors. I expect the compiler to figure out that all the code paths in the following code are not error free. If authorizeUser returns UnauthorizedCommand then the call to (command $ authorizeUser cmd userId) will fail during runtime.

data Command = UnauthorizedCommand | Command {command :: String, userId :: String}

authorizedUsers = ["1", "2", "3"]

authorizeUser :: String -> String -> Command
authorizeUser cmd userId = if (userId `elem` authorizedUsers) then Command {command=cmd, userId=userId} else UnauthorizedCommand

main :: IO ()
main = do
  cmd <- getLine
  userId <- getLine
  case (command $ authorizeUser cmd userId) of
    "ls" -> putStrLn "works"
    _ -> putStrLn "not authorized"

Is there a compiler switch to enable such checking?

I've the impression that you want check user input. If you are waiting data from the user, you'll never be able to do a compile check on his entry. You only can "compile check" code you write. Can you clarify what you want check ? — Sebastien, Feb 08 '16 at 09:34

score 5 · Answer 1 · answered Feb 08 '16 at 11:10

The main problem in this example is that using the record syntax in a data type with multiple constructors can end up with record selector functions that are partial. It's therefore not recommended to ever mix records and multiple constructors unless all constructors have identical record fields.

The simplest solution is to not use record syntax here and to define your own command accessor which makes the error case explicit with a Maybe return type:

data Command = UnauthorizedCommand | Command String String

command :: Command -> Maybe String
command UnauthorizedCommand = Nothing
command (Command cmd _)     = Just cmd

A slightly more complex way to check this during compile time is to use GADTs to encode the permission level in the types.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

data Permission
  = Authorized | Unauthorized

data Command p where
  UnauthorizedCommand :: Command Unauthorized
  Command :: {command :: String, userId :: String} -> Command Authorized

Now the type of the command selector is Command Authorized -> String so you get a compile time error if you try to use it with an unauthorized command.

This seems promising. Although it would've been better if it would've been possible without the type-related boilerplate. Your second approach, GADTs, went over my head. Is there a gentle introduction to GADTs that you can recommend? — Saurabh Nanda, Feb 08 '16 at 16:10
how do I write a function which returns `Command p`? I tried the following but it didn't work: http://lpaste.net/151949 How does one practically use this approach to do what I'm trying to do? — Saurabh Nanda, Feb 09 '16 at 13:12

Sebastien · Answer 2 · 2016-02-08T09:47:54.340

You can use the "case" only on authorizeUser and then filter the DATA Command

data Command = UnauthorizedCommand | Command {command :: String, userId :: String}

authorizedUsers = ["1", "2", "3"]

authorizeUser :: String -> String -> Command
authorizeUser cmd userId = if (userId `elem` authorizedUsers) then Command {command=cmd, userId=userId} else UnauthorizedCommand

main :: IO ()
main = do
  cmd <- getLine
  userId <- getLine
  case  authorizeUser cmd userId of
    Command "ls" _ -> putStrLn "works"
    _ -> putStrLn "not authorized" -- either the user id is not good or the command is not good.

If you have several command, you can also do:

main = do
  cmd <- getLine
  userId <- getLine
  case  authorizeUser cmd userId of

    Command _ _ -> case cmd of
        "ls" -> putStrLn "works"
        "cd" -> putStrLn "moved!"
        _ -> putStrLn "Bad command!"
    _ -> putStrLn "not authorized" -- or: Unauthorized -> putStrLn "Not authorized"

PS : Note you can factor the putStrLns

score 1 · Answer 3 · edited May 23 '17 at 12:23

I think I've finally understand your question: you want Haskell generate error/warning when calling command on an arbitrary Command. It is related to this answer : https://stackoverflow.com/a/3804900/3421913 . In short:

It is not possible to check (or very very hard) at compile time if a command is Command Str Str or Unauthorized: in your case it is quite simple, but it might be more complex.
You sometimes know that your value has the good property but it's difficult to express that in haskell (see the linked answer above with the duplicates/remove_duplicates functions). In your case, authorizeUser cmd userId is unsafe (since cmd and userId are user input), so we won't use the command function which will fail if the user is a monkey. Instead, we'll use the pattern matching I've proposed in my other answer. If you have some invariant ensuring that c::Command is not Unauthorized, you might use directly command.

This could have been added to your other answer as an edit. It is possible to post multiple answers on SO, but they are not commonly found. I do not perfectly know the guidelines, but I believe multiple answers should be reserved to completely different approaches to the problem. — chi, Feb 08 '16 at 10:55

GHC compiler not complaining about incorrect code paths

3 Answers3