Rohit's Blog

Occasional writing on software engineering.

Lava in Scala 3, Part 1: One Circuit, Four Interpretations

scaladsl

This series works through “Lava: Hardware Design in Haskell” by Per Bjesse, Koen Claessen, Mary Sheeran and Satnam Singh (ICFP 1998). Lava is a hardware description language embedded in Haskell, and its central trick is that a circuit description is polymorphic in its own interpretation: write the circuit once, then simulate it, generate a logical formula and hand it to a theorem prover, or emit VHDL for fabrication — all from the same source.

The design is theirs. The Scala 3 is mine, and this one has an unusual property: the authors’ stated future work is a language feature Scala already has.

🔗The problem

Hardware design got productive by climbing levels of abstraction — transistors, then gates, then register-transfer level, then programming languages. VHDL and Verilog were the step that made modern chips possible.

But VHDL was designed as a simulation language, and it is now used as input to synthesis engines, equivalence checkers, and formal verification tools. It fits some of those badly.

What you actually want is to describe a circuit at whatever level suits you, and then analyse that one description in many ways. The paper names three as essential:

  • Simulation — feed it inputs, look at the outputs.
  • Verification — prove a property about it.
  • Code generation — produce something a fab can build.

All three, on one description. The authors note the temptation to design yet another hardware description language, and that they resisted it. Instead: embed one in Haskell, and let the host language’s type system carry the weight.

🔗The trick, in one function

Here’s a half adder — two input bits, two output bits, an AND gate and an XOR gate.

In Haskell it’s a function whose type is polymorphic in a monad m, constrained by a class Circuit. Choosing m chooses the interpretation. The circuit doesn’t know and doesn’t care.

In Scala 3:

def halfAdd[F[_]](using c: Circuit[F])(a: c.Bit, b: c.Bit): F[(c.Bit, c.Bit)] =
  import c.given
  for
    carry <- c.and2(a, b)
    sum   <- c.xor2(a, b)
  yield (carry, sum)

Two inputs, two outputs, and — by convention throughout Lava — wires are grouped so that a circuit always takes exactly one value and returns exactly one value.

If that shape looks familiar, it should: this is tagless final. An abstract effect type F[_], a capability trait constraining it, and a program written against the capability rather than any concrete implementation. The technique is Scala bread-and-butter and most Scala programmers learned it from Carette, Kiselyov and Shan’s Finally Tagless, Partially Evaluated — which is from 2009. Lava is doing it in 1998, for circuits, and the paper doesn’t even remark on it. It just needed multiple interpretations and this is what fell out.

🔗The capability hierarchy

Not every operation makes sense to every interpretation. Arithmetic makes sense to a high-level simulation and is meaningless to a physical circuit, which has no notion of numbers at all. So Lava is structured as a hierarchy of classes, and a circuit’s type says which interpretations are allowed to run it.

The base class requires being a monad, plus the basic gates:

trait Circuit[F[_]] extends Monad[F]:
  type Bit

  def low: Bit
  def high: Bit

  def and2(a: Bit, b: Bit): F[Bit]
  def or2(a: Bit, b: Bit): F[Bit]
  def xor2(a: Bit, b: Bit): F[Bit]
  def inv(a: Bit): F[Bit]

Then subclasses for capabilities that only some interpretations have:

trait Arithmetic[F[_]] extends Circuit[F]:
  type Num
  def plus(a: Num, b: Num): F[Num]
  def times(a: Num, b: Num): F[Num]

trait Sequential[F[_]] extends Circuit[F]:
  def delay(init: Bit, x: Bit): F[Bit]
  def loop(f: Bit => F[Bit]): F[Bit]

trait Symbolic[F[_]] extends Circuit[F]:
  def newBitVar: F[Bit]

And now a circuit’s type is a statement about what can run it:

def square[F[_]](using a: Arithmetic[F])(x: a.Num): F[a.Num] =
  a.times(x, x)

square can only be run by an interpretation that supports arithmetic. That’s checked at compile time, and it’s the same discipline as a well-designed tagless-final effect stack: ask for the narrowest capability you need, and the type documents it.

🔗The future work that Scala already had

The paper’s Future Work section contains a sentence I did a double-take at:

We would be able to generalise our system further if multiple parameter type classes were provided in Haskell.

Their problem: all interpretations share the same primitive datatypes. A Bit is the same Bit whether you’re simulating or generating VHDL, so it has to be a sum type big enough for every interpretation at once — a concrete boolean and a symbolic variable, with the constructors kept abstract so that the simulator can’t be handed a variable it has no idea what to do with. That’s a runtime-enforced invariant standing in for a type-level one.

What they wanted was for each interpretation to bring its own datatypes.

In Scala 3 that’s a type member, which is what type Bit above is doing:

object Std extends Circuit[Id]:
  type Bit = Boolean                    // simulation: a bit is a boolean

object Sym extends Symbolic[SymM]:
  type Bit = BitExpr                    // symbolic: a bit is an expression

The simulator’s Bit is Boolean. There is no constructor for a variable, so the impossible state isn’t guarded against — it’s unrepresentable. The abstract-constructor discipline the paper needed becomes a type equation.

Two honest caveats, because “Scala wins” claims need them.

This is history, not a live Haskell deficiency. Multi-parameter type classes were already available as a GHC extension in 1998 and have been standard practice for decades. The paper is a snapshot of Haskell 98.

And Scala’s version costs something at the use site. Because Bit is a member of the instance, referring to it means referring to that instance’s Bit — a path-dependent type. Hence the slightly unusual signature:

def halfAdd[F[_]](using c: Circuit[F])(a: c.Bit, b: c.Bit): F[(c.Bit, c.Bit)]

The using clause comes first, so that later parameters can mention c. Scala 3 allows that, and here it’s essential. If path-dependent types are unfamiliar, the dependent and structural types post covers the mechanics.

If you’d rather pay the cost as extra type parameters, the literal multi-parameter encoding works too:

trait Circuit[F[_], Bit]:
  def and2(a: Bit, b: Bit): F[Bit]

def halfAdd[F[_], B](a: B, b: B)(using Circuit[F, B], Monad[F]): F[(B, B)]

Cleaner signatures, noisier types as the hierarchy grows — Arithmetic needs Bit and Num, and every downstream signature carries both. I’ve used type members throughout because the hierarchy is what gets complicated, and that’s exactly where members pay off.

🔗The simplest interpretation

A combinational circuit has no notion of time or state, so simulating one needs no effects at all. The identity monad suffices:

type Id[A] = A

object Std extends Circuit[Id]:
  type Bit = Boolean

  def low  = false
  def high = true

  def and2(a: Boolean, b: Boolean): Id[Boolean] = a && b
  def or2 (a: Boolean, b: Boolean): Id[Boolean] = a || b
  def xor2(a: Boolean, b: Boolean): Id[Boolean] = a != b
  def inv (a: Boolean): Id[Boolean]             = !a

  // Monad[Id] — flatMap is application, pure is identity
  def pure[A](a: A): Id[A] = a
  def flatMap[A, B](fa: Id[A])(f: A => Id[B]): Id[B] = f(fa)
  def tailRecM[A, B](a: A)(f: A => Id[Either[A, B]]): Id[B] =
    f(a) match
      case Right(b) => b
      case Left(a2) => tailRecM(a2)(f)

Run it and the half adder computes:

scala> halfAdd(using Std)(true, true)
val res0: (Boolean, Boolean) = (true, false)

One and one is two: carry set, sum clear.

tailRecM is cats bookkeeping rather than anything from the paper — cats requires it for stack safety, and for Id it’s the obvious loop. Worth knowing it’s there; not worth thinking about.

🔗What the other three look like

The rest of the series builds them, but the shape is worth having up front, because it isn’t what I expected:

Simulation is a different monad — Id, no effects, values in and values out.

Verification and VHDL are the same monad. Both need symbolic evaluation: feed the circuit abstract variables instead of values, and what comes back is a description of the circuit rather than an answer. That description is a netlist — a list of assertions naming each gate’s output. From there, verification and VHDL generation differ only in how you print the netlist. One emits a logical formula for a theorem prover; the other emits an entity and an architecture.

That surprised me. I had assumed four interpretations meant four monads. It’s two monads and three back-ends, and the reason is that “generate a description” is one capability with many consumers.

Layout is the fourth, and it’s the one I find most charming. It’s symbolic evaluation extended to track not just how components are functionally composed but where they sit on the gate array. In the layout interpretation, A >-> B means “A feeds B” and “A is placed to the left of B”. One operator, two meanings, kept in sync by construction — where in VHDL you’d attach position attributes to instances by hand and hope they still match the netlist next week.

🔗Where this sits

If you’ve been following along, this is the same idea as Composing Contracts with the payoff moved. There, one contract description drove one interpreter, and the interesting work was in the semantics. Here the semantics is comparatively simple and the interesting work is in there being several.

That’s the general argument for a deep embedding, and Lava is the cleanest demonstration of it I know: a description you can take apart is a description you can do arithmetic on, prove things about, compile, and lay out. A description made of host-language closures is a description you can only run.

Next: Part 2 — Combinators for regular circuits, in which higher-order functions turn out to matter more in practice than the authors expected, and >-> turns out to be something cats already ships.

🔗Sources

  • Bjesse, Per, Koen Claessen, Mary Sheeran & Satnam Singh. Lava: Hardware Design in Haskell. ICFP 1998. The monadic embedding, the Circuit/Arithmetic/Sequential/Symbolic class hierarchy, the identity-monad simulator, the layout interpretation, and the observation about wanting multiple-parameter type classes are all theirs.
  • Sheeran, Mary. μFP, an Algebraic VLSI Design Language. 1985, and Jones & Sheeran’s Ruby — the earlier work Lava builds on.
  • Carette, Jacques, Oleg Kiselyov & Chung-chieh Shan. Finally Tagless, Partially Evaluated. JFP 2009 — the technique Lava is using eleven years early.
  • O’Donnell, John. Hydra — the monad-free alternative the paper credits as an inspiration, and whose cleaner types it explicitly concedes.

The Scala 3 translation, the type-member encoding of per-interpretation datatypes, and the observation that this is the generalisation the authors wanted are mine.