../
2025-05-17
This article will use Haskell.
Let’s start by enabling some extensions:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds#-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
import Data.Type.Equality
Everything in a computer is “Zero” and “One”:
data Bit = Zero | One
We create a type for each of the two values in the Bit type—"Zero" and “One"—which is called a Singleton Type:
-- Prefix S, an abbreviation for Singleton
data SBit :: Bit -> * where
SZero :: SBit 'Zero
SOne :: SBit 'One
All Boolean circuits can be built using “NAND gates,” but first, we must define the “NAND gate”:
type family Nand (a :: Bit) (b :: Bit) :: Bit where
Nand 'One 'One = 'Zero
Nand _ _ = 'One
The type family provides the “definition,” which can also be called the “Specification” (or Spec). Whether proving or checking, the goal is to ensure the program complies with the standard defined here.
Then we can implement it:
nandGate :: SBit a -> SBit b -> SBit (Nand a b)
nandGate SOne SOne = SZero
nandGate SZero _ = SOne
nandGate _ SZero = SOne
Zero becomes one, one becomes zero; this is the NOT gate. Therefore, we give the definition:
type family Not (a :: Bit) :: Bit where
Not 'One = 'Zero
Not 'Zero = 'One
The “NOT gate” can be implemented using the “NAND gate”:
notGateImpl x = nandGate x x
Submit this implementation to the compiler:
notGate :: SBit a -> SBit (Not a)
notGate = notGateImpl
It gets rejected by the compiler:
Couldn't match type: Nand a a
with: Not a
Expected: SBit a -> SBit (Not a)
Actual: SBit a -> SBit (Nand a a)
notGateImpl returns SBit (Nand a a), while the return value expected by notGate is SBit (Not a). We need to prove that SBit (Not a) and SBit (Nand a a) are the same thing. This way, we can achieve the conversion.
There are two approaches here. The first is to crush it with pure force, using brute-force enumeration to prove that this relationship is absolutely true:
notGateProof :: SBit a -> SBit (Nand a a) :~: SBit (Not a)
notGateProof SOne = Refl
notGateProof SZero = Refl
Then, use this proof to implement a safe type cast:
notGate :: SBit a -> SBit (Not a)
notGate x = castWith (notGateProof x) (notGateImpl x)
Thus, the “NOT gate” is complete.
The second approach is to settle for the next best thing and only add a type constraint:
notGate :: (SBit (Nand a a) ~ SBit (Not a)) => SBit a -> SBit (Not a)
notGate x = nandGate x x
This also compiles, and the code is simpler.
However, this feels more like a “static check.” For example, if we deliberately write an incorrect implementation:
notGate :: (SBit 'Zero ~ SBit (Not a)) => SBit a -> SBit (Not a)
notGate x = SZero
Obviously, SBit 'Zero and SBit (Not a) are not equivalent when a is 'Zero, but this still passes compilation.
If a notGate call appears in the program where x is SOne:
zero = notGate SOne
Because it happens to satisfy the condition, it still compiles.
Only when a notGate call where x is SZero appears in the program:
one = notGate SZero
will the problem be discovered during type checking. At this point, the compiler will report an error:
• Couldn't match type ‘'Zero’ with ‘'One’
arising from a use of ‘notGate’
• In the expression: notGate SZero
In an equation for ‘one’: one = notGate SZero
Since the second method is simpler, I won’t go into further detail about it later; I will only introduce the first method. From a practical perspective, proofs for the first method are often hard to provide, and most of the time, the “static check” of the second method is sufficient.
What is an “AND gate”? One combined with one yields one; the rest yield zero:
type family And (a :: Bit) (b :: Bit) :: Bit where
And 'One 'One = 'One
And _ _ = 'Zero
A NAND gate plus a NOT gate makes an AND gate:
andGateImpl a b = notGate $ nandGate a b
Brute-force proof via enumeration:
andGateProof :: SBit a -> SBit b -> SBit (Not (Nand a b)) :~: SBit (And a b)
andGateProof SZero SOne = Refl
andGateProof SZero SZero = Refl
andGateProof SOne SOne = Refl
andGateProof SOne SZero = Refl
Submit to the compiler:
andGate :: SBit a -> SBit b -> SBit (And a b)
andGate a b = castWith (andGateProof a b) (andGateImpl a b)
The “AND gate” is complete.
As usual, we first give the definition: zero and zero make zero, the rest are all one:
type family Or (a :: Bit) (b :: Bit) :: Bit where
Or 'Zero 'Zero = 'Zero
Or _ _ = 'One
Let’s try a fancy implementation method, using De Morgan’s laws to compose an “OR gate” using “AND gates” and “NOT gates”:
orGateImpl a b = notGate (andGate (notGate a) (notGate b))
Continue with brute-force enumeration to prove we are right:
orGateProof :: SBit a -> SBit b
-> SBit(Not (And (Not a) (Not b))) :~: SBit (Or a b)
orGateProof SZero SZero = Refl
orGateProof SZero SOne = Refl
orGateProof SOne SZero = Refl
orGateProof SOne SOne = Refl
The compiler happily accepts it:
orGate :: SBit a -> SBit b -> SBit (Or a b)
orGate a b = castWith (orGateProof a b) (orGateImpl a b)
What is presented here is an example so trivial it couldn’t be more trivial, but it uses quite a few language features, serving as a summary of my recent studies. However, implementing non-trivial examples often requires using some very complex and ugly Template Haskell libraries, which I don’t really want to touch, so I plan to look into Lean 4 later.
Mistivia - https://mistivia.com