(This is a continuation from Part I, a philosophical exploration about programming, with sandwiches. Go read it first, if you haven’t yet.)

In Part I, I talked about error handling, mutability and state, and programming paradigms. Now it’s time to look at a problem from the perspective of using type theory. My original plan was, after writing an idiomatic Haskell solution to making abstract sandwiches, to write a Haskell solution using type-level programming techniques. Writing an Agda solution was going to be the last step. Well, plans change. After some attempts at trying to write a meaningful type-level Haskell solution, I realized that Haskell’s type system is simply not equipped to express these kinds of ideas nearly as well as Agda’s.¹ Let me explain.

Defining a Sandwich as a Type

At the end of Part I, I explained how it’s easily possible to make an impossible sandwich with the previously proposed solution. Let’s see how we can fix that.

In the context of this exploration, I’m going to define a sandwich as follows:

A sandwich consists of a bottom and a top, which are both slices of bread. Neither the bottom or top can be smeared on the outside. At least one of the bottom or top must be smeared on the inside. A sandwich may be in one or more pieces (i.e., it can be cut).

I know, this doesn’t cover nearly all the exotic sandwiches you have in mind. I want to keep the scope of this problem small so the code is easier to understand, so we’re just going to deal with peanut butter and/or jelly sandwiches. To be clear, the reason sandwiches can’t be smeared on the outside is it makes them icky to hold.

So, with that definition in mind, let’s look at the Haskell sandwich from Part I and see where it falls short.

data Sandwich = Sandwich
  { bottom :: SliceOfBread
  , top :: SliceOfBread
  , pieces :: Integer
  }

(This isn’t exactly what I had in Part I. Here, I’ve made a small change to simplify the problem: instead of keeping track of the pieces and their details, we’re only interested in the number of pieces.)

What we have here is a definition of a Sandwich type in Haskell. The concept of type theory is that there are types and values (also called terms or elements). A value belongs to a certain type. No value exists without a type. When we think or program in type theory, we define what something is by making a new type for it. Then, we can make values of that type. Just like I gave an English definition of a sandwich (type), I can now go make an actual sandwich (value) and say that it fits the definition. For object-oriented programmers, it can help to think of types as being like classes and values as being like instances of a class.

Taking our Sandwich type and reverse engineering it into English, we get:

A sandwich consists of a bottom and a top, both slices of bread. (Off to a great start!) A sandwich may be in any number of pieces.

Hmm. This doesn’t quite match our desired definition. First, there’s nothing about smearing. And, the sandwich can be in zero or even negative pieces! Now, to be fair, the smearing is included in the SliceOfBread type:

data SliceOfBread = SliceOfBread
  { flavour :: BreadFlavour
  , top :: Maybe Condiment
  , bottom :: Maybe Condiment
  }

This type says, “a slice of bread is of a certain flavour and may be smeared with a condiment on the top and/or bottom.”

So, there is something about smearing, but it doesn’t have the restriction we want, about the sandwich’s bottom and top being smeared only on the inside. In fact, with Haskell’s type system, we can’t represent that! Our only option is to leave the type as it is and handle the proper making of a sandwich in the logic of functions and thread error handling through all those functions (using Either). But, as we’ve seen (in Part I), that still leaves us with the ability to make improper sandwiches if we forego the use of those functions. For example:

-- Two plain slices of bread shouldn't be considered a sandwich.
-- Not to mention it's in 0 pieces. What is this? An eaten sandwich?
badSandwich = Sandwich
  { bottom = SliceOfBread { flavour=Sourdough, top=Nothing, bottom=Nothing }
  , top = SliceOfBread { flavour=Sourdough, top=Nothing, bottom=Nothing }
  , pieces = 0
  }

The purpose of embedding our ideal definitions in types is to make it impossible to do things wrong. I don’t want it to be possible to make an improper sandwich, or even fail at any step along the way. That brings us to Agda.

Agda is a dependently typed programming language. Dependent types allow us to represent things intuitively. A dependent type is a type whose definition depends on a value. In the Sandwich type, its bottom has the type SliceOfBread, but that’s not enough information. We want it to be a SliceOfBread that is not smeared on its bottom. In other words, its type should be a SliceOfBread whose value looks something like this:

SliceOfBread { flavour=?, top=?, bottom=Nothing }

All this to say, the type of a sandwich’s bottom slice depends on its value.

In Agda, we can represent a sandwich like this:

record Sandwich : Type where
  field
    top : SliceOfBread
    bottom : SliceOfBread
    shellOk : checkShell top bottom
    pieces : Σ n ꞉ ℕ , n ≥ 1

In English, this means:

A sandwich must have all of the following properties:

• a top, which is a slice of bread
• a bottom, which is a slice of bread
• a proof that the shell is OK
• be cut into 1 or more pieces

Where’s the part about smearing? Well, that’s covered by the “proof that the shell is OK”. I’m calling the top and bottom slices of the sandwich its “shell”. The checkShell function looks like this:

checkShell : SliceOfBread → SliceOfBread → Type
checkShell top bottom =
  -- The top slice is not smeared on its top
  is-nothing (smearedTop top)
  -- and the bottom slice is not smeared on its bottom
  × is-nothing (smearedBottom bottom)
  -- and either the bottom is smeared on its top or the top is smeared on its bottom (or both).
  × (is-just (smearedBottom top) ∔ is-just (smearedTop bottom))

The type signature of this checkShell function says it takes in two slices of bread (a top and a bottom) and returns a type. Not a value of a specific type, like a boolean, but rather a value that is a type itself. A function returning a type as a value might seem like an odd thing, and it should, because it only makes sense in Agda-land. What does it mean? Why not return a boolean (true or false)? Well, if we return a boolean, we will have to check if the function returns true wherever we use it. But remember, we’re trying to make it impossible to build an improper sandwich. So, instead of checking that the function returned the right value, we can have a function that can only return a value if its arguments pass its validation check. This idea from type theory, often called “propositions as types”, is the idea that an element of a type is a proof of a theorem. In checkShell, the only elements of its resulting type are proofs that the top and bottom slices are smeared appropriately, as checked by the body of the function. Take a moment to digest this. Now, the Sandwich property shellOk has the type of checkShell top bottom, which means shellOk is a proof that the shell of the sandwich is OK! Anytime we want to make a value of the type Sandwich, we need to provide a proof that its shell is OK.

Altogether, this means we can only create a value of type Sandwich if it is a proper sandwich! And the type of Sandwich (together with checkShell) represents our original definition accurately:

A sandwich consists of a bottom and a top, which are both slices of bread. Neither the bottom or top can be smeared on the outside. At least one of the bottom or top must be smeared on the inside. A sandwich may be in one or more pieces (i.e., it can be cut).

Dependently Typed Utensils

In Part I, I encoded utensils in Haskell like this:

data Condiment = PeanutButter | Jelly

data UtensilShape = Knife | Spoon | Fork

data Utensil = Utensil
  { shape :: UtensilShape
  , loadedWith :: Maybe Condiment
  }

These are type definitions. A utensil has a shape (knife, spoon, or fork) and may be loaded with a condiment. Now, the problem is, I wanted to say that a utensil has a shape and may be loaded with a condiment if its shape is a knife. But we can’t write that in Haskell because loadedWith would depend on the value of shape.

Since Agda is dependently typed, we can easily write this!

-- We only have peanut butter and jelly in the pantry.
data Condiment : Type where
  peanutButter jelly : Condiment

data UtensilShape : Type where
  knife spoon fork : UtensilShape

record Utensil : Type where
  field
    shape : UtensilShape
    loadedWith : Maybe ((shape ≡ knife) × Condiment)

The Maybe type works the same as in Haskell, where the possible values of Maybe a are:

• nothing, or
• just x, where x is a value of type a.

The part (shape ≡ knife) × Condiment describes a pair of values (x , y), where x is a proof that the shape is a knife and y is a condiment.

Now, the only possible values of loadedWith are:

• nothing
• just (refl knife , peanutButter)
• just (refl knife , jelly)

refl knife is a proof that the shape is a knife (when it is, in fact, a knife).

We can make a knife loaded with peanut butter like this:

pbKnife : Utensil
pbKnife = utensil knife (just (refl knife , peanutButter))

If we try to make a fork loaded with peanut butter, we can’t:

pbFork : Utensil
pbFork = utensil fork (just (? , peanutButter))

Nothing fits in the question mark! We would need to provide a proof that fork ≡ knife, which is obviously impossible. We can only make a fork that’s clean:

cleanFork : Utensil
cleanFork = utensil fork nothing

Dependently Typed Actions

Now, for the sake of exploration, I wanted to see how far I could take this. So far, I’ve only shown implementions for static things, like sandwiches and utensils, but there’s more to the problem. In the Haskell code from Part I, there’s a function to fetch a utensil of a specified shape:

fetchUtensil :: UtensilShape -> Utensil
fetchUtensil s = Utensil
  { shape = s
  , loadedWith = Nothing
  }

This function takes a utensil shape and returns a clean utensil of that shape. However, the type signature of the function only says it takes a utensil shape and returns a utensil. It doesn’t specify that the returned utensil will be the right shape or that it will be clean; that’s left to the body of the function. The common approach to making sure this function is implemented correctly is to write tests for it:

testFetchUtensil :: IO ()
testFetchUtensil = do
  print (fetchUtensil Knife == Utensil { shape = Knife, loadedWith = Nothing })
  print (fetchUtensil Fork == Utensil { shape = Fork, loadedWith = Nothing })
  print (fetchUtensil Spoon == Utensil { shape = Spoon, loadedWith = Nothing })

Now, if we accidentally wrote fetchUtensil to always return a knife,

fetchUtensil :: UtensilShape -> Utensil
fetchUtensil s = Utensil
  { shape = Knife
  , loadedWith = Nothing
  }

our tests would catch the mistake.

But there’s another approach we can take. Using dependent types in Agda, we can give the function the type of “taking a utensil shape and returning a clean utensil of that shape”, just like I wanted to describe it.

fetchUtensil
  : (s : UtensilShape)
  → Σ u ꞉ Utensil , (shape u ≡ s) × is-nothing (loadedWith u)
fetchUtensil s = utensil s nothing , refl s , refl

What this type really says is, “take a utensil shape and return a pair of values (u , p) where u is a utensil and p is a proof that u has the given shape and is clean.” Then, the function body has no choice but to implement exactly that type. If we implement it any other way, the code won’t compile! This is the difference: having our mistakes caught during compiling versus running the code. If the function’s meaning is encoded in its type, our code won’t compile unless the function’s body honors that type.

To be clear, I’m not advocating for all programs to be written in Agda. It’s not a programming language meant for producing general purpose applications. In fact, it’s only meant for writing (mathematical) proofs. But! It’s a great tool for discovering, planning, and expressing ideas rigorously. If the kids in the Exact Instructions Challenge video had planned the steps to making a sandwich in Agda, they would have left no room for their dad to make mistakes. Silly dad, dependent types are for kids!

Just for fun, here’s the most complex part of the sandwich solution in Agda versus in Haskell. Not for the faint of heart!

Haskell:

loadFrom :: Utensil -> CondimentJar -> Either String (Utensil, CondimentJar)
loadFrom _ CondimentJar{lid=Closed} = Left "The jar is closed and knife-impermeable."
loadFrom _ CondimentJar{condiment=Nothing} = Left "The jar is empty. How disappointing."
loadFrom Utensil{shape=Fork} _ = Left "Forks aren't the right shape for condiments."
loadFrom u cj@CondimentJar{condiment=Just c}
  = Right (u { loadedWith = Just c }, cj { condiment = Nothing })

Agda:

-- A Maybe value is left unchanged if we map it to the second value of a pair and project that second value.
-- Needed to prove this for part of loadFrom (following).
map-pr₂-pair-refl
  : {A B : Type} {b : B} (ma : Maybe A)
  → ma ≡ map pr₂ (map (λ (a : A) → (b , a)) ma)
map-pr₂-pair-refl {A} {B} {b} (just x) = refl (just x)
map-pr₂-pair-refl {A} {B} {b} nothing = refl nothing

-- Load a clean knife with a condiment from a jar that is open and full.
-- Take a utensil that is a knife and clean.
-- Take a condiment jar that is full and open.
-- Return the knife, now loaded with the condiment from the jar,
--   and the condiment jar, still open but now empty.
loadFrom
  : (uₛ : Σ u ꞉ Utensil , (shape u ≡ knife) × is-nothing (loadedWith u))
    (cjₛ : Σ cj ꞉ CondimentJar , is-just (condiment cj) × (state cj ≡ open'))
  → Σ (u' , cj') ꞉ Utensil × CondimentJar
    , (shape u' ≡ shape (pr₁ uₛ)) -- Same shape (*the* knife)
      × (condiment (pr₁ cjₛ) ≡ map pr₂ (loadedWith u')) -- Loaded with condiment from jar
      × (state cj' ≡ state (pr₁ cjₛ)) -- State unchanged (still open)
      × is-nothing (condiment cj') -- Now empty
loadFrom
  (u , isKnife , notLoaded)
  (cj , isFull , isOpen)
  = (record u { loadedWith = loadedWith' } , record cj { condiment = nothing })
    , refl (shape u) , isLoaded' , refl (state cj) , refl
  where
  loadedWith' : Maybe ((shape u ≡ knife) × Condiment)
  loadedWith' = map (λ x → (isKnife , x)) (condiment cj)

  isLoaded' : condiment cj ≡ map pr₂ loadedWith'
  isLoaded' = map-pr₂-pair-refl (condiment cj)

Making a Sandwich

Now that I’ve shown how static things and actions can be written in Agda, how about using these individual parts together to make a sandwich? Remember, the main goal of this whole exercise is to demonstrate what it would be like to program a computer to make a sandwich (without ending up with a real sandwich being squeezed out the USB port).

I’m going to show a few examples of attempts at making a sandwich and how mistakes are caught. To be clear, a failed attempt doesn’t mean something is wrong with the functions for making sandwiches; it’s the opposite! It’s showing how the code forces us to make proper sandwiches. In each of these attempts, I’m going to mock getting items from the kitchen by invoking fetching functions like fetchUtensil, but it should be understood that any method of creating a value of a certain type equates to fetching it in the real world (things don’t magically come into existence).

Attempt 1: Forgot to open the jar of peanut butter

This attempt didn’t result in a completed sandwich because we forgot to open the jar of peanut butter.

sandwichAttempt1 : Sandwich
sandwichAttempt1 = {!!}
  where
  -- Get a knife with peanut butter.
  step1 : Σ _ ꞉ Utensil × CondimentJar , _
  step1 =
    let
      newKnife : Utensil
      newKnife = pr₁ (fetchUtensil knife)
      pb : CondimentJar
      pb = pr₁ (fetchCondimentJar peanutButter)
    -- Not possible because the pb jar isn't open!
    in loadFrom (newKnife , (refl knife , refl)) (pb , ((peanutButter , refl) , {!!})) -- closed ≡ open'

In Agda, {!!} denotes a hole to be filled with some value of the expected type. When writing Agda code, it’s typical to have lots of holes, and the goal is to fill them all with appropriate types (and with interactive assistance of Agda, which is really cool!). The first hole, in sandwichAttempt1 = {!!} is expecting a value of type Sandwich. Since this is a failed attempt at making a sandwich, this hole will be left unfilled. The real evidence that this attempt isn’t going to work is on the last line:

loadFrom (newKnife , (refl knife , refl)) (pb , ((peanutButter , refl) , {!!}))

The hole at the end of that line is expecting a value of the type closed ≡ open', meaning a proof that closed is the same as open. It’s expecting this type because loadFrom takes an open condiment jar as its second argument and we’ve given it a closed one, pb. Obviously, we can’t supply a proof that the given jar is open because it’s not! So this hole must remain unfilled, and we’ll stay hungry.

Attempt 2: Tried to make a sandwich without condiments

sandwichAttempt2 : Sandwich
sandwichAttempt2 = sandwich topSlice' bottomSlice' (refl , refl , {!!}) (1 , ⋆)
  where
  -- Get a knife with peanut butter.
  step1 : Σ _ ꞉ Utensil × CondimentJar , _
  step1 =
    let
      newKnife : Utensil
      newKnife = pr₁ (fetchUtensil knife)
      pb : CondimentJar
      pb = pr₁ (fetchCondimentJar peanutButter)
    in loadFrom (newKnife , (refl knife , refl)) (pr₁ (openJar pb) , ((peanutButter , refl) , refl open'))

  -- Get a couple slices of bread.
  topSlice' : SliceOfBread
  topSlice' = pr₁ (fetchSliceOfBread wholeGrain)
  bottomSlice' : SliceOfBread
  bottomSlice' = pr₁ (fetchSliceOfBread sourdough)

This time, we got closer to making a proper sandwich! In step1, we got a knife and loaded it with peanut butter from a jar. Then, we got a couple slices of bread. We didn’t bother to use our knife or spread any condiments on either slice; we just left them plain. When we tried to make a sandwich out of these plain slices, we ended up with a hole:

sandwich topSlice' bottomSlice' (refl , refl , {!!}) (1 , ⋆)

This hole is expecting a value of the type is-just (smearedBottom topSlice') ∔ is-just (smearedTop bottomSlice'), which means a proof that the top slice is smeared on its bottom or the bottom slice is smeared on its top. Since our slices are plain, we can’t provide that!

Attempt 3: Successful sandwich making!

Okay, this is a long one. Hey, it takes a lot of work to make a proper sandwich!

sandwichAttempt3 : Sandwich
sandwichAttempt3 = sandwich topSliceWithJelly bottomSliceWithPB (refl , (refl , inl (jelly , refl))) (1 , ⋆)
  where
  -- Get a knife with peanut butter.
  step1 : Σ _ ꞉ Utensil × CondimentJar , _
  step1 =
    let
      newKnife : Utensil
      newKnife = pr₁ (fetchUtensil knife)
      pb : CondimentJar
      pb = pr₁ (fetchCondimentJar peanutButter)
    in loadFrom (newKnife , refl knife , refl) (pr₁ (openJar pb) , (peanutButter , refl) , refl open')

  -- Get a slice of bread and smear it with the PB knife.
  step2 : Σ _ ꞉ SliceOfBread × Utensil , _
  step2 =
    let
      bottomSlice : SliceOfBread
      bottomSlice = pr₁ (fetchSliceOfBread sourdough)
      pbKnife : Utensil
      pbKnife = pr₁ (pr₁ step1)
      emptyPB : CondimentJar
      emptyPB = pr₂ (pr₁ step1)
    in
      smearSliceOfBread
      (pbKnife , (refl (shape pbKnife)) , ((refl (shape pbKnife)) , peanutButter) , refl)
      top
      (bottomSlice , (inl (refl top , refl)))

  -- Our successfuly smeared slice to be used as the bottom of the sandwich!
  bottomSliceWithPB : SliceOfBread
  bottomSliceWithPB = pr₁ (pr₁ step2)

  -- Get another slice of bread and smear it with jelly, using the same knife as before.
  step3 : Σ _ ꞉ SliceOfBread × Utensil , _
  step3 =
    let
      jellyKnife : Utensil
      jellyKnife =
        let
          -- The knife is now clean after having spread all its peanut butter on the other slice.
          usedKnife : Utensil
          usedKnife = pr₂ (pr₁ step2)
          j : CondimentJar
          j = pr₁ (fetchCondimentJar jelly)
        in pr₁ (pr₁ (loadFrom (usedKnife , (refl knife , refl)) (pr₁ (openJar j) , (jelly , refl) , refl open')))
      topSlice : SliceOfBread
      topSlice = pr₁ (fetchSliceOfBread wholeGrain)
    in
      smearSliceOfBread
      (jellyKnife , (refl knife , (refl knife , jelly) , refl))
      bottom
      (topSlice , (inr (refl bottom , refl)))

  -- Our successfully smeared slice to be used as the top of the sandwich!
  topSliceWithJelly : SliceOfBread
  topSliceWithJelly = pr₁ (pr₁ step3)

I broke it down into steps (step1, step2, step3) so it’s a bit easier to follow. The important part is we have our sandwich:

sandwich topSliceWithJelly bottomSliceWithPB (refl , (refl , inl (jelly , refl))) (1 , ⋆)

It has a top slice, a bottom slice, proof that the slices are smeared appropriately, and it’s in 1 piece.

For most of you, it’s probably really difficult to try reading a foreign language in an unfamiliar paradigm. Don’t worry about piecing together every little bit. What you should be looking at are the types of the variables and what things they refer to. For example:

usedKnife : Utensil
usedKnife = pr₂ (pr₁ step2)

The first line tells us usedKnife is a utensil. And, in the second line, we can see it comes from step2, which involved a knife being used to smear a slice of bread with peanut butter, as the comment says. So, now we know usedKnife is not just any utensil, but a knife, and the one we used previously.

See the full code on GitHub: https://github.com/SlimTim10/simple-sandwich

Conclusion

I hope you enjoyed this exploration with me! Send me a message if you have any comments or feedback. I love to chat about this stuff! Many thanks to Danny for sparking this idea and sharing the journey. Go check out his blog, it’s a real treat to read.