| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
| Extensions |
|
Libjwt.PrivateClaims
Description
Collection of functions, types and type families that are needed to implement type-safe private claims.
This is essentially an implementation of open product type as described in Sandy Maguire "Thinking with Types".
The only difference to the book is that the implementation is backed by HashMap to make lookups by name easier.
In addition, there are also FromPrivateClaims and ToPrivateClaims type-classes and
view pattern :< to help create and deconstruct values.
Synopsis
- data Claim (a :: Type) = Grant Symbol a
- type (->>) name a = 'Grant name a
- data Namespace
- class KnownNamespace (ns :: Namespace) where
- namespaceValue :: proxy ns -> Maybe String
- data ClaimName (name :: Symbol) = ClaimName
- claimNameVal :: forall name. KnownSymbol name => ClaimName name -> String
- data Ns (ns :: Symbol) = Ns
- data ClaimWitness (name :: Symbol) a
- testify :: ClaimWitness name a -> a
- (->>) :: ClaimName name -> a -> ClaimWitness name a
- data PrivateClaims (ts :: [Claim Type]) (ns :: Namespace)
- type Empty = '[] :: [Claim Type]
- nullClaims :: PrivateClaims Empty 'NoNs
- addClaim :: forall name a ts ns. CanAdd name ts => ClaimName name -> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) ': ts) ns
- (.:) :: forall name a ts ns. CanAdd name ts => ClaimWitness name a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) ': ts) ns
- type family CanAdd n ns :: Constraint where ...
- type family RestrictedName (name :: Symbol) :: Bool where ...
- getClaim :: forall name ts ns. CanGet name ts => ClaimName name -> PrivateClaims ts ns -> LookupClaimType name ts
- (.!) :: forall name ts ns. CanGet name ts => PrivateClaims ts ns -> ClaimName name -> LookupClaimType name ts
- type family CanGet n ns :: Constraint where ...
- type family LookupClaimType (name :: Symbol) (ts :: [Claim Type]) :: Type where ...
- pattern (:<) :: KnownSymbol name => a -> PrivateClaims tl ns -> PrivateClaims ((name ->> a) ': tl) ns
- withNs :: ToPrivateClaims a => Ns ns -> a -> PrivateClaims (Claims a) ('SomeNs ns)
- someNs :: Ns ns -> PrivateClaims ts 'NoNs -> PrivateClaims ts ('SomeNs ns)
- noNs :: PrivateClaims ts any -> PrivateClaims ts 'NoNs
- class ToPrivateClaims a where
- type Claims a :: [Claim Type]
- type OutNs a :: Namespace
- toPrivateClaims :: a -> PrivateClaims (Claims a) (OutNs a)
- class FromPrivateClaims a where
- fromPrivateClaims :: ts ~ Claims a => PrivateClaims ts ns -> a
Kinds
data Claim (a :: Type) Source #
Kind of claims
A claim is made up of a type-level literal and a type (this is essentialy a type-level tuple (Symbol, *))
Instances
type (->>) name a = 'Grant name a infix 6 Source #
A convenient alias.
Let's you write '["claimName" ->> Int, "anotherName" ->> String] to indicate a list of types of kind Claim,
instead of '[Grant "claimName" Int, Grant "anotherName" String],
Kind of namespaces
These types represent a URL-like claim prefix
class KnownNamespace (ns :: Namespace) where Source #
Class of Namespace with known compile-time value
Instances
| KnownNamespace 'NoNs Source # | |
Defined in Libjwt.PrivateClaims | |
| KnownSymbol ns => KnownNamespace ('SomeNs ns) Source # | |
Defined in Libjwt.PrivateClaims | |
Value-level counterparts
data ClaimName (name :: Symbol) Source #
Type-level literal representing a claim name
Can be used with -XOverloadedLabels
Constructors
| ClaimName |
claimNameVal :: forall name. KnownSymbol name => ClaimName name -> String Source #
Retrieve the string associated with ClaimName
data Ns (ns :: Symbol) Source #
Type-level literal representing a namespace
Can be used with -XOverloadedLabels
(the limited label syntax makes this rarely possibble though, a more common use is to write Ns @"https:example.com")
Constructors
| Ns |
data ClaimWitness (name :: Symbol) a Source #
Keeps the value of type a and the name (type-level) with which it is associated
Instances
testify :: ClaimWitness name a -> a Source #
(->>) :: ClaimName name -> a -> ClaimWitness name a infix 6 Source #
Associate name with a value
With -XOverloadedLabels
>>>:t #someName ->> True#someName ->> True :: ClaimWitness "someName" Bool
Private claims type
data PrivateClaims (ts :: [Claim Type]) (ns :: Namespace) Source #
Container of named claims ts, possibly prefixed with some namespace ns
For example PrivateClaims '["string" denotes a structure containing
a String under the "string" key plus an int under the "int" key.
There is no namespace, so the keys will not be prefixed by any prefix when serializing the structure->> String, "int" ->> Int] 'NoNs
Instances
Construction
nullClaims :: PrivateClaims Empty 'NoNs Source #
Empty claims
addClaim :: forall name a ts ns. CanAdd name ts => ClaimName name -> a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) ': ts) ns Source #
Insert the claim.
The claim can be safely added iff:
- there is no claim of the same
namein the container, - its name is not the name of any public claim (like iss or sub)
Otherwise it is a compile-time error (see CanAdd constraint)
With -XOverloadedLabels
>>>addClaim #string "Value of claim" nullClaims(#string ->> "Value of claim")
With -XTypeApplications and -XDataKinds
>>>addClaim (ClaimName @"string") "Value of claim" nullClaims(#string ->> "Value of claim")
(.:) :: forall name a ts ns. CanAdd name ts => ClaimWitness name a -> PrivateClaims ts ns -> PrivateClaims ((name ->> a) ': ts) ns infixr 5 Source #
Alias for addClaim (binds to the right)
With -XOverloadedLabels
>>>#string ->> "Value of claim" .: nullClaims(#string ->> "Value of claim")
type family CanAdd n ns :: Constraint where ... Source #
Constraint specifying when a claim named n can be added to the list of claims ns
Satisfied iff:
nis a type-level literal,- in the names of
nsclaims there is non(uniqueness), nis not one of the restricted names (seeRestrictedName)
>>>:kind! CanAdd "name" '["n1" ->> Int, "n2" ->> String]CanAdd "name" '["n1" ->> Int, "n2" ->> String] :: Constraint = (GHC.TypeLits.KnownSymbol "name", () :: Constraint, () :: Constraint)
>>>:kind! CanAdd "n1" '["n1" ->> Int, "n2" ->> String]CanAdd "n1" '["n1" ->> Int, "n2" ->> String] :: Constraint = (GHC.TypeLits.KnownSymbol "n1", () :: Constraint, (TypeError ...))
Equations
| CanAdd n ns = (KnownSymbol n, DisallowRestrictedName (RestrictedName n) n, RequireUniqueName (UniqueName n ns) n) |
type family RestrictedName (name :: Symbol) :: Bool where ... Source #
Equations
| RestrictedName "iss" = 'True | |
| RestrictedName "sub" = 'True | |
| RestrictedName "aud" = 'True | |
| RestrictedName "exp" = 'True | |
| RestrictedName "nbf" = 'True | |
| RestrictedName "iat" = 'True | |
| RestrictedName "jti" = 'True | |
| RestrictedName _ = 'False |
Lookup
getClaim :: forall name ts ns. CanGet name ts => ClaimName name -> PrivateClaims ts ns -> LookupClaimType name ts Source #
Look up the claim value associated with name.
Value can be retrieved if proven to exists in the container.
Otherwise it is a compile-time error (see CanGet constraint)
With -XOverloadedLabels
>>>getClaim #bool $ #string ->> "Value of claim" .: #bool ->> False .: nullClaimsFalse
(.!) :: forall name ts ns. CanGet name ts => PrivateClaims ts ns -> ClaimName name -> LookupClaimType name ts Source #
Alias for getClaim (container goes first)
With -XOverloadedLabels
>>>(#string ->> "Value of claim" .: #bool ->> False .: nullClaims) .! #boolFalse
type family CanGet n ns :: Constraint where ... Source #
Constraint specifying when a claim named n can be looked up in the list of claims ns
Satisfied iff ns contains a claim named n and n is a type-level literal
>>>:kind! CanGet "n1" '["n1" ->> Int, "n2" ->> String]CanGet "n1" '["n1" ->> Int, "n2" ->> String] :: Constraint = (GHC.TypeLits.KnownSymbol "n1", () :: Constraint)
>>>:kind! CanGet "n" '["n1" ->> Int, "n2" ->> String]CanGet "n" '["n1" ->> Int, "n2" ->> String] :: Constraint = (GHC.TypeLits.KnownSymbol "n", (TypeError ...))
Equations
| CanGet n ns = (KnownSymbol n, RequireExists (NameExists n ns) n) |
type family LookupClaimType (name :: Symbol) (ts :: [Claim Type]) :: Type where ... Source #
Looks up the type associated with name in the '[n1 pairs list. Gets stuck if ->> a, n2 ->> b, ...]name is not in ts
>>>:kind! LookupClaimType "n1" '["n1" ->> Int, "n2" ->> String]LookupClaimType "n1" '["n1" ->> Int, "n2" ->> String] :: * = Int
Equations
| LookupClaimType n ((n ->> a) ': _) = a | |
| LookupClaimType n (_ ': rest) = LookupClaimType n rest |
Patern matching
pattern (:<) :: KnownSymbol name => a -> PrivateClaims tl ns -> PrivateClaims ((name ->> a) ': tl) ns infixr 5 Source #
Extract values from the container in the order in which they appear in the claim list
Namespaces
withNs :: ToPrivateClaims a => Ns ns -> a -> PrivateClaims (Claims a) ('SomeNs ns) Source #
Convert to private claims with some namespace
someNs :: Ns ns -> PrivateClaims ts 'NoNs -> PrivateClaims ts ('SomeNs ns) Source #
Set namespace
noNs :: PrivateClaims ts any -> PrivateClaims ts 'NoNs Source #
Unset namespace
Conversions
class ToPrivateClaims a where Source #
Class of types that can be converted to PrivateClaims
Minimal complete definition
Nothing
Instances
class FromPrivateClaims a where Source #
Class of types that can be constructed from PrivateClaims
Minimal complete definition
Nothing
Methods
fromPrivateClaims :: ts ~ Claims a => PrivateClaims ts ns -> a Source #
Convert from claims
default fromPrivateClaims :: (Generic a, RecordFromPrivateClaims (Rep a), ts ~ ClaimsFromRecord (Rep a)) => PrivateClaims ts ns -> a Source #