Programs are Proofs!
It sounds really weird that program are proofs, but this is where it gets really fun.
Think about the types in the simple typed language:
type ::= primitive | function | ( type ) primitive ::= A | B | C | D | ... function ::= type -> type
Look at the type “A -> A”. Now, instead of seeing “->” as the function type constructor, try looking at it as logical implication. “A implies A” is clearly a theorem of intuitionistic logic. So the type “A -> A” is a theorem in the corresponding logic.
Now, look at “A -> B”. That’s not a theorem, unless there’s some other context that proves it. As a function type, that’s the type of a function which, without including any context of any kind, can take a parameter of type A, and return a value of a different type B. You can’t do that - there’s got to be some context which provides a value of type B - and to access the context, there’s got to be something to allow the function to access its context: a free variable. Same thing in the logic and the lambda calculus: you need some kind of context to establish “A->B” as a theorem (in the logic)
If there is a closed expression whose type is a theorem in the corresponding intuitionistic logic, then the expression that has that type is a proof of the theorem.
As all we known, Haskell doesn’t have dependent type, but we can get very close with extensions, e.g. “GADT (Generalized Algebraic Data Type)”, and prove theorem by it.
Use GADT to “simulate” Dependent Type
First we need types to represent values
data Z data S n
S n are just types, you cannot construct values with these types. We need to connect them with some values we can construct.
data Nat :: * -> * where Zero :: Nat Z Succ :: Nat n -> Nat (S n)
Now we have natural numbers whose values is represented by types .
(Succ Zero) :: Nat (S Z) -- 1 (Succ (Succ Zero)) :: Nat (S (S Z)) --2
In another words, its type is isomorphic to its value.
It is meaningless to have only numbers, so the next thing is to build arithmetic on it.
What would be
Nat n + Nat m ?
Firstly, it should be a
Nat, and then its type should correspond to the sum.
With the help of GHC’s Type Family and Type Operator extension, we can give reasonable definition of addition and multiplication on the level of types.
type family (:+:) (n :: *) (m :: *) :: * type instance Z :+: m = m type instance S n :+: m = S (n :+: m) type family (:*:) (n :: *) (m :: *) :: * type instance Z :*: m = Z type instance S n :*: m = m :+: (n :*: m)
Then the addition and multiplication on the level of values.
infixl 4 + -- priority 4 (+) :: Nat n -> Nat m -> Nat (n :+: m) Zero + n = n (Succ x) + n = Succ (x + n) infixl 5 * -- priority 5 (*) :: Nat n -> Nat m -> Nat (n :*: m) Zero * _ = Zero (Succ n) * m = m + n * m
(Succ (Succ Zero)) * (Succ (Succ Zero)) :: Nat (S (S (S (S Z))))
Since we have natural numbers based on types, we can define
Vector now (
List that have length information in their types).
data Vec * -> * -> * where VNil :: Vec a Z --  VCons :: a -> Vec a n -> Vec a (S n) -- (:) (++) :: Vec a n -> Vec a m -> Vec a (n :+: m) VNil ++ ys = ys VCons x xs ++ y = VCons x (xs ++ y)
As long as we have length information, them we can build
safeHead :: Vec a (S n) -> a safeHead (VCons x _) = x safeTail :: Vec a (S n) -> Vec a n safteTail (VCons _ xs) = xs
Vec a (S n) says that the input vector cannot be empty, so these two functions are total functions.
We can define subtraction/maximum/minimum type operator and then some other utility function of
Vector in similar ways.
Give priorities to type operators to save some brackets later.
infixl 2 === infixl 4 :+: infixr 4 :-: infixl 5 :*:
Proof Simple Theorem now!
Haskell doesn’t have
Prop, so we need to describe “Equal” from scratch.
Start with defining the type which means two
data Equal :: * -> * -> * where EqZ :: Equal Z Z -- 0 == 0 EqS :: Equal n m -> Equal (S n) (S m) -- n == m => (n+1) == (m+1) infixl 2 === -- priority 2 type x === y = Equal x y -- give Equal x y a shorter name
Now prove that
Equal is an equivalence relationship.
ref :: Nat n -> n === n ref Zero = EqZ ref (Succ n) = EqS (refl n)
sym :: n === m -> m === n sym EqZ = EqZ sym (EqS eq) = EqS (sym eq)
infixl 3 <=> -- priority 3 (<=>) :: a === b -> b === c -> a === c EqZ <=> EqZ = EqZ EqS eq1 <=> EqS eq2 = EqS (eq1 <=> eq2)
Associativity of Addition
plusComb :: Nat n -> Nat m -> Nat p -> n :+: (m :+: p) === n :+: m :+: p
Commutativity of Addition
plusCommutes :: Nat n -> Nat m -> n :+: m === m :+: n
Commutativity is harder, but I give an idea here.
First prove the case that
m = 0
plusZero :: Nat a -> Z :+: a === a :+: Z
And prove a lemma that
rightS :: Nat a -> Nat b -> S a :+: b === a :+: S b
Then use the lemma to prove the theorem.
Or it also can be done without the lemma.
Commutativity of multiplication
Here comes the multiplication.
The idea is almost the same, but need more lemmas, e.g.:
multCommuteS :: Nat n -> Nat m -> m :*: S n === m :+: m :*: n plusSwap :: Nat a -> Nat b -> Nat c -> a :+: (b :+: c) === b :+: (a :+: c)
The proof would look like this:
equalPlus :: Nat a -> Nat b -> a === b -> Nat c -> a :+: c === b :+: c equalPlus a b eq Zero = symm (nPlusZero a) <=> eq <=> nPlusZero b equalPlus a b eq (Succ c) = nPlusSm a c <=> Fuck (equalPlus a b eq c) <=> symm (nPlusSm b c) equalPlus' :: Nat a -> Nat b -> a === b -> Nat c -> c :+: a === c :+: b equalPlus' a b eq c = plusCommutes c a <=> equalPlus a b eq c <=> plusCommutes b c plusSwap' :: Nat a -> Nat b -> Nat c -> a :+: b :+: c === b :+: a :+: c plusSwap' a b = equalPlus (a + b) (b + a) (plusCommutes a b) plusSwap :: Nat a -> Nat b -> Nat c -> a :+: (b :+: c) === b :+: (a :+: c) plusSwap a b c = plusCommute a b c <=> plusSwap' a b c <=> symm (plusCommute b a c) multCommuteS_1 :: Nat n -> Nat m -> n :+: (m :*: S n) === m :+: (n :+: (m :*: n)) multCommuteS_1 n m = equalPlus' (m * Succ n) (m + m * n) (multCommuteS n m) n <=> plusSwap n m (m * n) multCommuteS :: Nat n -> Nat m -> m :*: S n === m :+: m :*: n multCommuteS _ Zero = Refl multCommuteS n (Succ m) = Fuck $ multCommuteS_1 n m multCommutes :: Nat n -> Nat m -> n :*: m === m :*: n multCommutes Zero m = symm $ multNZero m multCommutes (Succ n) m = symm (multCommuteS n m <=> equalPlus' (m * n) (n * m) (multCommutes m n) m)
Beyond the Naturals
We have just described the “Equal” of Naturals, but how to describe “Equal” of any value?
data Equal :: * -> * -> * where Refl :: Equal a a Derive :: Equal a b -> Equal (p a) (p b)
Refl corresponds to
Derive corresponds to
EqS. From the definition,
Refl is reflexivity.
sym ‘s definition is similar to before, but the proof of transitivity needs to be modified.
(<=>) :: a === b -> b === c -> a === c Refl <=> Refl = Refl Derive x <=> Refl = Derive $ x <=> Refl Refl <=> Derive y = Derive $ Refl <=> y Derive x <=> Derive y = Derive $ x <=> y
We can try another data to see how the new
Bool in type.
data T data F
and corresponded value
data Boolean :: * -> * where Tr :: Boolean T Fa :: Boolean F
Then we need negate, or , and in type.
type family Inv (n :: *) :: * type instance Inv T = F type instance Inv F = T type family (||) (n :: *) (m :: *) :: * type instance T || T = T type instance F || T = T type instance T || F = T type instance F || F = F type family (&&) (n :: *) (m :: *) :: * type instance T && T = T type instance T && F = F type instance F && T = F type instance F && F = F
first prove double negation
doubleNeg :: Boolean b -> Inv (Inv b) === b doubleNeg Tr = Refl doubleNeg Fa = Refl
Then De Morgan’s Rule
demorgan :: Boolean a -> Boolean b -> Inv (a && b) === Inv a || Inv b demorgan Tr Tr = Refl demorgan Tr Fa = Refl demorgan Fa Tr = Refl demorgan Fa Fa = Refl
Similarly, we can prove some properties of Naturals by type families, e.g. parity.
type family IsOdd (n :: *) :: * type instance IsOdd Z = F type instance IsOdd (S Z) = T type instance IsOdd (S (S n)) = IsOdd n type family IsEven (n :: *) :: * type instance IsEven Z = T type instance IsEven (S Z) = F type instance IsEven (S (S n)) = IsEven n
Other ways to describe Property
Equal to describe that two types equal, in the same way, we can describe some other relationships, e.g.
another way of describing parity:
data Even :: * -> * where ZeroEven :: Even Z Add2Even :: Even n -> Even (S (S n)) data Odd :: * -> * where OneOdd :: Odd (S Z) Add2Odd :: Odd n -> Odd (S (S n))
or x > y?
data Greater :: * -> * where GreZ :: Greater (S Z) Z GreS1 :: Greater x y -> Greater (S x) y GreS2 :: Greater x y -> Greater (S x) (S y)