How to restrict function to certain constructors

Learn
#1

I’m aware of this StackOverflow question but my question goes one step beyond what’s asked there.

I’m trying to model authentication in a web app in a way that I can have functions that require a user to be an admin

scaryStuff :: ??? -> IO ()
scaryStuff (Admin UserSession {..}) = undefined

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.

1 Like
#2

I just wrote an answer to a related question on stackoverflow: https://stackoverflow.com/a/68446500/15207568

I would say the simplest way is to change your scaryStuff to allow more inputs, but then return a Maybe:

scaryStuff :: Auth -> Maybe (IO ())
scaryStuff Admin = Just ...
scaryStuff _ = Nothing

(Perhaps you can use MaybeT IO () instead for better ergonomics in some cases)

If you have many scaryStuff functions then it might be easier to have a separate checking function:

newtype IsAdmin = IsAdmin Auth

mkIsAdmin :: Auth -> Maybe IsAdmin
mkIsAdmin Admin = Just Admin
mkIsAdmin _ = Nothing

scaryStuff :: IsAdmin -> IO ()
scaryStuff = ...

You can make use of the refined package which has some built-in functionality:

{-# LANGUAGE DataKinds, FlexibleContexts, MultiParamTypeClasses, TypeApplications, ScopedTypeVariables, DeriveLift #-}
module AuthTypes where

import Refined
import Data.Proxy
import Language.Haskell.TH.Syntax (Lift)

data Auth = None | User | Admin deriving Lift

data AuthLevel p = AuthLevel

authLevel :: Auth -> Int
authLevel None  = 0
authLevel User  = 1
authLevel Admin = 2

instance forall p. Predicate p Int => Predicate (AuthLevel p) Auth where
  validate _ x = validate (Proxy @p) (authLevel x)

{-# LANGUAGE DataKinds, TemplateHaskell #-}
import AuthTypes
import Refined

scaryStuff :: Refined (AuthLevel (From 2)) Auth -> IO ()
scaryStuff _ = putStrLn "Launch missiles!"

main :: IO ()
main = do
  scaryStuff $$(refineTH Admin)
  scaryStuff $$(refineTH User) -- error

And you can make this even more convenient by using LIquid Haskell:


module Auth where

data Auth = None | User | Admin

{-@ measure authLevel @-}
authLevel :: Auth -> Int
authLevel None = 0
authLevel User = 1
authLevel Admin = 2

{-@ type Admin = { x:Auth | authLevel x == 2 } @-}

{-@ scaryStuff :: Admin -> IO () @-}
scaryStuff Admin = putStrLn "Launch missiles!"

main = do
  scaryStuff Admin
  scaryStuff User -- error

Try it here

1 Like
#3

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.

#4

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.

#5

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

 withAuth :: (forall s. Auth s a -> IO r) -> IO r
#6

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.

Why not? Can you provide an example?

#7

Sorry for the late reply!

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"