Brian McKenna

For the past few years I’ve been the most senior developer on my teams in Atlassian, in both position (Principal Engineer) and time (almost 9 years) - this means I usually take on the responsibility of managing our software architecture.

Architecture is the relationships between systems, which can be fairly tricky to talk about. Probably the best form of communication is a diagram, with boxes representing systems (or components) and lines representing relationships between them. This can still have issues.

When my previous engineering manager joined the Atlassian Marketplace team, he asked everyone to draw an architecture diagram. Each came out extremely different. The people focused on frontend had things like Jira, Embedded Marketplace, Commerce, Provisioning, Atlassian Connect, then an arrow to a huge box - just labelled Marketplace backend.

The people focused on backend had the reverse - a huge box just labelled frontend!

Actual relationships do exist between systems (e.g. network calls, shared storage) but an architecture diagram can’t give all details without becoming the code it’s meant to represent. That means all architecture diagrams are views into an abstraction. It’s not wrong to have a big box representing your backend; it’s just one way of viewing an abstraction.

Some teams and projects will have a diagram and point to it as “here is the architecture” - but it’s not the architecture, it’s just one particular view.

Ideally, we’d have dozens of architecture diagrams - from various views, from various proposals, from various teams. We don’t see this very much and I think part of the problem is that architecture diagrams can be costly.

Most diagramming tools require you to use the mouse, pointing and clicking and dragging and drawing. They can be very fiddly and even buggy; e.g. there’s one architecture diagram for Atlassian Marketplace with an old outdated box that can’t be deleted using the software it was diagrammed in, it just won’t allow that, for some reason.

If someone adds a relationship to a new system, will they even remember to visit the Confluence page to click and drag and draw over the architecture diagrams?

Maybe we should write architecture diagrams using code instead. With code, we can update architecture diagrams within a pull request, version them and quickly modify many of them at once.

We can also add some formality. Instead of modelling things with lines and boxes, we can directly model systems and relationships.

The C4 Model formalises architecture into 4 abstractions: system context, containers, components and code. I only use system context and containers; components and code are too detailed. A container is something which runs, such as an application server, database, filesystem, etc. A system represents some group of software, and it can have containers which that software is deployed within.

There are a bunch of tools for using C4. There are two which you might have already used for other things, such as PlantUML and Mermaid. One of the above images was generated from this PlantUML code:

@startuml
!include  https://raw.githubusercontent.com/plantuml-stdlib/C4-PlantUML/master/C4_Container.puml

title Marketplace from backend view

AddElementTag("highlight", $bgColor="orange")

System(marketplace, "Marketplace")
System(commerce, "Commerce")
System(hams, "HAMS")
System(identity, "Atlassian Identity")
System(pako, "People Atlassian Knows Of")
System(frontend, "Marketplace FRONTEND", $tags="highlight")
System(algolia, "Algolia")
System(upm, "Universal Plugin Manager")

Rel(marketplace, commerce, "Fetches pricing")
Rel(marketplace, hams, "Fetches legacy pricing")
Rel(marketplace, identity, "Fetches users")
Rel(marketplace, pako, "Queries reports")
Rel(marketplace, algolia, "Searches")
Rel(frontend, marketplace, "Queries")
Rel(upm, marketplace, "Queries")

SHOW_LEGEND()

@enduml

But instead of writing PlantUML, I use Haskell to model architecture. A simple example would look like:

data AtlassianSystem
  = Marketplace
  | Identity
  | Pako
  deriving (Eq, Ord, Show)

data AtlassianTechnology
  = REST
  | SQL
  deriving (Eq, Ord, Show)

marketplaceSystem ::
  SoftwareSystem
    AtlassianSystem
    ()
    AtlassianTechnology
    ()
marketplaceSystem =
  softwareSystem
    & relationships . at Identity ?~ relationship REST
    & relationships . at Pako ?~ relationship SQL

marketplace ::
  Model
    ()
    ()
    AtlassianSystem
    ()
    AtlassianTechnology
    ()
marketplace =
  model
    & softwareSystems . at Marketplace ?~ marketplaceSystem
    & softwareSystems . at Identity ?~ softwareSystem
    & softwareSystems . at Pako ?~ softwareSystem

And the Haskell library can spit out PlantUML from this model. There’s a few checks which can be implemented on this model, e.g. do any components reference systems which their container doesn’t?

Going further into code, most systems have a consistent way of communicating with services. Atlassian has a Service Proxy to handle common service to service communication. When configuring Service Proxy, you give it a list of services that your service depends on. We can easily write some Haskell which takes that configuration and spits out a C4 Model, allowing us to create a bunch of diagrams.

We can also generate a model from running tests. Each test can generate a sequence diagram using something like DataFlow. Collecting the systems used in all tests can generate a C4 system context and container diagram for our whole system. Here’s an example sequence diagram generated by running a single test:

I’m pretty convinced that we should be using code to generate architecture diagrams. Code allows making quick changes. Architecture code can be versioned with the code which implements it. We can write algorithms to check our architecture. I’d like to see more tools available to describe architecture as part of code, allowing us to generate as many diagrams as we want, for accurate and easy communication.

Do you use code to diagram architecture? Do you do something other than just write PlantUML or Mermaid, by hand? I’d love to hear more!

A while ago I blogged about using Agda to prove the parity of added numbers. I’ve recently been doing some work on Idris and wondered how easy it would be to translate my Agda proof to Idris.

The original Agda code looked something like this:

module EvenOdd where

open import Data.Nat

data Even : ℕ → Set where
  evenZero : Even 0
  evenSuc : {n : ℕ} → Even n → Even (suc (suc n))

_e+e_ : {n m : ℕ} → Even n → Even m → Even (n + m)
evenZero e+e b = b
evenSuc a e+e b = evenSuc (a e+e b)

The direct Idris translation looks like:

module EvenOdd

data Even : Nat -> Type where
  evenZ : Even Z
  evenS : Even n -> Even (S (S n))

total
ee : Even n -> Even m -> Even (n + m)
ee evenZ m = m
ee (evenS n) m = evenS (ee n m)

The few differences:

• We don’t have to import a Nat type

• Totality is not the default (there is a flag to make it so, though)

• We can’t define mixed letter and symbol operators

Pretty easy! Time for something trickier. Now, I haven’t done very much type level Haskell but I wanted to see how easy it would be to translate to the recent GHC 7.8 release.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}

module EvenOdd where

data Nat = Z | S Nat

data Even :: Nat -> * where
  EvenZ :: Even Z
  EvenS :: Even n -> Even (S (S n))

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

ee :: Even n -> Even m -> Even (Plus n m)
ee EvenZ m = m
ee (EvenS n) m = EvenS (ee n m)

Getting a bit trickier. We’ve had to do the following:

• Enable data type promotion, so that data types can be kinds

• Enable type families, so we can write a type level functions

• Define our own Nat and use that as a kind

• Define our own Plus type level function (the type family)

• Get totality results as warnings (or errors via -Wall)

The few problems are caused by Haskell’s distinction between values, types and kinds. Everything else looks extremely similar - we’ve been lucky to fall into an area where the GHC data kinds extension works really well and we can promote our simple Nat type to a kind.

Let’s step it right up. Now let’s encode this in Scala. Are you ready?

package org.brianmckenna.evenodd

sealed trait Nat
trait Z extends Nat
case object Z extends Z
case class S[N <: Nat](n: N) extends Nat

sealed trait Even[N <: Nat]
trait EvenZ extends Even[Z]
case object EvenZ extends EvenZ
case class EvenS[N <: Nat](n: Even[N]) extends Even[S[S[N]]]

object Even {
  implicit val evenZ = EvenZ
  implicit def evenS[N <: Nat](implicit even: Even[N]) = EvenS[N](even)
}

sealed trait Plus[N <: Nat, M <: Nat] {
  type Result <: Nat
}

object Plus {
  type Aux[N <: Nat, M <: Nat, R <: Nat] = Plus[N, M] {
    type Result = R
  }

  implicit def plusZ[M <: Nat] = new Plus[Z, M] {
    type Result = M
  }

  implicit def plusS[N <: Nat, M <: Nat](implicit plus: Plus[N, S[M]]) = new Plus[S[N], M] {
    type Result = plus.Result
  }
}

object ee {
  def apply[N <: Nat, M <: Nat, R <: Nat](n: Even[N], m: Even[M])(implicit sum: Plus.Aux[N, M, R], re: Even[R]) = re
}

Now, this probably looks pretty verbose since we have to define our own type level Nat and Plus function. The type level Plus uses Scala’s path-dependent types.

What’s interesting is that our theorem is expressed as a constraint that given Even[N] and Even[M] then we can construct an Even[N + M] from an implicit. What we’ve given up is a constructive proof that every combination of two even numbers always results in an even number (but we know from our previous proofs that it’s true) - specifically, we can’t tell if the the implicit re can be found for all values. We could fix this by splitting the implicit up into each case but we can’t get totality checking.

Hopefully this gives a very quick feel for programming at the type level in Agda, Idris, Haskell and Scala. Type level programming in Agda and Idris is just as easy as programming at the value level. Type level programming in Haskell and Scala is a bit annoying, we have to write functions very differently at the type level and value level, but it’s impressive that we can achieve our goal in much more widely used languages.

Thanks to Miles Sabin for help with simplifying the Scala version.