Wednesday, September 29, 2021

Fall-from-Grace: A ready-to-fork functional programming language

Fall-from-Grace: A ready-to-fork functional programming language

I’m publishing a repository containing a programming language implementation named Fall-from-Grace (or “Grace” for short). The goal of this language is to improve the quality of domain-specific languages by providing a useful starting point for implementers to fork and build upon.

You can visit the project repository if you want to cut to the chase. The README already provides most of the information that you will need to begin using the language. This announcement post focuses more upon the history and motivation behind this project. Specifically, I imagine some people will want to understand how this work relates to my work on Dhall.

TL;DR: I created a functional language that is a superset of JSON, sort of like Jsonnet but with types and bidirectional type inference.

The motivation

The original motivation for this project was very different than the goal I finally settled upon. My original goal was to build a type checker with type inference for Nix, since this is something that a lot of people wanted (myself included). However, I bit off more than I could chew because Nix permits all sorts of stuff that is difficult to type-check (like computed record fields or the callPackages idiom in Nixpkgs).

I lost steam on my Nix type-checker (for now) but then I realized that I had still built a fairly sophisticated interpreter implementation along the way that other people might find useful. In particular, this was my first new interpreter project in years since I created Dhall, and I had learned quite a few lessons from Dhall about interpreter best practices.

“So”, I thought, “why not publish what I had created so far?”

Well, I can think of one very good reason why not: I want to continue to support and improve upon Dhall because people are using Dhall in production and I have neither the time nor the inclination to build yet another ecosystem around a new programming language. But somebody else might!

So I took the project in a totally different direction: publish an instructive implementation of a programming language that others could fork and build upon.

Unlike Dhall, this new language would not be encumbered by the need to support a language standard or multiple independent implementations, so I could go nuts with adding features that I omitted from Dhall. Also, this language would not be published in any way so that I could keep the implementation clear, opinionated, and maintainable. In other words, this language would be like an “executable tutorial”.

The starting point

I designed the initial feature set of this new language based on feedback I had received from Dhall’s skeptics. The rough language these people had in mind went something like this:

  • The language had to have bidirectional type inference

    The most common criticism I received about Dhall was about Dhall’s limited type inference.

  • The language had to have JSON-compatible syntax

    One of the things that had prevented people from using Dhall was that the migration story was not as smooth as, say, CUE (which is a superset of YAML) or Jsonnet (which is a superset of JSON), because Dhall was not a superset of any existing file format.

    Also, many people indicated that JSON syntax would be easier for beginners to pick up, since they would likely be comfortable with JSON if they had prior experience working with JavaScript or Python.

  • The language had to have JSON-compatible types

    JSON permits all sorts of silliness (like [ 1, [] ]), and people wanted a type system that can cope with that stuff, while still getting most of the benefits of working with types. Basically, they wanted something sort of like TypeScript’s type system.

  • They don’t want to run arbitrary code

    TypeScript already checks off most of the above points, but these people were looking for alternatives because they didn’t want to permit users to run arbitrary JavaScript. In other words, they don’t want a language that is “Pac-Man complete” and instead want something more limited as a clean slate for building their own domain-specific languages.

What I actually built

I created the Fall-from-Grace language, which is my best attempt to approximate the Dhall alternative that most people were looking for.

Fall-from-Grace has:

  • JSON-compatible syntax

  • Bidirectional type-inference and type-checking

  • A JSON-compatible type system

  • Dhall-style filepath and URL imports

  • Fast interpretation

  • Open records and open unions

    a.k.a. row polymorphism and polymorphic variants

  • Universal quantification and existential quantification

    a.k.a. “generics” and “typed holes”

One way to think of Grace is like “Dhall but with better type inference and JSON syntax”. For example, here is the Grace equivalent of the tutorial example from dhall-lang.org:

# ./users.ffg
let makeUser = \user ->
      let home       = "/home/" + user
      let privateKey = home + "/.ssh/id_ed25519"
      let publicKey  = privateKey + ".pub"

      in  { home: home, privateKey: privateKey, publicKey: publicKey }

in  [ makeUser "bill"
    , makeUser "jane"
    ]

… which produces this result:

$ grace interpret ./users.ffg
[ { "home": "/home/bill"
  , "privateKey": "/home/bill/.ssh/id_ed25519"
  , "publicKey": "/home/bill/.ssh/id_ed25519.pub"
  }
, { "home": "/home/jane"
  , "privateKey": "/home/jane/.ssh/id_ed25519"
  , "publicKey": "/home/jane/.ssh/id_ed25519.pub"
  }
]

Just like Dhall, Grace supports let expressions and anonymous functions for simplifying repetitive expressions. However, there are two differences here compared to Dhall:

  • Grace uses JSON-like syntax for records (i.e. : instead of = to separate key-value pairs)

    Because Grace is a superset of JSON you don’t need a separate grace-to-json tool like Dhall. The result of interpreting Grace code is already valid JSON.

  • Grace has better type inference and doesn’t require annotating the type of the user function argument

    The interpreter can work backwards to infer that the user function argument must have type Text based on how user is used.

Another way to think of Grace is as “Jsonnet + types + type inference”. Grace and Jsonnet are both programmable configuration languages and they’re both supersets of JSON, but Grace has a type system whereas Jsonnet does not.

The following example Grace code illustrates this by fetching all post titles from the Haskell subreddit:

# ./reddit-haskell.ffg
let input
      = https://www.reddit.com/r/haskell.json
      : { data: { children: List { data: { title: Text, ? }, ? }, ? }, ? }

in  List/map (\child -> child.data.title) input.data.children

… which at the time of this writing produces the following result:

$ grace interpret ./reddit-haskell.ffg
[ "Monthly Hask Anything (September 2021)"
, "Big problems at the timezone database"
, "How can Haskell programmers tolerate Space Leaks?"
, "async graph traversal in haskell"
, "[ANN] Call For Volunteers: Join The New \"Our Foundation Task Force\""
, "Math lesson to be learned here?"
, "In search a functional job"
, "Integer coordinate from String"
, "New to Haskell"
, "Variable not in scope error"
, "HF Technical Track Elections - Announcements"
, "Learning Haskell by building a static blog generator"
, "Haskell Foundation Board meeting minutes 2021-09-23"
, "Haskell extension 1.7.0 VS Code crashing"
, "[question] Nix/Obelisk with cabal packages intended for hackage"
, "George Wilson - Cultivating an Engineering Dialect (YOW! Lambda Jam 2021)"
, "A new programming game, Swarm by Brent Yorgey"
, "Scheme in 48 hours, First chapter issue"
, "Recursively delete JSON keys"
, "Issue 282 :: Haskell Weekly newsletter"
, "Haskell"
, "Yaml parsing with preserved line numbers"
, "I would like some input on my code if anybody have time. I recently discovered that i can use variables in Haskell (thought one could not use them for some reason). Would just like some input on how i have done it."
, "Diehl's comments on Haskell numbers confuse..."
, "Please explain this syntax"
, "Can Haskell automatically fuse folds?"
]

Here we can see:

  • Dhall-style URL imports

    We can import JSON (or any Grace code) from a URL just by pasting the URL into our code

  • Any JSON expression (like haskell.json) is also a valid Grace expression that we can transform

  • We can give a partial type signature with holes (i.e. ?) specifying which parts we care about and which parts to ignore

Grace’s type system is even more sophisticated than that example lets on. For example, if you ask grace for the type of this anonymous function from the example:

\child -> child.data.title

… then the interpreter will infer the most general type possible without any assistance from the programmer:

forall (a : Type) .
forall (b : Fields) .
forall (c : Fields) .
  { data: { title: a, b }, c } -> a

This is an example of row-polymorphism (what Grace calls “open records”).

Grace also supports polymorphic variants (what Grace calls “open unions”), so you can wrap values of different types in constructors without having to declare any union type in advance:

[ GitHub
    { repository: "https://github.com/Gabriel439/Haskell-Turtle-Library.git"
    , revision: "ae5edf227b515b34c1cb6c89d9c58ea0eece12d5"
    }
, Local { path: "~/proj/optparse-applicative" }
, Local { path: "~/proj/discrimination" }
, Hackage { package: "lens", version: "4.15.4" }
, GitHub
    { repository: "https://github.com/haskell/text.git"
    , revision: "ccbfabedea1cf5b38ff19f37549feaf01225e537"
    }
, Local { path: "~/proj/servant-swagger" }
, Hackage { package: "aeson", version: "1.2.3.0" }
]

… and the interpreter automatically infers the most general type for that, too:

forall (a : Alternatives) .
  List
    < GitHub: { repository: Text, revision: Text }
    | Local: { path: Text }
    | Hackage: { package: Text, version: Text }
    | a
    >

Open records + opens unions + type inference mean that the language does not require any data declarations to process input. The interpreter infers the shape of the data from how the data is used.

Conclusion

If you want to learn more about Grace then you should check out the README, which goes into more detail about the language features, and also includes a brief tutorial.

I also want to conclude by briefly mentioning some other secondary motivations for this project:

  • I want to cement Haskell’s status as the language of choice for implementing interpreters

    I gave a longer talk on this subject where I argue that Haskell can go mainstream by cornering the “market” for interpreted languages:

  • I hope to promote certain Haskell best practices for implementing interpreters

    Grace provides a model project for implementing an interpreted language in Haskell, including project organization, choice of dependencies, and choice of algorithms. Even if people choose to not fork Grace I hope that this project will provide some useful opinionated decisions to help get them going.

  • I mentor several people learning programming language theory and I wanted instructive example code to reference when teaching them

    One of the hardest parts about teaching programming language theory is that it’s hard to explain how to combine language features from more than one paper. Grace provides the complete picture by showing how to mix together multiple advanced features.

  • I wanted to prototype a few language features for Dhall’s language standard

    For example, I wanted to see how realistic it would be to standardize bidirectional type-checking for Dhall. I may write a follow-up post on what I learned regarding that.

  • I also wanted to prototype a few implementation techniques for the Haskell implementation of Dhall

    The Haskell implementation of Dhall is complicated enough that it’s hard to test drive some implementation improvements I had in mind, but Grace was small enough that I could learn and iterate on some ideas more quickly.

I don’t plan on building an ecosystem around Grace, although anybody who is interested in doing so can freely fork the language. Now that Grace is complete I plan on using what I learned from Grace to continue improving Dhall.

I also don’t plan on publishing Grace as a package to Hackage nor do I plan to provide an API for customizing the language behavior (other than forking the language). I view the project as an educational resource and not a package that people should depend on directly, because I don’t commit to supporting this project in production.

I do believe Grace can be forked to create a “Dhall 2.0”, but if that happens such an effort will need to be led by somebody else other than me. The main reason why is that I’d rather preserve Grace as a teaching tool and I don’t have the time to productionize Grace (productionizing Dhall was already a big lift for me).

However, I still might fork Grace in the future for other reasons (including a second attempt at implementing a type-checker for Nix).

Thursday, September 9, 2021

Optics are monoids

lens-trick

This post documents my favorite lens trick of all time. Also, this trick works for any optics package based on van Laarhoven lenses, like lens-family-core or microlens.

This post assumes some familiarity with lenses, so if you are new to lenses then you might want to first read:

The title is slightly misleading and the precise statement is that Folds are Monoids, and all of the following optics are subtypes of Folds:

  • Getter
  • Lens
  • Traversal
  • Prism
  • Iso

… but I couldn’t fit that all of that in the title.

That means that if you combine any of the above optic types using <>, you will get a new optic that can be used as a Fold that combines their targets. For example:

>>> toListOf _1 (True, False)          -- _1 is a Lens
[True]
>>> toListOf _2 (True, False)          -- _2 is a Lens
[False]
>>> toListOf (_1 <> _2) (True, False)  -- (_1 <> 2) is a Fold
[True,False]

Also, mempty is the “empty” Fold that targets nothing:

>>> toListOf mempty (True, False)
[]

There’s more to this trick, though, and we can build upon this idea to create optics that traverse complex data structures in a single pass.

Realistic example

To illustrate the trick, I’ll use a realistic example inspired by one of my interpreter side projects. I’ll keep things simple by reducing the original example to the following syntax tree for a toy lambda calculus implementation:

data Syntax
    = Variable String
    | Lambda String Syntax
    | Apply Syntax Syntax
    | Let String Syntax Syntax

example :: Syntax
example = Lambda "x" (Lambda "y" (Apply (Variable "x") (Variable "y")))

Now suppose we’d like to write a function that verifies that our syntax tree has no empty variable names. Without optics, we could write something like this:

wellFormed :: Syntax -> Bool
wellFormed (Variable name) =
    not (null name)
wellFormed (Lambda name body) =
    not (null name) && wellFormed body
wellFormed (Apply function argument) =
    wellFormed function && wellFormed argument
wellFormed (Let name assignment body) =
    not (null name) && wellFormed assignment && wellFormed body

… which works as expected on a few smoke tests:

>>> wellFormed example
True
>>> wellFormed (Variable "")
False

This implementation is simple enough for now. However, real interpreters tend to add a whole bunch of other constructors to the syntax tree. For example, each new keyword or datatype we add to the language will add another constructor to the syntax tree and each new constructor increases the boilerplate code for functions like wellFormed.

Thankfully, the lens and generic-lens packages provide useful utilities that simplify recursive functions like wellFormed. All we have to do is derive Plated and Generic for our Syntax type, like this:

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}

module Example where

import Data.Generics.Product (the)
import Data.Generics.Sum (_As)
import GHC.Generics (Generic)

import Control.Lens
import Data.Data (Data)

data Syntax
    = Variable String
    | Lambda String Syntax
    | Apply Syntax Syntax
    | Let String Syntax Syntax
    deriving (Data, Generic, Show)

instance Plated Syntax

example :: Syntax
example = Lambda "x" (Lambda "y" (Apply (Variable "x") (Variable "y")))

Once we derive Plated we can use the cosmos lens to zoom in on all sub-expressions:

>>> toListOf cosmos example
[ Lambda "x" (Lambda "y" (Apply (Variable "x") (Variable "y")))
, Lambda "y" (Apply (Variable "x") (Variable "y"))
, Apply (Variable "x") (Variable "y")
, Variable "x"
, Variable "y"
]

… and when we derive Generic we can further narrow down the results using _As and the from the generic-lens package:

>>> :set -XTypeApplications
>>> :set -XDataKinds
>>> toListOf (cosmos . _As @"Variable") example  -- Get all Variable names
["x","y"]

>>> toListOf (cosmos . _As @"Lambda" . the @1) example  -- Get all Lambda names
["x","y"]

>>> toListOf (cosmos . _As @"Let" . the @1) example  -- Get all Let names
[]

So we can combine these tricks to implement our wellFormed function using optics to handle the automatic tree traversal:

wellFormed :: Syntax -> Bool
wellFormed syntax =
        hasn't (cosmos . _As @"Variable" . only "") syntax
    &&  hasn't (cosmos . _As @"Lambda" . the @1 . only "") syntax
    &&  hasn't (cosmos . _As @"Let" . the @1 . only "") syntax

… but we’re not done here!

The cosmos Traversal factored away some of the repetition because we no longer need to recursively descend into subexpressions any longer. We also no longer need to explicitly handle constructors that have no variable names, like Apply.

Our wellFormed function is still repetitive, though, because three times in a row we write:

hasn't (cosmos .. only "") syntax

… and we’d like to factor out this repetition.

Our first instinct might be to factor out the repetition with a helper function, like this:

wellFormed :: Syntax -> Bool
wellFormed syntax =
        noEmptyVariables (_As @"Variable")
    &&  noEmptyVariables (_As @"Lambda" . the @1) 
    &&  noEmptyVariables (_As @"Let" . the @1)
  where
    noEmptyVariables fold =
        hasn't (cosmos . fold . only "") syntax

… and that does work, but there is actually a better way. We can instead use the fact that Traversals are also Folds and Folds are Monoids to write this:

wellFormed :: Syntax -> Bool
wellFormed syntax =
    hasn't
        ( cosmos
        . (   _As @"Variable"
          <>  _As @"Lambda" . the @1
          <>  _As @"Let" . the @1
          )
        . only ""
        )
        syntax

In other words, we can take the following three Traversals that each focus on a different source of variable names:

  • _As @"Variable" - Focus in on variable names
  • _As @"Lambda" . the @1 - Focus in on Lambda-bound variables
  • _As @"Let" . the @1 - Focus in on Let-bound variables

… and when we combine them using <> we get a Fold that focuses on all possible sources of variable names. We can then chain this composite Fold in between cosmos and only to find all of the empty variable names.

In fact, we’re not limited to using <>. Any utility that works on Monoids will work, like mconcat, so we can refactor our code even further like this:

wellFormed :: Syntax -> Bool
wellFormed = hasn't (cosmos . names . only "")

-- | Get all variable names within the current constructor
names :: Monoid m => Getting m Syntax String
names =
    mconcat
        [ _As @"Variable"
        , _As @"Lambda" . the @1
        , _As @"Let" . the @1
        ]   

Now we have factored out a useful and reusable names Fold1 that we can combine with cosmos to get all names within our syntax tree:

>>> toListOf (cosmos . names) example
["x","y","x","y"]

This means that any new contributor to our interpreter can register a new source of variable names by adding a Traversal to that list and all downstream functions that use names will automatically update to do the right thing.

Why this trick?

I briefly touched on some other cool tricks in the course of this post, including:

  • The use of Plated for simplifying recursive Traversals
  • The use of generic-lens for boilerplate-free optics

… so why do I consider “optics as monoids” to be the coolest trick of them all? After all, Plated and generic-lens did most of the heavy lifting in the above example.

The reason why I particularly love the Monoid instance for lenses is because (as far as I know) nobody ever designed lenses to do this; this is purely an emergent property of independent design choices spread out over time.

This shouldn’t surprise us too much, because Haskell’s mathematically inspired type classes sort of follow the Unix philosophy to Do one thing and do it well. If each piece does one small thing correctly, then if you combine multiple pieces then the composite result is correct by construction.

However, you don’t need to take my word for it. I’ll walk through in detail how this works, first at the type level and then at the term level.

Type level

The first piece of the puzzle is the following Semigroup and Monoid instances for functions in base:

instance Semigroup b => Semigroup (a -> b) where
    (f <> g) x = f x <> g x

instance Monoid b => Monoid (a -> b) where
    mempty x = mempty

These instances says that a function is a Monoid if the function’s result is also a Monoid. We combine two functions by combining their outputs (when given the same input) and the empty function ignores its input and produces an empty output.

The second piece of the puzzle is the Const type (the constant Functor), which has a Semigroup and Monoid instance, too:

newtype Const a b = Const { getConst :: a }

instance Monoid a => Monoid (Const a b) where
    mempty = Const mempty

instance Semigroup a => Semigroup (Const a b) where
    Const x <> Const y = Const (x <> y)

These instances are so simple that we could have just derived them (and indeed, that is what the base package does):

newtype Const a b = Const { getConst :: a }
    deriving newtype (Semigroup, Monoid)

In other words, Const a b is a Monoid if a is a Monoid. Combining two Consts combines their stored value, and the empty Const stores an empty value.

The final piece of the puzzle is that a Fold from the lens package is just a higher-order function over Consts:

-- This not the real type, but it's equivalent
type Fold a b = forall m . Monoid m => (b -> Const m b) -> (a -> Const m a)

… and that type is a valid Monoid, because:

  • (b -> Const m b) -> (a -> Const m a) is a Monoid if (a -> Const m a) is a Monoid

    … according to the Monoid instance for functions

  • a -> Const m a is a Monoid if Const m a is a Monoid

    … also according to the Monoid instance for functions

  • Const m a is a Monoid if m is a Monoid

    … according to the Monoid instance for Const

  • m is a Monoid

    … according to the Monoid m => constraint in the type of Fold

Therefore, all Folds are Monoids.

Term level

However, knowing that a Fold type-checks as a Monoid is not enough. We want to build an intuition for what happens when we use Monoid operations on Folds.

The most compact way we can state our intuition is by the following two laws:

toListOf (l <> r) a = toListOf l a <> toListOf r a

toListOf mempty a = mempty

In other words, if you combine two Folds then you combine their “targets”, and the empty Fold has no targets.

These laws are also known as “monoid morphism laws”. In other words, toListOf is a function that transforms one type of Monoid (Folds) into another type of Monoid (lists).

We can verify those two laws using equational reasoning, but in order to do so we need to use the following simplified definition for toListOf:

{-# LANGUAGE RankNTypes #-}

import Data.Functor.Const (Const(..))

toListOf :: Fold a b -> a -> [b]
toListOf fold a = getConst (fold (\b -> Const [b]) a)

The real toListOf function from the lens package has a different, but equivalent, implementation. The real implementation is more efficient, but takes more steps when proving things using equational reasoning, so I prefer to use this simpler implementation.

Now let’s prove the two monoid morphism laws. The proof for the first law is:

toListOf (l <> r) a

-- Substitute `toListOf` with its definition
= getConst ((l <> r) (\b -> Const [b]) a)

-- If `l` and `r` are functions, then according to the `Semigroup` instance for
-- functions:
--
--     (f <> g) x = f x <> g x
--
-- … where in this case:
--
--     f = l
--     g = r
--     x = \b -> Const [b]
= getConst ((l (\b -> Const [b]) <> r (\b -> Const [b])) a)

-- Use the `Semigroup` instance for functions again, except this time:
--
--     f = l (\b -> Const [b])
--     g = r (\b -> Const [b])
--     x = a
= getConst (l (\b -> Const [b]) a <> r (\b -> Const [b]) a)

-- Now use the `Semigroup` instance for `Const`, which (essentially) says:
--
--     getConst (x <> y) = getConst x <> getConst y
--
-- … where:
--
--     x = l (\b -> Const [b]) a
--     y = r (\b -> Const [b]) a
= getConst (l (\b -> Const [b]) a) <> getConst (r (\b -> Const [b]) a)

-- Now apply the definition of `toListOf`, but in reverse:
= toListOf l a <> toListOf r a

… and the proof for the second law is:

toList mempty a

-- Substitute `toListOf` with its definition
= getConst (mempty (\b -> Const [b]) a)

-- If `mempty` is a function, then according to the `Monoid` instance for
-- functions:
--
--     mempty x = mempty
--
-- … where in this case:
--
--     x = \b -> Const [b]
= getConst (mempty a)

-- Use the `Monoid` instance for functions again, except this time:
--
--     x = a
= getConst mempty

-- Now use the `Monoid` instance for `Const`, which says:
--
--    mempty = Const mempty
= getConst (Const mempty)

-- getConst (Const x) = x
= mempty

Conclusion

Hopefully that gives you a taste for how slick and elegant Haskell’s lens package is. If you like this post, you might also like these other posts:

Also, I know that I skimmed through the subjects of Plated and generic-lens, which are interesting topics in their own right. I hope to cover those in more detail in future posts.

I don’t know if this trick can be made to work for optics (an alternative to lens that uses an abstract interface to improve error messages). I know that it does not work at the time of this writing, but perhaps a Monoid instance could be added for the Optic type? I also have no idea if this trick or a related trick works for profunctor-optics (a different formulation of lenses based on profunctors).

I haven’t benchmarked whether combining Folds is faster than doing separate passes over the same data structure. I believe it’s more lazy, though, to process the data structure in a single pass using a composite Fold.

Appendix

Here is the complete code example if you want to test this out locally:

{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE TypeApplications   #-}

module Example where

import Data.Generics.Product (the)
import Data.Generics.Sum (_As)
import GHC.Generics (Generic)

import Control.Lens
import Data.Data (Data)

data Syntax
    = Variable String
    | Lambda String Syntax
    | Apply Syntax Syntax
    | Let String Syntax Syntax
    deriving (Data, Generic, Show)

instance Plated Syntax

example :: Syntax
example = Lambda "x" (Lambda "y" (Apply (Variable "x") (Variable "y")))

wellFormed :: Syntax -> Bool
wellFormed = hasn't (cosmos . names . only "")

names :: Monoid m => Getting m Syntax String
names =
    mconcat
        [ _As @"Variable"
        , _As @"Lambda" . the @1
        , _As @"Let" . the @1
        ]

  1. The type of names is morally Fold Syntax String, which according to the lens documentation is the essentially same type, but only the Getting version of the type will type-check here.↩︎

Wednesday, September 1, 2021

Forward and reverse proxies explained

proxy

This post explains what is the difference between a forward proxy and a reverse proxy. This post will likely be most useful for:

  • engineers designing on-premises enterprise software to forward traffic in restrictive networking environments

  • authors of forward and reverse proxy packages / frameworks

  • people who want to learn more about networking in general

I’m writing this mainly because I had to puzzle through all of this when I was designing part of our product’s network architecture at work and I frequently explain what I learned to my coworkers. Most of the existing explanations of proxies were not helpful to me when I learned this for the first time, so I figured I would try to explain things in my own words so that I can reference this post when teaching others.

This post will not touch upon the use cases for forward and reverse proxies and instead will mostly focus on the architectural differences between them. If you are interested in learning more about how they are used in practice then I recommend reading the Wikipedia article on proxies:

Also, this post assumes some familiarity with the HTTP and HTTPS protocols.

The difference

The simplest difference between the two types of proxies is that:

  • A reverse proxy is a proxy where the proxy selects the origin server
  • A forward proxy is a proxy where the client selects the origin server

… and “origin server” means the server where the HTTP resource originates from that the proxy forwards the HTTP request to.

There are a few alternative definitions for forward proxy and reverse proxy, but in my experience the above definitions promote the correct intuition.

curl examples

I sometimes explain the difference between forward and reverse proxies in terms of curl commands.

For example, if I host a reverse proxy at reverse.example.com that forwards requests to google.com, then a sample HTTP request going through the reverse proxy might look like the following curl command:

$ curl https://reverse.example.com

In a reverse proxy, the client (e.g. curl) does not select the origin server (e.g. google.com). In this particular example the origin server is hard-coded into the reverse proxy and there would be no way for the client to specify that the HTTP request should be forwarded to github.com instead.

The data flow for such a request looks something like this:

┌──────────────────────────────────┐
│                                  │
│            google.com            │
│                                  │
└──────────────────────────────────┘
         ↑                ↓
 "GET / HTTP/1.1" "HTTP/1.1 200 OK"
         ↑                ↓
┌──────────────────────────────────┐
│                                  │
│        reverse.example.com       │
│                                  │
└──────────────────────────────────┘
         ↑                ↓
 "GET / HTTP/1.1" "HTTP/1.1 200 OK"
         ↑                ↓
┌──────────────────────────────────┐
│                                  │
│               curl               │
│                                  │
└──────────────────────────────────┘

In other words:

  • The client (e.g. curl) sends an HTTP request to the reverse proxy
  • The proxy (e.g. reverse.example.com) forwards the HTTP request to the origin server
  • The origin server (e.g. google.com) responds to the HTTP request
  • The proxy forwards the HTTP response back to the client

Now suppose that I host a forward proxy at forward.example.com. A sample HTTP request destined for google.com going through the forward proxy might look like this:

$ curl --proxy https://forward.example.com https://google.com

In a forward proxy, the client (e.g. curl) selects the origin server (e.g. google.com) and could have potentially selected a different origin server, such as github.com, like this:

$ curl --proxy https://forward.example.com https://github.com

… and then the forward proxy would forward the request to github.com instead1.

The data flow for a request going through a forward proxy depends on whether the client connects to the origin server using HTTP or HTTPS.

If the client uses HTTP then the data flow for a forward proxy typically looks like this:

┌──────────────────────────────────────────────────┐
│                                                  │
│                    google.com                    │
│                                                  │
└──────────────────────────────────────────────────┘
                ↑                         ↓
        "GET / HTTP/1.1"          "HTTP/1.1 200 OK"
                ↑                         ↓
┌──────────────────────────────────────────────────┐
│                                                  │
│                forward.example.com               │
│                                                  │
└──────────────────────────────────────────────────┘
                ↑                         ↓
 "GET http://google.com HTTP/1.1" "HTTP/1.1 200 OK"
                ↑                         ↓
┌──────────────────────────────────────────────────┐
│                                                  │
│                       curl                       │
│                                                  │
└──────────────────────────────────────────────────┘

In other words:

  • The client (e.g. curl) sends an HTTP request to the proxy with the origin server in the request line
  • The proxy (e.g. forward.example.com) forwards the request to the origin server specified on the request line
  • The origin server (e.g. google.com) responds to the HTTP request
  • The proxy forwards the HTTP response back to the client

The main difference from the previous example is the HTTP request line that curl sends to forward.example.com. Forward proxies receive an absolute URI from the client (e.g. http://google.com) instead of a relative URI (like /). This is how the forward proxy knows where to forward the client’s request.

Now contrast that with the data flow for a forward proxy when the client uses HTTPS:

                             ┌────────────┐
                             │            │
                             │ google.com │
                             │            │
                             └────────────┘
                                    ↑
                                   TCP
                                    │
┌───────────────────────────────────│─┐
│                                   │ │
│          forward.example.com      │ │
│                                   │ │
└───────────────────────────────────│─┘
                ↑                   │
 "CONNECT google.com:443 HTTP/1.1" TCP
                ↑                   ↓
┌─────────────────────────────────────┐
│                                     │
│                curl                 │
│                                     │
└─────────────────────────────────────┘

This is a different flow of information:

  • The client (e.g. curl) sends a CONNECT request to the proxy
  • The proxy (e.g. forward.example.com) opens a TCP connection to the origin server (e.g. google.com)
  • The proxy forwards the rest of the client’s connection as raw TCP traffic directly to the origin server
    • This TCP connection is encrypted, so by default the proxy cannot intercept or modify HTTPS traffic

However, despite the difference in data flow both HTTP forward proxies and HTTPS forward proxies let the client select the origin server. This is why we still call them both forward proxies even though they are architecturally different server types.

nc examples

If you’re curious, you can verify the difference in curl’s behavior when using HTTP vs HTTPS forward proxies on the command line. If you set up nc to listen on port 8000:

$ nc -l 8000

… and then ask curl to use localhost:8000 as a forward proxy, you’ll see different results depending on whether the origin server URI uses an HTTP or HTTPS scheme. For example, if you run:

$ curl --proxy http://localhost:8000 --data 'A secret!' http://example.com

… then nc will print the following incoming request from curl:

$ nc -l 8000
POST http://example.com/ HTTP/1.1
Host: example.com
User-Agent: curl/7.64.1
Accept: */*
Proxy-Connection: Keep-Alive
Content-Length: 9
Content-Type: application/x-www-form-urlencoded

A secret!

Note that the request line has an absolute URI specifying the origin server to connect to. Also, the HTTP forward proxy has complete access to the contents of the request (including the headers and payload) and can tamper with them before sending the request further upstream.

Contrast that with an HTTPS request that goes through a forward proxy:

$ curl --proxy http://localhost:8000 --data 'A secret!' https://example.com

… where now nc will print an incoming request that looks like this:

$ nc -l 8000
CONNECT example.com:443 HTTP/1.1
Host: example.com:443
User-Agent: curl/7.64.1
Proxy-Connection: Keep-Alive

This time the HTTP method is CONNECT (regardless of what the original method was) and the client only divulges enough information to the proxy to establish the TCP tunnel to example.com.

Blurring the line

Sometimes people configure reverse proxies to behave like a “poor person’s forward proxy”. For example, you could imagine a reverse proxy configured to select the origin server based on the value of an HTTP header:

$ curl --header 'Origin: google.com' https://reverse.example.com

… or based on the URI:

$ curl https://reverse.example.com/?url=google.com

… or based on a subdomain (one per supported origin server):

$ # Yes, I have actually seen this in the wild
$ curl https://google.reverse.example.com

This sort of thing is possible, and there are some constrained use cases for doing things this way, but you should err on the side of using a forward proxy if you intend to let the client select the origin server. Forward proxy software (like squid) will better support this use case than reverse proxy software (like haproxy) and HTTP clients (like your browser or curl) will also better support forward proxies for this use case.

Example pseudocode

To further clarify the difference, here is some example pseudocode for how one would implement the various types of proxies.

The request handler for a hand-written reverse proxy might look something like the following Python pseudocode:

def handleRequest(request):
    # Forward the incoming request further upstream to some predefined origin
    # server (e.g. google.com), typically with some changes to the HTTP headers
    # that we won't cover in this post.
    response = httpRequest(
        host = "https://google.com",
        method = request.method,
        headers = fixRequestHeaders(request.headers),
        path = request.path,
        query = request.query,
        body = request.body
    )

    # Now forward the origin server's response back to the client
    respond(
        headers = fixResponseHeaders(response.headers),
        statusCode = response.statusCode,
        body = response.body
    )

The request handler for an HTTP forward proxy would look something like this:

def handleRequest(request):
    # A request to an HTTP forward proxy has a request line with an absolute
    # URI:
    #
    #     ${METHOD} ${SCHEME}://${HOST}${PATH} HTTP/1.1
    #
    # … which is how the proxy knows where to forward the request further
    # upstream.
    upstreamURI = request.absoluteURI

    if upstreamURI is not None:
        # Other than obtaining the origin server from the request line, the rest
        # is similar to a reverse proxy.
        response = httpRequest(
            host = upstreamURI.host,
            method = request.method,
            headers = fixRequestHeaders(request.headers),
            path = upstreamURI.path,
            query = upstreamURI.query,
            body = request.body,
        )

        respond(
            headers = fixResponseHeaders(response.headers),
            statusCode = response.statusCode,
            body = response.body
        )
    else:
        respond(
            statusCode = 400,
            body = "The request line did not have an absolute URI",
        )

On the other hand, a HTTPS forward proxy would look something like this:

def handleRequest(request):
    # A request to an HTTPS forward proxy has a request line of the form:
    #
    #     CONNECT ${HOST}:${PORT} HTTP/1.1
    if request.connect is not None:
       forwardTcp(
           host = request.connect.host,
           port = request.connect.port,
           socket = request.socket
       )
    else:
        respond(
            statusCode = 400,
            body = "The HTTP method was not CONNECT"
        )

Combining a forward and reverse proxy

This section illustrates a scenario where you might combine a forward proxy and a reverse proxy to further reinforce the difference between the two.

Suppose that we wish to create a forward proxy reachable at https://both.example.com using squid. The problem is that squid does not provide out-of-the-box support for listening to HTTPS connections to squid itself.

Carefully note that squid can easily forward an HTTPS connection (using a CONNECT tunnel, as explained above), but squid does not support encrypting the client’s initial HTTP request to squid itself requesting the establishment of the CONNECT tunnel.

However, we can run a reverse proxy that can handle TLS termination (such as haproxy) listening on https://both.example.com. The reverse proxy’s sole job is to accept encrypted HTTPS requests sent to https://both.example.com and then forward the decrypted HTTP request to the squid service running on the same machine. squid then forwards the request further depending on the origin server specified in the HTTP request line.

In this scenario, squid is still acting as a forward proxy, in the sense that squid uses the HTTP request line provided by the client to determine where to forward the request. Vice versa, haproxy is acting as a reverse proxy because haproxy always forwards all incoming requests to squid regardless of what the client specifies.

This scenario illustrates one reason why I don’t define forward or reverse proxies in terms of which network or machine the proxy runs on. In this example, both the forward proxy and reverse proxy are running on the same network and machine.

There are other types of proxies that this post didn’t cover, but if you want to learn more you should also check out:

  • Transparent proxies

    These are proxies where the client doesn’t specify the proxy at all because it intercepts all client traffic. I personally view transparent proxies as a third type of forward proxy (the client still selects the origin server), although transparent proxies are architecturally very different from non-transparent forward proxies.

  • SSL Forward Proxy

    This is a variation on a forward proxy that can decrypt HTTPS traffic. However, this requires the client to opt into this decryption in some way.


  1. Some forward proxies do not forward all HTTP requests. Instead, a forward proxy might specify which hostnames, protocols, and ports to permit in an access control list. This means that the example from the text would only work if the forward proxy’s access control lists permitted requests to google.com and github.com.↩︎