but at the same time I need functions that can return a type that’s either an admin, a normal user, or not logged in at all.
login :: IO ???
login = do
userid <- login
userSession <- getUserSession userid
userRoles <- getUserRoles userid
if hasAdmin userRoles then Admin userSession
else User userSession
The way I’m handling this right now is by stacking lots and lots of types inside one another.
data Auth = None | Authenticated
data Authenticated = User UserSession | Admin
newtype Admin = Admin UserSession
which let’s me write functions that can work with any kind of auth foo :: Auth -> IO () or restricted to specific types of auth bar :: Admin -> IO ()
So what have I tried so far? It’s easy enough to do something with DataKinds:
data AuthStatus
= None
| AuthUser
| AuthAdmin
deriving (Show, Eq)
data Auth s a where
NotAuthenticated :: Auth None a
IsUser :: UserSession -> Auth AuthUser UserSession
IsAdmin :: UserSession -> Auth AuthAdmin UserSession
But this only achieves the first part, namely restricting functions to certain inputs. This doesn’t let me write a function that either returns or accepts just a general Auth thing, without immediately restricting it to just one variation.
Summary
I need a single type that can act both as a normal ADT but where I can also restrict functions to just a single constructor. I can achieve this by wrapping types inside another but that’s ugly. I’m wondering if there’s something else out there that I’m just not aware of.
The problem with this is that it requires me to handle Nothing in many places where a Nothing should never happen. I currently use the very verbose setup I have for route handlers. And certain route handlers make no sense for people who aren’t administrators. I therefore don’t want these to accept a Maybe User and then check if it’s Just and that the user has the admin role. I just want to say, at the type level, this thing only works with Admin.
Why do I even want to have the admin constraint in the type signature? Well I could of course just do the check in the parent function that calls that route handler. But having the constraint in the type signature means I can’t just forget to check if the user is an admin, it’s required to even use the route handler function.
With the smart constructors, refined package, and liquid haskell you can do the checks externally (in the place you authenticate for example, and then at the use sites you can specify in the types that you only want administrators. Then you don’t have to handle Maybes in unnecessary places.
As you mentioned you could use your GADT approach and wrap it in an existential when returning. This is unfortunately a bit heavyweight in current Haskell
data SomeAuth a where
SA :: Auth s a -> SomeAuth s a
The other way to encode this is a continuation which is probably worse
This doesn’t let me write a function that either returns or accepts just a general Auth thing, without immediately restricting it to just one variation.
The existential solves the problem quite nicely and honestly doesn’t seem like a lot of work. What it can’t do, I think, is restrict a function to TWO constructors, instead of just one.
In general, for authentication, a function that works with UserLevel should also work with AdminLevel
Here’s an example that you can run if you have Nix installed (also as a gist). If not, well, it only requires GHC, so you can probably just remove the first two lines.
$ chmod +x file.hs
$ ./file.hs
This snippet shows the use of an existential, as mentioned by @Tarmean. If you replace the login snippet with this:
login =
if False
then None
else User "I am Joe"
it won’t work, since the return type is restricted to one of the GADT branches.
#! /usr/bin/env nix-shell
#! nix-shell -p ghcid -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [])" -i "ghcid -c 'ghci -Wall' -T main"
-- Run this with
-- $ chmod +x ./file.hs
-- $ ./file.hs
--
-- See this thread https://discourse.haskell.org/t/how-to-restrict-function-to-certain-constructors/2785/7
-- for a discussion of the problem
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
main :: IO ()
main =
-- Change "admin" to "user" for the user session or any other string for the
-- NoAuthentication session
let session = login "koo"
in do
handleAnyAuthenticationLevel session
case session of
(HelperType adminSession@(Admin _)) -> handleOnlyAdmins adminSession
_ -> print "403"
data AuthenticationLevel
= NoAuthentication
| UserLevel
| AdminLevel
data Session authStatus sessionValue where
None :: Session 'NoAuthentication sessionValue
User :: String -> Session 'UserLevel String
Admin :: String -> Session 'AdminLevel String
data HelperType c where
HelperType :: Session a c -> HelperType c
-- This works
handleAnyAuthenticationLevel :: HelperType c -> IO ()
handleAnyAuthenticationLevel (HelperType None) =
print $ "handleAnyAuthenticationLevel: " ++ ":("
handleAnyAuthenticationLevel (HelperType (User value)) =
print $ "handleAnyAuthenticationLevel: " ++ value
handleAnyAuthenticationLevel (HelperType (Admin value)) =
print $ "handleAnyAuthenticationLevel: " ++ value
handleOnlyAdmins :: Session 'AdminLevel String -> IO ()
handleOnlyAdmins (Admin value) = print $ "handleOnlyAdmins: " ++ value
-- This compiles, thanks to the existential
login :: String -> HelperType String
login "admin" = HelperType $ Admin "I am an admin"
login "user" = HelperType $ User "I am a user"
login _ = HelperType None
-- This does not compile, since the return type is restricted to one of the
-- GADT branches
-- loginDoesNotCompile =
-- if False
-- then None
-- else User "I am Joe"