A compile-time prime checker for the Glorious Glasgow Haskell Compilation System

MetaPrime.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE UndecidableInstances #-}

-- Booleans
data F
data T

-- Nonnegative integers
data Zero
data Succ n

-- Lists
data Nil
data Cons x xs

-- Read: "And is a function that takes values p and q and produces a value r"
class And p q r | p q -> r
instance And F q F    -- False && q = False
instance And T q q    -- True  && q = q

class IfThenElse b x y z | b x y -> z
instance IfThenElse F x y y
instance IfThenElse T x y x

-- Okay, now we have more than two values to match, so we need to recurse.
-- Notice that x+1 >= y+1 exactly when x >= y.
-- Read: "Where x is no less than y, x+1 is no less than y+1"
class NoLessThan x y b | x y -> b
instance NoLessThan x Zero T
instance NoLessThan Zero (Succ y) F
instance (NoLessThan x y b) => NoLessThan (Succ x) (Succ y) b

class Equals x y b | x y -> b
instance Equals Zero Zero T
instance Equals Zero (Succ y) F
instance Equals (Succ x) Zero F
instance (Equals x y b) => Equals (Succ x) (Succ y) b

class Minus x y z | x y -> z
instance Minus x Zero x
instance Minus Zero (Succ y) Zero
instance (Minus x y z) => Minus (Succ x) (Succ y) z

-- Two options for matching the divisor. Zero, or nonzero.
-- Everything divides zero.
-- x divides y+1 exactly when the following hold:
--   x <= y+1
--   x divides y+1-x
class Divides x y b | x y -> b
instance Divides x Zero T
instance (NoLessThan (Succ y) x p, Minus (Succ y) x z, Divides x z q, And p q b) => Divides x (Succ y) b

-- Now we're getting into lists. This "function", given n, produces the range [n,n-1..1].
-- Pretty straightforward recursion: Range Zero = Nil, Range (S x) = Cons (S x) (Range x)
class Range n xs | n -> xs
instance Range Zero Nil
instance (Range n xs) => Range (Succ n) (Cons (Succ n) xs)

-- Apply a function f represented as a value rather than as a typeclass.
class Apply f x y | f x -> y

-- flip Divides, partially applied to one argument.
-- Apply (Divides' n) m is equivalent to Divides m n
data Divides' n
instance (Divides m n b) => Apply (Divides' n) m b

-- Count the values in xs that yield T under the predicate f.
-- Exercise for the reader: Make sense of this one.
class CountIf f xs n | f xs -> n
instance CountIf f Nil Zero
instance (Apply f x b, CountIf f xs m, IfThenElse b (Succ m) m n) => CountIf f (Cons x xs) n

-- For clarity
type Two = Succ (Succ Zero)

-- n is prime iff exactly two numbers in the range [n,n-1..1] divide n.
class IsPrime n b | n -> b
instance (Range n xs, CountIf (Divides' n) xs m, Equals Two m b) => IsPrime n b


-- And now, a test suite.
-- Everything happens at compile time, so if the code compiles, the tests pass.
-- Try it out yourself! Change a T to F or a F to T, then recompile.

type One = Succ Zero
class IsOnePrime b | -> b where
    isOnePrime :: b
    isOnePrime = undefined
instance (IsPrime One b) => IsOnePrime b
testOne = isOnePrime :: F

-- type Two = Succ One
-- Already defined above
class IsTwoPrime b | -> b where
    isTwoPrime :: b
    isTwoPrime = undefined
instance (IsPrime Two b) => IsTwoPrime b
testTwo = isTwoPrime :: T

type Three = Succ Two
class IsThreePrime b | -> b where
    isThreePrime :: b
    isThreePrime = undefined
instance (IsPrime Three b) => IsThreePrime b
testThree = isThreePrime :: T

type Four = Succ Three
class IsFourPrime b | -> b where
    isFourPrime :: b
    isFourPrime = undefined
instance (IsPrime Four b) => IsFourPrime b
testFour = isFourPrime :: F

type Five = Succ Four
class IsFivePrime b | -> b where
    isFivePrime :: b
    isFivePrime = undefined
instance (IsPrime Five b) => IsFivePrime b
testFive = isFivePrime :: T

type Six = Succ Five
class IsSixPrime b | -> b where
    isSixPrime :: b
    isSixPrime = undefined
instance (IsPrime Six b) => IsSixPrime b
testSix = isSixPrime :: F

type Seven = Succ Six
class IsSevenPrime b | -> b where
    isSevenPrime :: b
    isSevenPrime = undefined
instance (IsPrime Seven b) => IsSevenPrime b
testSeven = isSevenPrime :: T

type Eight = Succ Seven
class IsEightPrime b | -> b where
    isEightPrime :: b
    isEightPrime = undefined
instance (IsPrime Eight b) => IsEightPrime b
testEight = isEightPrime :: F

type Nine = Succ Eight
class IsNinePrime b | -> b where
    isNinePrime :: b
    isNinePrime = undefined
instance (IsPrime Nine b) => IsNinePrime b
testNine = isNinePrime :: F

type Ten = Succ Nine
class IsTenPrime b | -> b where
    isTenPrime :: b
    isTenPrime = undefined
instance (IsPrime Ten b) => IsTenPrime b
testTen = isTenPrime :: F

type Eleven = Succ Ten
class IsElevenPrime b | -> b where
    isElevenPrime :: b
    isElevenPrime = undefined
instance (IsPrime Eleven b) => IsElevenPrime b
testEleven = isElevenPrime :: T

type Twelve = Succ Eleven
class IsTwelvePrime b | -> b where
    isTwelvePrime :: b
    isTwelvePrime = undefined
instance (IsPrime Twelve b) => IsTwelvePrime b
testTwelve = isTwelvePrime :: F

type Thirteen = Succ Twelve
class IsThirteenPrime b | -> b where
    isThirteenPrime :: b
    isThirteenPrime = undefined
instance (IsPrime Thirteen b) => IsThirteenPrime b
testThirteen = isThirteenPrime :: T

type Fourteen = Succ Thirteen
class IsFourteenPrime b | -> b where
    isFourteenPrime :: b
    isFourteenPrime = undefined
instance (IsPrime Fourteen b) => IsFourteenPrime b
testFourteen = isFourteenPrime :: F

type Fifteen = Succ Fourteen
class IsFifteenPrime b | -> b where
    isFifteenPrime :: b
    isFifteenPrime = undefined
instance (IsPrime Fifteen b) => IsFifteenPrime b
testFifteen = isFifteenPrime :: F

type Sixteen = Succ Fifteen
class IsSixteenPrime b | -> b where
    isSixteenPrime :: b
    isSixteenPrime = undefined
instance (IsPrime Sixteen b) => IsSixteenPrime b
testSixteen = isSixteenPrime :: F

type Seventeen = Succ Sixteen
class IsSeventeenPrime b | -> b where
    isSeventeenPrime :: b
    isSeventeenPrime = undefined
instance (IsPrime Seventeen b) => IsSeventeenPrime b
testSeventeen = isSeventeenPrime :: T

type Eighteen = Succ Seventeen
class IsEighteenPrime b | -> b where
    isEighteenPrime :: b
    isEighteenPrime = undefined
instance (IsPrime Eighteen b) => IsEighteenPrime b
testEighteen = isEighteenPrime :: F

type Nineteen = Succ Eighteen
class IsNineteenPrime b | -> b where
    isNineteenPrime :: b
    isNineteenPrime = undefined
instance (IsPrime Nineteen b) => IsNineteenPrime b
testNineteen = isNineteenPrime :: T

type Twenty = Succ Nineteen
class IsTwentyPrime b | -> b where
    isTwentyPrime :: b
    isTwentyPrime = undefined
instance (IsPrime Twenty b) => IsTwentyPrime b
testTwenty = isTwentyPrime :: F