Codifying presence/absence of authentication at type level
Context: I'm approaching Haskell from a standpoint of converting runtime errors to compile-time errors. My hypothesis is that this is possible if one can codify business logic within the program's types itself.
I'm writing a Telegram bot, which should be accessible by users within my company. To achieve this "restriction", whenever someone starts chatting with the bot it will look up the chat_id in a table and check if a valid oauth_token exists. If not, the user will first be sent a link to complete a Google OAuth (our company's email is hosted on Google Apps for Business).
Users with a valid oauth_token will be able to give the Telegram bot some commands, which unauthenticated users should not be able to give.
Now, I'm trying to codify this logic at the type level itself. There will be some functions in my Haskell code that will have the ability to accept, as arguments, both, authenticated & unauthenticated users; while some functions should accept only authenticated users.
If I keep passing user objects of the same type, i.e. VLUser everywhere, then I will have to be careful to check for the presence of oauthToken in every function. Is there a way to create two user types - VLUser and VLUserAuthenticated where:
Both map to the same underlying table
A VLUserAuthenticated can be instantiated ONLY IF it has an oauthToken
data Unknown -- unknown users
data Authenticated -- verified users
newtype User a i = Id i deriving Show
It is important that the data constructor Id is not exposed to user, but the module provides functions to initialize and authenticate users:
-- initializes an un-authenticated user
newUser :: i -> User Unknown i
newUser = Id
-- authenticates a user
authUser :: (User a i) -> User Authenticated i
authUser (Id i) = Id i -- dummy implementation
then, you may control access at the type level without code duplication, without run-time checks and without run-time cost:
-- open to all users
getId :: User a i -> i
getId (Id i) = i
-- only authenticated users can pass through
getId' :: User Authenticated i -> i
getId' (Id i) = i
For example, if
\> let jim = newUser "jim"
\> let joe = authUser $ newUser "joe"
joe is an authenticated user and can be passed to either function:
\> getId joe
\> getId' joe
whereas, you will get compile-time error if you call getId' with jim:
\> getId jim
\> getId' jim -- compile-time error! not run-time error!
Couldn't match type ‘Unknown’ with ‘Authenticated’
Expected type: User Authenticated [Char]
Actual type: User Unknown [Char]
In the first argument of ‘getI
Asked in February 2016Viewed 3,361 timesVoted 10Answered 1 times