What if your compiler could be even more pedantic than Rust in preventing you from shooting yourself in the foot? What if we could weaponize the nitpicking power of the achtually meme persona so it’s pretty much impossible to forget to apply security constraints?

Dream no more, my dear reader, Lean 4 is here to help you atone for being mere, flawed flesh that sometimes forgets to use the gated constructor with a massive DO NOT USE ANY OTHER CONSTRUCTOR on top and ignores the deprecation warnings put on the other one just to be consumed by the gated one.

I recently stumbled upon this great article by Hayley Brinicombe — if it’s too long for you, you can read this other link — and thought: What if the helpful constructors laid out in that article were instead high-achieving arseholes that would get in your way if you try to bypass them, and the macros that called them were instead helpers that hide the need for the logic while keeping the checks consistent?

That led to a frenzy of a few minutes of writing the code for this article, followed by four weeks of absolute neglect, where just a few lines were written at night, at weekends, but enough of them made an article so…

Let’s start with some naive authentication typing, we have a user and an error type. Inductive types in Lean are a concept larger than discriminated unions, but for our current use case, in this context, they are discriminated unions.

structure User where
  sub : String
  roles : HashSet String

inductive ApiError where
  | notFound : ApiError
  | unauthorized : ApiError
  | forbidden : String → ApiError
  -- We'll get back to this case later on
  | utterDisaster : ApiError → ApiError

Some naive storage backend, in this case, we have a warehouse that has an inventory with the stock of every product, and we can make requests.

structure Warehouse where
  inventory : HashMap String Nat

structure WitdrawalRequest where
  itemId : String
  amount : Nat

Fulfilling an order from the warehouse requires the role "warehouse-management", so a function for that would look something like this:

def canThisUserFulfil
    (wh : Warehouse)
    (r : WitdrawalRequest)
    (user : User)
    : Except ApiError Bool := do
  if user.roles.contains "warehouse-management"
     || user.roles.contains "admin"
  then
    match wh.inventory.get? r.itemId with
    | some stock => pure <| stock >= r.amount
    | none => throw .notFound
  else
    throw <| ApiError.forbidden
      "User does not have required role: warehouse-management"

That’s alright when you have only a few endpoints, and they all require roles, but what happens when you have endpoints that everyone can use, other that everyone authenticated can use, and ones that require a role? Something you would model like this:

inductive SecurityLevel where
  | everyone
  | authenticated
  | requiredRole (role : String)

An abstraction of an endpoint is now doable, and here is where the dark magic begins, because Lean 4 is a polymorphic language in the mathematical sense.

What do I mean with “in the mathematical sense”? You might ask.

No mainstream programming language is polymorphic in the mathematical sense.

I would answer.

Lean achieves polymorphism with dependent types, which allows the shape of a type to evolve as its constraints are satisfied, so if we were to define a signature for an endpoint without true polymorphism, what would be the type of the endpoint?

inductive EndpointHandler (α : Type) where
  | everyone (handler : Option User → Except ApiError α)
  | authenticated (handler : User → Except ApiError α)
  | requiredRole (role : String) (handler : User → Except ApiError α)

So the function that would wrap the endpoint to apply security would look like:

def myEndpoint
    (securityLevel : SecurityLevel)
    (handler : EndpointHandler α)
    (maybeUser : Option User)
    : Except ApiError α :=
  match securityLevel, handler with
  | SecurityLevel.everyone,
    EndpointHandler.everyone h =>
    h maybeUser
  | SecurityLevel.authenticated,
    EndpointHandler.authenticated h =>
    match maybeUser with
    | some user => h user
    | none => throw .unauthorized
  | SecurityLevel.requiredRole role,
    EndpointHandler.requiredRole handlerRole h =>
    if handlerRole != role then
      throw <| ApiError.utterDisaster
        s!"Security level and handler role mismatch: {role} vs {handlerRole}"
    else
      match maybeUser with
      | some user =>
        if user.roles.contains handlerRole || user.roles.contains "admin"
        then h user
        else throw <| ApiError.forbidden
          s!"User does not have required role: {handlerRole}"
      | none => throw .unauthorized
  | _, _ => throw <| ApiError.utterDisaster
    "Security level and handler type do not match"

And this is the issue, the .utterDisaster case has no reason to exist, because this can be gated at compilation time thanks to the wonders of polymorphism, first of all, we define a type UserWithRole, which is a sub type of a User “in the mathematical sense”.

Oh, boy…

As far as I know, TypesCrypt is the only mainstream language that has some degree of sub typing in the mathematical sense.

A sub type is not about inheritance, but about defining a slice of an existing type.

def UserWithRole (r : String) : Type :=
  { u : User // u.roles.contains r = true || u.roles.contains "admin" = true }

-- With some abbreviation to make it more intuitive:
abbrev HasRole (u : User) (r : String) : Prop :=
  u.roles.contains r = true || u.roles.contains "admin" = true

def UserWithRole (r : String) : Type :=
  { u : User // HasRole u r }

Now UserWithRole "warehouse-manager" can only be constructed with a user that has said role, this is compile time enforced, and there’s no way around it, we need to provide an actual proof that the user has the role.

def tryMakeUserWithRole
    (user : User)
    (role : String)
    : Except ApiError (UserWithRole role) :=
  if holds : HasRole user role
  then pure ⟨user, holds⟩
  else throw <| ApiError.forbidden
    s!"User does not have required role: {role}"

So the type of a handler now would look a bit different if we use this power:

inductive Handler {α} : SecurityLevel → Type _ where
  | everyone
    (handler : Option User -> Except ApiError α)
    : Handler .everyone
  | authenticated
    (handler : User -> Except ApiError α)
    : Handler .authenticated
  | requiredRole
    (role : String)
    (handler : UserWithRole role -> Except ApiError α)
    : Handler (.requiredRole role)

The type of Handler is SecurityLevel → Type _ where which means — ignore the underscore, we’re deep into it now, but not THAT deep — which means that a type is constructed by providing a security level. This is not a type, is a type constructor.

And this is the point when one usually flips the table, and decides to go out for a walk in an unsavory neighbourhood known for daylight armed robbery in order to feel safer again.

Hold on, though, because with this structure, and a bit of glue, we arrive at an elegant, completely type-safe structure to define our endpoints.

First the scary glue, which I will explain in depth in another article:

/-- Anything that can stand in for a `Handler`. `α` and `level` are `outParam`s,
    so the *source* type drives inference of the security level — which a plain
    `Coe` can't do, since `endpoint`'s `level` is otherwise an undetermined
    metavar at the call site. -/
class ToHandler
    (H : Type _)
    (α : outParam (Type _))
    (level : outParam SecurityLevel)
  where
  toHandler : H → Handler (α := α) level

/-- An actual `Handler` is its own handler. -/
instance
    {α : Type}
    {level : SecurityLevel}
    : ToHandler (Handler (α := α) level) α level
  where
  toHandler := id

/-- A role-checked handler (what `requires` produces) becomes a `requiredRole`
    `Handler`, so callers can skip the `Handler.requiredRole "role"` wrapper. -/
instance {α : Type} {role : String}
    : ToHandler
        (ReaderT (UserWithRole role) (Except ApiError) α)
        α
        (.requiredRole role)
  where
  toHandler h := Handler.requiredRole role h

A class here is some sort of a contract, similar to an interface, but you can make instances of a class for certain types or even sub types without said types knowing about it, and the last instance does that, it applies only for required role handlers.

As a result, the actual type of our endpoint can be as simple as this:

abbrev Endpoint (α : Type) := Option User → Except ApiError α

The wiring of the endpoint itself doesn’t feel much simpler, but you will notice that there is no .utterDisaster anymore, everything is type-checked:

def endpoint
    {H : Type _}
    {α : Type}
    {level : SecurityLevel}
    [ToHandler H α level]
    (handler : H)
    : Endpoint α :=
  match ToHandler.toHandler handler with
  | Handler.everyone everyoneHandler => everyoneHandler
  | Handler.authenticated authHandler =>
    fun maybeUser =>
      match maybeUser with
      | some user => authHandler user
      | none => throw .unauthorized
  | Handler.requiredRole role roleHandler =>
    fun maybeUser =>
      match maybeUser with
      | some user =>
        if holds : HasRole user role
        -- The type constructor requires proof.
        then roleHandler ⟨user, holds⟩
        else throw <| ApiError.forbidden
          s!"User does not have required role: {role}"
      | none => throw .unauthorized

Now we drop a macro in there to make it look like a neat DSL:

/-- `requires "role" name (binders...) : RetType := body` expands to a `def`
  that returns `ReaderT (UserWithRole "role") (Except ApiError) RetType`,
  so the body can reach the role-checked user via `read`. -/
macro "requires"
    role:str
    name:ident
    binders:bracketedBinder*
    " : "
    ret:term
    " := "
    body:term
    : command =>
  `(def $name $binders*
      : ReaderT (UserWithRole $role) (Except ApiError) $ret :=
    $body)

Finally, the question as to whether we can fulfil the order:

requires
    "warehouse-management"
    canFulfil
    (wh : Warehouse)
    (r : WitdrawalRequest)
    : Bool := do
  match wh.inventory.get? r.itemId with
  | some stock => pure r.amount <= stock
  | none => throw .notFound

-- And the creation of the enpoint
def canFulfilEndpoint
    (wh : Warehouse)
    (r : WitdrawalRequest)
    : Endpoint Bool :=
  endpoint <| canFulfil wh r

You surely noticed that the user is not even part of the function parameters, and we don’t even have the error type in the signature, yet we can throw, that’s all strongly typed, and verified by the compiler.

But what if we wanted to access the user for some reason? Let’s say that our warehouse is in another planet and our company has an inclusive recruitment policy in terms of number of hands, and our users can only carry two items per hand, that’s where the ReaderT bit comes into play:

structure User where
  sub : String
  roles : HashSet String
  numberOfHands : Nat

inductive ApiError where
  | notFound : ApiError
  | unauthorized : ApiError
  | forbidden : String → ApiError
  -- Unapologetically punny, as always.
  | shorthanded: ApiError

requires
    "warehouse-management"
    canFulfil
    (wh : Warehouse)
    (r : WitdrawalRequest)
    : Bool := do
  match wh.inventory.get? r.itemId with
  | some stock =>
    if stock < r.amount
    then return false

    -- The ReaderT allows us to do this bit.
    -- The bit being discarded is the proof of being a
    -- warehouse manager.
    let ⟨user, _⟩ ← read
    -- The user can only carry two items per hand.
    if (user.numberOfHands * 2) < r.amount
    then throw .shorthanded
    else pure true
  | none => throw .notFound