UNQ PhD · supporting material

Capabilities in the type

The thesis needs a program's type to say which resources it may use: the network, files, the console. With that, an oracle can reject whatever was not granted while a language model writes the code. This page compares four ways of achieving it in Haskell, with the same problem in all of them: download a page and print its first line.

All the code on this page comes from the repository sawady/haskell-capabilities and compiles with GHC 9.12.2. The errors shown are the ones GHC gives.

Reading order

The sections follow the order in which the files are best read. Each one builds on the previous ones and needs, in addition, what is listed here:

Type classes, monads and monad transformers are explained in the Typeclassopedia and in the documentation of transformers and mtl. The extensions of section 4 are in the GHC User's Guide: GADTs, DataKinds, multi-parameter classes and overlapping instances.

The starting point: IO allows everything

In Haskell, the type IO () says that the function does input and output, but not which. This version, besides downloading the page, reads the process's environment variables, and its type does not change.

src/A_TypesOnly.hs Haskell 2010
summaryIO :: (Url -> IO String) -> Url -> IO ()
summaryIO fetch url = do
  page <- fetch url
  putStrLn (firstLine page)
  env <- getEnvironment
  putStrLn ("  (read " ++ show (length env) ++ " environment variables without permission)")
output runs
1. IO only:
<title of https://example.org>
  (read 2 environment variables without permission)

This is called ambient authority: the code can do anything the process can do, without anyone having granted it. The four approaches that follow try to remove it.

1. Types only: capabilities as arguments

The most direct way is to pass each capability as a value: a record with the functions that implement it. If the result is still IO, the type names the capabilities but does not enforce them. The important change is to make the monad abstract:

src/A_TypesOnly.hs Haskell 2010
data Net m = Net { httpGet :: Url -> m String }

data Console m = Console { printLine :: String -> m () }

summary :: Monad m => Net m -> Console m -> Url -> m ()
summary net console url = do
  page <- httpGet net url
  printLine console (firstLine page)

Since the function does not know what m is, it can only do what the records give it. This is plain Haskell 2010 and it already solves the safety problem. What it does not give is convenience: each capability is passed by hand in every call, and a function's type lists the records in a fixed order.

2. Tagless final: capabilities as type classes

Instead of passing records, each capability is a single-parameter type class. A function that needs the network asks for Net m, and the compiler finds the implementation.

src/Capabilities.hs Haskell 2010
class Monad m => Net m where
  httpGet :: Url -> m String

class Monad m => Console m where
  printLine :: String -> m ()

class Monad m => Files m where
  readTextFile :: FilePath -> m String
src/B_TaglessFinal.hs, no signatures on purpose Haskell 2010
summary url = do
  page <- httpGet url
  printLine (firstLine page)

-- | Also uses files: GHC infers @(Net m, Files m, Console m)@.
summaryWithFile url path = do
  page <- httpGet url
  note <- readTextFile path
  printLine (firstLine page ++ " / " ++ note)

Neither function has a signature, and GHC infers exactly the capabilities each one uses:

types inferred by GHC ghc -e ':t ...'
summary :: (Net m, Console m) => Url -> m ()
summaryWithFile
  :: (Net m, Files m, Console m) => Url -> FilePath -> m ()

This is what matters most to the thesis. The set of capabilities a fragment uses comes out of type inference, which is decidable in Haskell 2010. The oracle only has to compare that set with the grant.

The interpreter is a concrete monad with instances for some capabilities. Choosing the interpreter is choosing what is granted. There is one over IO and a pure one for testing, and the same program runs in both without changes.

What GHC rejects

must-fail/B_CapabilityNotGranted.hs: the signature grants network and console, the body reads a file does not compile
must-fail/B_CapabilityNotGranted.hs:12:13: error: [GHC-39999]
    • Could not deduce ‘Files m’ arising from a use of ‘readTextFile’
      from the context: (Net m, Console m)
must-fail/B_DirectIO.hs: with the abstract monad, IO cannot be used does not compile
must-fail/B_DirectIO.hs:13:3: error: [GHC-25897]
    • Couldn't match type ‘m’ with ‘IO’
      Expected: m ()
        Actual: IO ()
must-fail/B_InterpreterLacksCapability.hs: the interpreter does not grant files does not compile
must-fail/B_InterpreterLacksCapability.hs:35:16: error: [GHC-39999]
    • No instance for ‘Files App’

Exploring it in GHCi

What GHC infers can also be asked directly. From the root of the repository, ghci -isrc src/B_TaglessFinal.hs loads the example: :t shows a type, :info a class and its instances, and :r reloads the files after editing them. Functions written at the prompt get their capabilities inferred just as in the file:

GHCi session on src/B_TaglessFinal.hs ghci
ghci> :info Files
type Files :: (* -> *) -> Constraint
class Monad m => Files m where
  readTextFile :: FilePath -> m String
  {-# MINIMAL readTextFile #-}
  	-- Defined at src/Capabilities.hs:23:1
instance [safe] Files Test
  -- Defined at src/B_TaglessFinal.hs:71:10
ghci> runState (runTest (summary "https://example.org")) []
((),["test page for https://example.org"])
ghci> let quiet url = do { page <- httpGet url; return (firstLine page) }
ghci> :t quiet
quiet :: Net m => Url -> m String
ghci> let both url path = do { page <- httpGet url; note <- readTextFile path; printLine (page ++ note) }
ghci> :t both
both :: (Net m, Files m, Console m) => Url -> FilePath -> m ()

Only Test grants Files ([safe] is a Safe Haskell annotation and can be ignored here). quiet does not print, and Console disappears from its type. Things to try: write a function that also reads a file and look at its type; in the file, give summary a signature with fewer capabilities than it uses and reload.

Why classes and not just types?

Records over an abstract monad (section 1) already give the same safety. The difference is in who does the work:

Records of functionsType classes
Who passes the capabilitiesThe programmer, as arguments, in every callThe compiler, through instance resolution
Which capabilities a function usesThe ones it receives; they have to be declaredGHC infers them
How they combineA list of arguments, in orderA set of constraints, unordered
Two implementations at onceYes, by passing two different recordsOne per monad; for another, another interpreter
For a model that generates codeIt has to carry the records through the whole programIt writes the code directly; the capabilities are deduced

For the thesis, the decisive row is the second one. With classes, the set of capabilities of a half-written program comes out of inference. With records, the oracle would have to track which arguments are used, which is also possible but is work of its own.

3. Monad transformers

This is the line of work of the UNQ research group the thesis belongs to. Each layer of the stack provides a capability, and the type names the concrete stack, in a fixed order.

src/C1_Transformers.hs Haskell 2010
type App = ReaderT Config (StateT Int IO)

fetch :: Url -> App String
fetch url = do
  lift (modify (+ 1))                     -- StateT layer: one layer down
  return ("<title of " ++ url ++ ">\nrest")

summary :: String -> App ()
summary path = do
  cfg <- ask                               -- ReaderT layer: the top one
  page <- fetch (server cfg ++ path)
  n <- lift get
  lift (lift (putStrLn (firstLine page ++ " (request " ++ show n ++ ")")))
  -- IO is at the bottom of the stack: with lift (lift ...) any IO can be
  -- done. Transformers put the capabilities in order, but they do not
  -- remove the ambient authority of IO.

The example shows two things. Using an inner layer means lifting by hand with lift, as many times as there are layers above it. And since IO is at the bottom of the stack, lift (lift ...) reaches any IO operation: transformers put the capabilities in order, but they do not remove ambient authority.

The mtl style is tagless final

The mtl classes, such as MonadReader and MonadState, are exactly the idea of section 2: MonadReader Config m means "m can read a Config". The difference is that they have two parameters, so they require extensions.

src/C2_Mtl.hs + FlexibleContexts
summary :: (MonadReader Config m, MonadState Int m, Net m) => String -> m String
summary path = do
  cfg <- ask
  modify (+ 1)
  page <- httpGet (server cfg ++ path)
  n <- get
  return (firstLine page ++ " (request " ++ show n ++ ")")

A capability of our own, such as Net, lives alongside the mtl ones. For it to go through the stack it takes one instance per transformer, which is known as the n² instances problem:

src/C2_Mtl.hs + FlexibleContexts
instance Net m => Net (ReaderT r m) where
  httpGet = lift . httpGet

instance Net m => Net (StateT s m) where
  httpGet = lift . httpGet

The consequence for the thesis: there is no need to choose between tagless final and transformers. Programs are written with capabilities as classes, and interpreters are built with transformer stacks, as in this example. What has to be avoided is MonadIO, which gives back the full ambient authority.

4. Effect systems with rows

Here the computation carries a row in its type: the list of effects it may use. Eff es a is a computation that produces an a using the effects in es. The function below is polymorphic in the row: it works in any row that contains Net and Console. That is row polymorphism.

src/D_EffectRows.hs + FlexibleContexts
summary :: (Member Net es, Member Console es) => Url -> Eff es ()
summary url = do
  page <- httpGet url
  printLine (takeWhile (/= '\n') page)

Effects only declare operations. What they do is decided by a handler, which removes one effect from the row and interprets it. When the row is empty, the computation is pure.

src/Effects.hs + 7 extensions
data Net a where
  HttpGet :: Url -> Net String

data Console a where
  PrintLine :: String -> Console ()
src/Effects.hs: the Net handler + 7 extensions
handleNet :: (Url -> String) -> Eff (Net ': es) a -> Eff es a
handleNet _ (Pure a) = Pure a
handleNet pages (Request (Here (HttpGet url)) k) = handleNet pages (k (pages url))
handleNet pages (Request (There u) k) = Request u (handleNet pages . k)

The same program is run by applying the handlers in order. One interprets the console by collecting lines in a list, without IO. Another interprets it with real IO, which then has to be further down the row. Rejecting a capability that was not granted works just as with classes:

must-fail/D_EffectNotInRow.hs: the row only has Net, the body prints does not compile
must-fail/D_EffectNotInRow.hs:12:3: error: [GHC-39999]
    • Could not deduce ‘Member Console es’
        arising from a use of ‘printLine’
      from the context: Member Net es

In Haskell the row is a type-level list, which is why DataKinds, GADTs, TypeOperators and four other extensions are needed. A list has an order and can repeat elements, which a real row does not. Languages designed for this, such as Koka, write the row in the function's type, with a variable for "the rest of the effects", and treat it as a set. In Haskell, libraries such as effectful, polysemy and fused-effects provide it. The repository uses a minimal version, written by hand in about 120 lines, so that the mechanism can be seen without dependencies.

In GHCi, ghci -isrc src/D_EffectRows.hs shows how each handler removes one effect from the row. Applying them in the other order is a good way to check the explanation:

GHCi session on src/D_EffectRows.hs ghci
ghci> :t summary
summary :: (Member Net es, Member Console es) => Url -> Eff es ()
ghci> :t handleNet fakePages (summary "https://example.org")
handleNet fakePages (summary "https://example.org")
  :: Member Console es => Eff es ()
ghci> :t handleConsolePure (handleNet fakePages (summary "https://example.org"))
handleConsolePure (handleNet fakePages (summary "https://example.org"))
  :: Eff es ((), [String])
ghci> run (handleConsolePure (handleNet fakePages (summary "https://example.org")))
((),["<title of https://example.org>"])

The four, side by side

Records over mTagless finalTransformersmtl styleEffect rows
Where the capability isIn the argumentsIn the class constraintsIn the layers of the stackIn the class constraintsIn the row of Eff
Removes ambient authorityYesYesNo: IO is at the bottomYes, except with MonadIOYes, unless IO is in the row
GHC infers the set usedNoYesNo: the stack is declaredYesYes
Order mattersThat of the argumentsNoYesNot in the program; yes in the interpreter's stackYes, when applying the handlers
ExtensionsNoneNoneNoneFlexibleContextsSeven
Cost of using itCarrying arguments aroundOne instance per capability and interpreterlift by handn² instancesWriting handlers

What suits the thesis

  1. Write the programs in tagless final, with single-parameter classes. It is Haskell 2010 with no extensions, inference is decidable and GHC computes the set of capabilities of each fragment. That is what the oracle needs.
  2. Build the interpreters with transformers. It is the existing line of work of the UNQ research group and it fits without conflict, as the mtl example shows.
  3. Leave out of the subset everything that gives back ambient authority: IO in signatures, MonadIO and unsafePerformIO. Otherwise the capabilities can be bypassed.
  4. Use effect rows as a point of comparison in the theoretical framework. They are more expressive, because a handler can reinterpret an effect, but they require extensions and a more complex type system for the oracle.

One limitation to keep in mind: with classes, the capability is "use the network", not "use this URL". Restricting which resources are accessed would call for refinements or other mechanisms, and is outside this scope.

Exercises

The repository has five graded exercises, from section 1 to section 4: adding a capability as a record and as a class, predicting GHC’s errors with transformers and in the mtl style, running the mtl-style program without IO, and following the row through the handlers. The solutions are apart from the statements, and ./build.sh checks them like the examples.

References

A minimal bibliography, by section.

Ambient authority and capabilities

Tagless final (section 2)

Monad transformers and the mtl style (section 3)

Effect rows (section 4)