We show invertible, terminating, 3-place addition, multiplication, and exponentiation relations on type-level Peano numerals, where _any_ two operands determine the third. We also show the invertible factorial relation. This gives us all common arithmetic operations on Peano numerals, including n-base discrete logarithm, n-th root, and the inverse of factorial. The inverting method can work with any representation of (type-level) numerals, binary or decimal. Furthermore, the inverter itself is generic: it is a type-class function, that is, a type-class parameterized by the type-class to `invert'. There has been a proposal on Haskell' to give equal rights to types and classes. In Haskell98+multi-parameter type classes, classes are already first-class, for all practical purposes. We can quite easily define (potentially, higher-order) type functions on type classes. Ashley Yakeley wrote: ] I know for the usual Peano representation of natural numbers, at least, ] it's possible to represent addition and subtraction with a single class ] with two fundeps (because classes represent relations between types ] rather than functions on them). That can be done even for decimal type numerals, cf. number-parameterized-types paper. But we can do better: we can have _three_ functional dependencies, so that any two operands of the type class determine the third. The key insight was the result of a conversation with Chung-chieh Shan and Gregory Price in the evening of Nov 10, 2003. Despite what the extension says, the arithmetic relations in this file are all decidable.

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}

module PeanoArithm where

data Z data S a __ = __

First we define a semi-sum relation, with only two functional dependencies:

class Sum2 a b c | a b -> c, a c -> b instance Sum2 Z a a instance Sum2 a b c => Sum2 (S a) b (S c)

Now we add the third dependency. It is that simple.

class Sum a b c | a b -> c, a c -> b, b c -> a instance (Sum2 a b c, Sum2 b a c) => Sum a b c

After defining a few numbers,

add:: Sum a b c => a -> b -> c add = __

type One = S Z type Two = S (S Z)

zero = __ :: Z one = __ :: One two = __ :: Two three = add one two n4 = add two two

we see that the typechecker can indeed add and subtract:

ta1 = \x -> (add three x `asTypeOf` three) ta2 = \x -> (add x two `asTypeOf` three) -- ta3 = \x -> (add three x `asTypeOf` two) -- fails

*PeanoArithm> :t ta1 ta1 :: Z -> S (S (S Z)) *PeanoArithm> :t ta2 ta2 :: S Z -> S (S (S Z)) Before we move to products, we introduce a few utilities

class NLE x y instance Sum2 x a y => NLE x y

class Mul a b c | a b -> c -- a single-dependency multiplication instance Mul Z b Z instance (Mul a b c', Sum c' b c) => Mul (S a) b c -- (a+1)*b = a*b + b

The relation |NLE x y| holds if |x| is less or equal to |y|, that is, there exists a numeral |a| that in sum with |x| gives |y|. We now introduce the generic inverter of an arithmetic function defined on the whole set of natural numbers. The inverter is parameterized by the numeric function (that is, a type class) to invert. We define the type of these classes by the following class. It maps types to classes (see also the HList paper):

class Registry clas a b c | clas a b -> c

The inverter, the type-class function, is so trivial that I'm ashamed to discuss it. It is a simple for-loop.

class Inv clas init limit a b c | clas init a b -> c instance (NLE x limit, Registry clas x b a', Sum2 a' r a, Inv' r clas x limit a b c) => Inv clas x limit a b c class Inv' r clas x limit a b c | r clas x a b -> c instance Inv' Z clas x limit a b x -- Found it instance Inv clas (S x) limit a b c -- try next x => Inv' (S r) clas x limit a b c

Division is defined as an inverse of multiplication:

data RegMul instance Mul a b c => Registry RegMul a b c

class Div m n q | m n -> q -- m = n * q instance Inv RegMul Z m m n q => Div m n q

We partially apply Inv to the right operands, and get the Div relation in return.

pdiv :: Div a b c => a -> b -> c pdiv = __

-- Only where all dependencies exist... class Product a b c | a b -> c, a c -> b, b c -> a instance (Mul a b c, Div c b a, Div c a b) => Product a b c

prod:: Product a b c => a -> b -> c prod = __

Now the typechecker can multiply and divide

n6 = prod two three tm1 = \x -> (prod three x `asTypeOf` n6) tm2 = \x -> (prod x two `asTypeOf` n6) -- tm3 = \x -> (prod x n4 `asTypeOf` n6) tm4 = \x -> (prod x n6 `asTypeOf` n6) -- tm5 = \x -> (prod x zero `asTypeOf` n6) tm6 = \x -> (prod x zero `asTypeOf` zero)

The inferred types are tm1 :: S (S Z) -> S (S (S (S (S (S Z))))) tm2 :: S (S (S Z)) -> S (S (S (S (S (S Z))))) tm4 :: S Z -> S (S (S (S (S (S Z))))) The commented-out tests raise type errors. The exponentiation is trivial:

class Raise b e c | b e -> c -- c = b ^ e instance Raise a Z (S Z) instance (Raise b e c', Mul b c' c) => Raise b (S e) c

The logarithm and the n-th root are two inverses of (partially-applied) exponentiation. It takes a couple of lines to define each

data RegRaiseI instance Raise b a c => Registry RegRaiseI a b c

class Log n b e | n b -> e -- e = log_b n instance Inv RegRaiseI Z n n b e => Log n b e

data RegRaise instance Raise a b c => Registry RegRaise a b c

class Root a b c | a b -> c -- c = b-th root of a instance Inv RegRaise Z a a b c => Root a b c

We introduce the full exponentiation relation

class Exp b e c | b e -> c, b c -> e, e c -> b instance (Raise b e c, Log c b e, Root c e b) => Exp b e c

pexp:: Exp a b c => a -> b -> c pexp = __

and test it

n8 = add n4 n4 n9 = prod three three te1 = pexp three two te2 = \x -> (pexp two x `asTypeOf` (add n8 n8)) te3 = \x -> (pexp x three `asTypeOf` n8) -- te4 = \x -> (pexp x three `asTypeOf` n6) te5 = \x -> (pexp three x `asTypeOf` three)

*PeanoArithm> :t te2 te2 :: S (S (S (S Z))) -> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))) *PeanoArithm> :t te3 te3 :: S (S Z) -> S (S (S (S (S (S (S (S Z))))))) Indeed, 4 is the binary logarithm of 16, and two is the cubic root of 8. Having gone that far, it is impossible to avoid factorial and its inverse (as an evidence of further evolution of the Haskell programmer)

class FactF a b | a -> b instance FactF Z (S Z) instance (FactF a b', Mul (S a) b' b) => FactF (S a) b

data RegFact instance FactF a c => Registry RegFact a b c

class FactR a c | a -> c -- Inverse of Fact instance Inv RegFact (S Z) a a Z c => FactR a c

class Fact a b | a -> b, b -> a instance (FactF a b, FactR b a) => Fact a b

fact :: Fact a b => a -> b fact = __

-- :t fact n4 *PeanoArithm> :t \x -> (fact x `asTypeOf` (prod n4 n6)) \x -> (fact x `asTypeOf` (prod n4 n6)) :: S (S (S (S Z))) -> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))))))))))) Indeed, 4 is the inverse factorial of 24. It took only a split second. The practical outcome of this exercise is the creation of a benchmark suite for Haskell typecheckers, e.g., computing the inverse factorial of 720. Perhaps there should be a shoot-out entry for the speed of typechecking. The implementation of RSA on type level is left for future work.