Conor McBride was not joking when he and his co-author entitled their paper about dependent typing in Haskell “Hasochism”: Lindley and McBride (2013).
In trying to resurrect the Haskell package yarr, it seemed that a dependently typed reverse function needed to be written. Writing such a function turns out to be far from straightforward. How GHC determines that a proof (program) discharges a proposition (type signature) is rather opaque and perhaps not surprisingly the error messages one gets if the proof is incorrect are far from easy to interpret.
I’d like to thank all the folk on StackOverflow whose answers and comments I have used freely below. Needless to say, any errors are entirely mine.
Here are two implementations, each starting from different axioms (NB: I have never seen type families referred to as axioms but it seems helpful to think about them in this way).
> {-# OPTIONS_GHC -Wall #-}
> {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
> {-# OPTIONS_GHC -fno-warn-type-defaults #-}
> {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
> {-# OPTIONS_GHC -fno-warn-missing-methods #-}
> {-# OPTIONS_GHC -fno-warn-orphans #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE ExplicitForAll #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE ScopedTypeVariables #-}
For both implementations, we need propositional equality: if a :~: b
is inhabited by some terminating value, then the type a
is the same as the type b
. Further we need the normal form of an equality proof: Refl :: a :~: a
and a function, gcastWith
which allows us to use internal equality (:~:)
to discharge a required proof of external equality (~)
. Readers familiar with topos theory, for example see Lambek and Scott (1988), will note that the notation is reversed.
> import Data.Type.Equality ( (:~:) (Refl), gcastWith )
For the second of the two approaches adumbrated we will need
> import Data.Proxy
The usual natural numbers:
> data Nat = Z | S Nat
We need some axioms:
- A left unit and
- Restricted commutativity.
> type family (n :: Nat) :+ (m :: Nat) :: Nat where
> Z :+ m = m
> S n :+ m = n :+ S m
We need the usual singleton for Nat
to tie types and terms together.
> data SNat :: Nat -> * where
> SZero :: SNat Z
> SSucc :: SNat n -> SNat (S n)
Now we can prove some lemmas.
First a lemma showing we can push :+
inside a successor, S
.
> succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
> succ_plus_id SZero _ = Refl
> succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl
This looks nothing like a standard mathematical proof and it’s hard to know what ghc is doing under the covers but presumably something like this:
- For
SZero
S Z :+ n2 = Z :+ S n2
(by axiom 2) =S n2
(by axiom 1) andS (Z + n2) = S n2
(by axiom 1)- So
S Z :+ n2 = S (Z + n2)
- For
SSucc
SSucc n :: SNat (S k)
son :: SNat k
andm :: SNat i
soSSucc m :: SNat (S i)
succ_plus id n (SSucc m) :: k ~ S p => S p :+ S i :~: S (p :+ S i)
(by hypothesis)k ~ S p => S p :+ S i :~: S (S p :+ i)
(by axiom 2)k :+ S i :~: S (k :+ i)
(by substitution)S k :+ i :~: S (k :+ i)
(by axiom 2)
Second a lemma showing that Z
is also the right unit.
> plus_id_r :: SNat n -> ((n :+ Z) :~: n)
> plus_id_r SZero = Refl
> plus_id_r (SSucc n) = gcastWith (plus_id_r n) (succ_plus_id n SZero)
- For
SZero
Z :+ Z = Z
(by axiom 1)
- For
SSucc
SSucc n :: SNat (S k)
son :: SNat k
plus_id_r n :: k :+ Z :~: k
(by hypothesis)succ_plus_id n SZero :: S k :+ Z :~: S (k + Z)
(by thesucc_plus_id
lemma)succ_plus_id n SZero :: k :+ Z ~ k => S k :+ Z :~: S k
(by substitution)plus_id_r n :: k :+ Z :~: k
(by equation 2)
Now we can defined vectors which have their lengths encoded in their type.
> infixr 4 :::
> data Vec a n where
> Nil :: Vec a Z
> (:::) :: a -> Vec a n -> Vec a (S n)
We can prove a simple result using the lemma that Z
is a right unit.
> elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n)
> elim0 n x = gcastWith (plus_id_r n) x
Armed with this we can write an reverse function in which the length of the result is guaranteed to be the same as the length of the argument.
> size :: Vec a n -> SNat n
> size Nil = SZero
> size (_ ::: xs) = SSucc $ size xs
> accrev :: Vec a n -> Vec a n
> accrev x = elim0 (size x) $ go Nil x where
> go :: Vec a m -> Vec a n -> Vec a (n :+ m)
> go acc Nil = acc
> go acc (x ::: xs) = go (x ::: acc) xs
> toList :: Vec a n -> [a]
> toList Nil = []
> toList (x ::: xs) = x : toList xs
> test0 :: [String]
> test0 = toList $ accrev $ "a" ::: "b" ::: "c" ::: Nil
ghci> test0
["c","b","a"]
For an alternative approach, let us change the axioms slightly.
> type family (n1 :: Nat) + (n2 :: Nat) :: Nat where
> Z + n2 = n2
> (S n1) + n2 = S (n1 + n2)
Now the proof that Z
is a right unit is more straightforward.
> plus_id_r1 :: SNat n -> ((n + Z) :~: n)
> plus_id_r1 SZero = Refl
> plus_id_r1 (SSucc n) = gcastWith (plus_id_r1 n) Refl
For the lemma showing we can push +
inside a successor, S
, we can use a Proxy
.
> plus_succ_r1 :: SNat n1 -> Proxy n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
> plus_succ_r1 SZero _ = Refl
> plus_succ_r1 (SSucc n1) proxy_n2 = gcastWith (plus_succ_r1 n1 proxy_n2) Refl
Now we can write our reverse function without having to calculate sizes.
> accrev1 :: Vec a n -> Vec a n
> accrev1 Nil = Nil
> accrev1 list = go SZero Nil list
> where
> go :: SNat n1 -> Vec a n1 -> Vec a n2 -> Vec a (n1 + n2)
> go snat acc Nil = gcastWith (plus_id_r1 snat) acc
> go snat acc (h ::: (t :: Vec a n3)) =
> gcastWith (plus_succ_r1 snat (Proxy :: Proxy n3))
> (go (SSucc snat) (h ::: acc) t)
> test1 :: [String]
> test1 = toList $ accrev1 $ "a" ::: "b" ::: "c" ::: Nil
ghci> test0
["c","b","a"]
Bibliography
Lambek, J., and P.J. Scott. 1988. Introduction to Higher-Order Categorical Logic. Cambridge Studies in Advanced Mathematics. Cambridge University Press. http://books.google.co.uk/books?id=6PY_emBeGjUC.
Lindley, Sam, and Conor McBride. 2013. “Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming.” In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, 81–92. Haskell ’13. New York, NY, USA: ACM. doi:10.1145/2503778.2503786.
Type families are internally defined as type equality axioms, so it’s not a bad way of thinking about them.