Is this code possible? - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Disco Dave

Is there anyway to get the isAuthorized' function to work?

import           Data.Kind                      ( Constraint
                                                , Type
                                                )
import           Data.Proxy                     ( Proxy(..) )

class IsAuthorized claim user where
  isAuthorized :: Proxy claim -> user -> Bool

data CombineLogic = And | Or

data Authorize' (combineLogic :: CombineLogic) (claims :: [Type]) (user :: Type)

type Authorize (claim :: Type) (user :: Type) = Authorize' 'And '[claim] user
type AuthorizeAll (claims :: [Type]) (user :: Type) = Authorize' 'And claims user
type AuthorizeAny (claims :: [Type]) (user :: Type) = Authorize' 'Or claims user

type family IsAuthorizedConstraints (claims :: [a]) (user :: Type) :: Constraint where
  IsAuthorizedConstraints '[] _ = ()
  IsAuthorizedConstraints (claim ': claims) user =
    (IsAuthorized claim user, IsAuthorizedConstraints claims user)

type family IsNonEmpty (xs :: [a]) :: Bool where
  IsNonEmpty '[] = 'False
  IsNonEmpty _   = 'True

type family Head (xs :: [a]) :: Maybe a where
  Head '[]       = 'Nothing
  Head (a ': _)  = 'Just a

type family Tail (xs :: [a]) :: [a] where
  Tail '[]        = '[]
  Tail (_ ': xs)  = xs

data SCombineLogic (c :: CombineLogic) where
  SOr :: SCombineLogic 'Or
  SAnd :: SCombineLogic 'And

class GetCombineLogic (c :: CombineLogic) where
  getCombineLogic :: SCombineLogic c
instance GetCombineLogic 'Or where
  getCombineLogic = SOr
instance GetCombineLogic 'And where
  getCombineLogic = SAnd

data SMaybe (m :: Maybe a) where
  SNothing :: SMaybe 'Nothing
  SJust :: Proxy a -> SMaybe ('Just a)

class GetMaybe (m :: Maybe Type) where
  getMaybe :: SMaybe m
instance GetMaybe 'Nothing where
  getMaybe = SNothing
instance GetMaybe ('Just a) where
  getMaybe = SJust (Proxy @a)


combineLogic
  :: forall combineLogic
   . GetCombineLogic combineLogic
  => Proxy combineLogic
  -> (Bool -> Bool -> Bool, Bool)
combineLogic _ = case getCombineLogic @combineLogic of
  SOr  -> ((||), False)
  SAnd -> ((&&), True)

isAuthorized'
  :: forall claims user cl a
   . ( IsAuthorizedConstraints claims user
     , GetCombineLogic cl
     , GetMaybe (Head claims)
     )
  => Proxy (Authorize' cl claims user)
  -> user
  -> Bool
isAuthorized' _ user =
  let (combine, def) = combineLogic (Proxy @cl)
  in case getMaybe @(Head claims) of
    SNothing -> def
    SJust claim -> isAuthorized claim user `combine` isAuthorized' nextClaims user
      where nextClaims = Proxy @(Authorize' cl (Tail claims) user)




newtype User = User { fromUser :: String }

instance IsAuthorized IsAdmin User where
  isAuthorized _ _ = True
instance IsAuthorized IsPremium User where
  isAuthorized _ _ = False

data IsAdmin
data IsPremium

type Claims = AuthorizeAll '[IsPremium, IsAdmin] User

_ = isAuthorized' (Proxy @Claims) (User "john.doe")
Lysxia

What is the error message? That's a pretty big piece of code for one to assimilate without context.

Disco Dave

Lol, yeah. Sorry. Wasn't sure the best way to ask.

/home/disco/Documents/code/haskell/servant-auth-playground/src/Authorization.hs:81:20: error:
    • Could not deduce (IsAuthorized a1 user)
        arising from a use of ‘isAuthorized’
      from the context: (IsAuthorizedConstraints claims user,
                         GetCombineLogic cl, GetMaybe (Head claims))
        bound by the type signature for:
                   isAuthorized' :: forall k (claims :: [*]) user (cl :: CombineLogic) (a :: k).
                                    (IsAuthorizedConstraints claims user, GetCombineLogic cl,
                                     GetMaybe (Head claims)) =>
                                    Proxy (Authorize' cl claims user) -> user -> Bool
        at src/Authorization.hs:(68,1)-(76,9)
      or from: Head claims ~ 'Just a1
        bound by a pattern with constructor:
                   SJust :: forall a1 (a2 :: a1). Proxy a2 -> SMaybe ('Just a2),
                 in a case alternative
        at src/Authorization.hs:81:5-15
    • In the first argument of ‘combine’, namely
        ‘isAuthorized claim user’
      In the expression:
        isAuthorized claim user `combine` isAuthorized' nextClaims user
      In a case alternative:
          SJust claim
            -> isAuthorized claim user `combine` isAuthorized' nextClaims user
            where
                nextClaims = Proxy @(Authorize' cl (Tail claims) user)
   |
81 |     SJust claim -> isAuthorized claim user `combine` isAuthorized' nextClaims user
   |                    ^^^^^^^^^^^^^^^^^^^^^^^

/home/disco/Documents/code/haskell/servant-auth-playground/src/Authorization.hs:81:54: error:
    • Could not deduce: IsAuthorizedConstraints (Tail claims) user
        arising from a use of ‘isAuthorized'’
      from the context: (IsAuthorizedConstraints claims user,
                         GetCombineLogic cl, GetMaybe (Head claims))
        bound by the type signature for:
                   isAuthorized' :: forall k (claims :: [*]) user (cl :: CombineLogic) (a :: k).
                                    (IsAuthorizedConstraints claims user, GetCombineLogic cl,
                                     GetMaybe (Head claims)) =>
                                    Proxy (Authorize' cl claims user) -> user -> Bool
        at src/Authorization.hs:(68,1)-(76,9)
      or from: Head claims ~ 'Just a1
        bound by a pattern with constructor:
                   SJust :: forall a1 (a2 :: a1). Proxy a2 -> SMaybe ('Just a2),
                 in a case alternative
        at src/Authorization.hs:81:5-15
    • In the second argument of ‘combine’, namely
        ‘isAuthorized' nextClaims user’
      In the expression:
        isAuthorized claim user `combine` isAuthorized' nextClaims user
      In a case alternative:
          SJust claim
            -> isAuthorized claim user `combine` isAuthorized' nextClaims user
            where
                nextClaims = Proxy @(Authorize' cl (Tail claims) user)
    • Relevant bindings include
        nextClaims :: Proxy (Authorize' cl (Tail claims) user)
          (bound at src/Authorization.hs:82:13)
        user :: user (bound at src/Authorization.hs:77:17)
        isAuthorized' :: Proxy (Authorize' cl claims user) -> user -> Bool
          (bound at src/Authorization.hs:77:1)
   |
81 |     SJust claim -> isAuthorized claim user `combine` isAuthorized' nextClaims user
   |                                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

/home/disco/Documents/code/haskell/servant-auth-playground/src/Authorization.hs:81:54: error:
    • Could not deduce (GetMaybe (Head (Tail claims)))
        arising from a use of ‘isAuthorized'’
      from the context: (IsAuthorizedConstraints claims user,
                         GetCombineLogic cl, GetMaybe (Head claims))
        bound by the type signature for:
                   isAuthorized' :: forall k (claims :: [*]) user (cl :: CombineLogic) (a :: k).
                                    (IsAuthorizedConstraints claims user, GetCombineLogic cl,
                                     GetMaybe (Head claims)) =>
                                    Proxy (Authorize' cl claims user) -> user -> Bool
        at src/Authorization.hs:(68,1)-(76,9)
      or from: Head claims ~ 'Just a1
        bound by a pattern with constructor:
                   SJust :: forall a1 (a2 :: a1). Proxy a2 -> SMaybe ('Just a2),
                 in a case alternative
        at src/Authorization.hs:81:5-15
    • In the second argument of ‘combine’, namely
        ‘isAuthorized' nextClaims user’
      In the expression:
        isAuthorized claim user `combine` isAuthorized' nextClaims user
      In a case alternative:
          SJust claim
            -> isAuthorized claim user `combine` isAuthorized' nextClaims user
            where
                nextClaims = Proxy @(Authorize' cl (Tail claims) user)
   |
81 |     SJust claim -> isAuthorized claim user `combine` isAuthorized' nextClaims user
   |                                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Lysxia

From Head claims = 'Just claim GHC won't infer that claims = claim ': _

Lysxia

Instead of a GetMaybe class, start by passing the GADT explicitly. And instead of SMaybe, which will only give you one element Head claims, you need a type witness for the whole list claims.

data TList :: [Type] -> Type where
  TNil :: TList '[]
  TCons :: TList xs -> TList (x ': xs)

isAuthorized' :: ...
   => TList claims
   -> ...
Disco Dave

What about this? I think this is simpler.

module Authorization
  ( IsAuthorized(..)
  , Authorize
  , AuthorizeAll
  , AuthorizeAny
  )
where

import           Data.Kind                      ( Type )
import           Data.Proxy                     ( Proxy(..) )


class IsAuthorized claim user where
  isAuthorized :: Proxy claim -> user -> Bool

instance IsAuthorizedMany (Authorize' cl claims user) user => IsAuthorized (Authorize' cl claims user) user where
  isAuthorized = isAuthorizedMany

data CombineLogic = And | Or

data Authorize' (combineLogic :: CombineLogic) (claims :: [Type]) (user :: Type)

type Authorize (claim :: Type) (user :: Type) = Authorize' 'And '[claim] user
type AuthorizeAll (claims :: [Type]) (user :: Type) = Authorize' 'And claims user
type AuthorizeAny (claims :: [Type]) (user :: Type) = Authorize' 'Or claims user

class IsAuthorizedMany claims user where
  isAuthorizedMany :: Proxy claims -> user -> Bool

instance IsAuthorizedMany (Authorize' 'And '[] _user) _user where
  isAuthorizedMany _ _ = True

instance (IsAuthorized claim user
         , IsAuthorizedMany (Authorize' 'And claims user) user
         )
      => IsAuthorizedMany (Authorize' 'And (claim ': claims) user) user where
  isAuthorizedMany _ user =
    isAuthorized (Proxy @claim) user
      && isAuthorizedMany (Proxy @(Authorize' 'And claims user)) user

instance IsAuthorizedMany (Authorize' 'Or '[] _user) _user where
  isAuthorizedMany _ _ = False

instance (IsAuthorized claim user
         , IsAuthorizedMany (Authorize' 'Or claims user) user
         )
      => IsAuthorizedMany (Authorize' 'Or (claim ': claims) user) user where
  isAuthorizedMany _ user =
    isAuthorized (Proxy @claim) user
      || isAuthorizedMany (Proxy @(Authorize' 'Or claims user)) user
Disco Dave

Also Zulip's haskell highlighting is confused XD

Disco Dave

And this seems to magically work. At least with this simple example.

data IsAdmin
data IsPremium

newtype FakeUser = FakeUser { fromUser :: String }

instance IsAuthorized IsAdmin FakeUser where
  isAuthorized _ _ = True
instance IsAuthorized IsPremium FakeUser where
  isAuthorized _ _ = False

type MyClaims = AuthorizeAll '[IsPremium, IsAdmin] FakeUser

shouldBeFalse = isAuthorized (Proxy @(AuthorizeAll '[IsPremium, IsAdmin] FakeUser)) (FakeUser "john.doe")
shouldBeTrue = isAuthorized (Proxy @(AuthorizeAny '[IsPremium, IsAdmin] FakeUser)) (FakeUser "john.doe")
Lysxia

Also Zulip's haskell highlighting is confused XD

(I just made a PR to pygments to fix it)

Disco Dave

Oh wow that's awesome :D

Disco Dave

The only weird part about this is that AuthorizeAny with an empty list is False and AuthorizeAll with an empty list is True

Lysxia

Weird but monoidal.

Disco Dave

The intention is to use this as a servant combinator. So I think I could just write my HasServer instance to required the claims list as non empty.