# Ticket #3005: TypeNats2.hs

File TypeNats2.hs, 16.8 KB (added by shelarcy, 4 months ago)
Line
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, ScopedTypeVariables #-}
2{-# LANGUAGE UndecidableInstances #-}
3{-
4 -
5 -  Copyright 2005-2006, Robert Dockins.
6 -
7 -}
8
9{- | This module defines type-level natural numbers and arithmetic operation on them
10     including addition, subtraction, multiplication, division and GCD.
11
12     Numbers are represented as a list of binary digits, terminated by a distinguished type 'Z'.
13     Least significant digits are outermost, which makes the numbers little-endian when read.
14
15     Because a binary representation is used, reasonably large numbers can be
16     represented.  I have personally done tests with numbers at the order
17     of 10^15 in GHC.  However, larger numbers require the GHC \'-fcontext-stack\' option.
18     For example, the test suite sets \'-fcontext-stack64\'.
19
20     Because of the limitations of typeclasses, some of the algorithms are pretty
21     messy.  The division algorithm is particularly ugly.  Suggestions for improvements
22     are welcome.
23 -}
24
25module TypeNats2 where
26
27-- | Terminates a list of binary digits with an imagined infinity of zeros.
28data Z
29
30-- | A zero bit.
31data O a
32
33-- | A one bit.
34data I a -- a one bit
35
36type Zero      =                 Z
37type One       =  (I             Z)
38type Two       =  (O (I          Z))
39type Three     =  (I (I          Z))
40type Four      =  (O (O (I       Z)))
41type Five      =  (I (O (I       Z)))
42type Six       =  (O (I (I       Z)))
43type Seven     =  (I (I (I       Z)))
44type Eight     =  (O (O (O (I    Z))))
45type Nine      =  (I (O (O (I    Z))))
46type Ten       =  (O (I (O (I    Z))))
47type Eleven    =  (I (I (O (I    Z))))
48type Twelve    =  (O (O (I (I    Z))))
49type Thirteen  =  (I (O (I (I    Z))))
50type Fourteen  =  (O (I (I (I    Z))))
51type Fifteen   =  (I (I (I (I    Z))))
52type Sixteen   =  (O (O (O (O (I Z)))))
53type Seventeen =  (I (O (O (O (I Z)))))
54type Eighteen  =  (O (I (O (O (I Z)))))
55type Nineteen  =  (I (I (O (O (I Z)))))
56
57type Twenty    =  (O (O (I (O (I Z)))))
58type Thirty    =  (O (I (O (I (I Z)))))
59type Fourty    =  (O (O (O (I (O (I Z))))))
60type Fifty     =  (O (I (O (O (I (I Z))))))
61type Sixty     =  (O (O (I (I (I (I Z))))))
62type Seventy   =  (O (I (I (O (O (O (I Z)))))))
63type Eighty    =  (O (O (O (O (I (O (I Z)))))))
64type Ninety    =  (O (I (O (I (I (O (I Z)))))))
65type Hundred   =  (O (O (I (O (O (I (I Z)))))))
66
67-- Hexidecimal digits
68type Ox0 a = (O (O (O (O a))))
69type Ox1 a = (I (O (O (O a))))
70type Ox2 a = (O (I (O (O a))))
71type Ox3 a = (I (I (O (O a))))
72type Ox4 a = (O (O (I (O a))))
73type Ox5 a = (I (O (I (O a))))
74type Ox6 a = (O (I (I (O a))))
75type Ox7 a = (I (I (I (O a))))
76type Ox8 a = (O (O (O (I a))))
77type Ox9 a = (I (O (O (I a))))
78type Oxa a = (O (I (O (I a))))
79type Oxb a = (I (I (O (I a))))
80type Oxc a = (O (O (I (I a))))
81type Oxd a = (I (O (I (I a))))
82type Oxe a = (O (I (I (I a))))
83type Oxf a = (I (I (I (I a))))
84
85-- some larger numbers
86type Thousand = Ox8 (Oxe (Ox3 Z))
87type Million  = Ox0 (Ox4 (Ox2 (Ox4 (Oxf Z))))
88type Billion  = Ox0 (Ox0 (Oxa (Oxc (Oxa (Ox9 (Oxb (Ox3 Z)))))))
89
90-- | The Natural class, with conversion to intergral values.
91--   The conversion should be linear in the number of bits, which
92--   is logarithmic in the magnitute of the number.
93
94class Natural a where
95  naturalToIntegral :: Integral b => a -> b
96
97instance Natural Z where
98  naturalToIntegral _ = fromInteger 0
99
100instance Natural a => Natural (O a) where
101  naturalToIntegral _ = let x = naturalToIntegral (undefined::a) in x+x
102
103instance Natural a => Natural (I a) where
104  naturalToIntegral _ = let x = naturalToIntegral (undefined::a) in succ (x+x)
105
106-- | Zero predicate.  Zero is represented by a single 'Z' or
107--   a string of 'O' terminated by 'Z'.
108class IsZero a
109instance IsZero Z
110instance IsZero a => IsZero (O a)
111
112-- | The equality relation on nats.
113class EqNat a b
114instance (IsZero a)  => EqNat a Z
115instance (EqNat Z b) => EqNat Z (O b)
116instance (EqNat a b) => EqNat (O a) (O b)
117instance (EqNat a b) => EqNat (I a) (I b)
118
119-- | The successor function; defined for all naturals.
120class (Natural a, Natural b) => NatSucc a b | a -> b
121instance                NatSucc Z (I Z)
122instance Natural a   => NatSucc (O a) (I a)
123instance NatSucc a b => NatSucc (I a) (O b)
124
125natSucc :: (NatSucc a b) => a -> b
126natSucc = undefined
127
128-- | The predecessor function; not defined for zero.
129class (Natural a, Natural b) => NatPred a b | a -> b
130instance Natural a   => NatPred (I a) (O a)
131instance NatPred a b => NatPred (O a) (I b)
132
133natPred :: NatPred a b => a -> b
134natPred = undefined
135
136
139--   Addition is defined for all pairs of natural numbers.
140
141class (Natural a,Natural b,Natural c) => Add a b c | a b -> c
143instance (Natural a)  => Add Z (O a) (O a)
144instance (Natural a)  => Add Z (I a) (I a)
145instance (Natural a)  => Add (O a) Z (O a)
146instance (Natural a)  => Add (I a) Z (I a)
147
148instance Add  a b c   => Add (O a) (O b) (O c)
149instance Add  a b c   => Add (I a) (O b) (I c)
150instance Add  a b c   => Add (O a) (I b) (I c)
151instance AddC a b c   => Add (I a) (I b) (O c)
152
153class (Natural a,Natural b,Natural c) => AddC a b c | a b -> c
154instance                 AddC Z Z (I Z)
155instance Natural a    => AddC Z (O a) (I a)
156instance NatSucc a b  => AddC Z (I a) (O b)
157instance Natural a    => AddC (O a) Z (I a)
158instance NatSucc a b  => AddC (I a) Z (O b)
159
160instance Add  a b c   => AddC (O a) (O b) (I c)
161instance AddC a b c   => AddC (I a) (O b) (O c)
162instance AddC a b c   => AddC (O a) (I b) (O c)
163instance AddC a b c   => AddC (I a) (I b) (I c)
164
165add :: Add a b c => a -> b -> c
167
168
169
170
171-- | A distinguished error type which is returned when
172--   subtraction is impossible.
173data CantSubtract
174
175
176-- | Binary subtraction. Slightly less elegant than the adder but it works.
177--   'DoSub' returns a distingushed error type if a < b and '()' if the subtraction suceeds.
178
179class (Natural a, Natural b) => Sub a b c | a b -> c
180instance DoSub a b c ()           => Sub a b c
181
182class (Natural a, Natural b) => DoSub a b c d | a b -> c d
183instance Natural a             => DoSub a Z a ()
184instance DoSub Z b c d         => DoSub Z (O b) c d  -- this rule does not loop, because
185                                                     -- the b parameter is decreasing
186instance Natural b             => DoSub Z (I b) () CantSubtract
187
188instance DoSub a b c d         => DoSub (O a) (O b) (O c) d
189instance DoSub a b c d         => DoSub (I a) (O b) (I c) d
190instance DoSub a b c d         => DoSub (I a) (I b) (O c) d
191instance SubBorrow b c a z z d => DoSub (O a) (I b) (I c) d
192
193sub :: Sub a b c => a -> b -> c
194sub = undefined
195
196-- this is tricky, we use the top level call to SubBorrow
197-- to unify the final result with z, so that is is avaliable
198-- when we want to call Sub again
199class (Natural b,Natural x) => SubBorrow b c x y z d | x z b -> c d, x -> y
200
201instance Natural b                 => SubBorrow b () Z    ()    z CantSubtract
202instance (Natural x,DoSub z b c d) => SubBorrow b c (I x) (O x) z d
203instance SubBorrow b c x y z d     => SubBorrow b c (O x) (I y) z d
204
205{-
206  how we used to do it.  This way can't return the distinguished
207  CantSubtract type when borrowing fails.  We need that distinguisged
208  type in order to do the tests we need for division and GCD
209
210  instance (Borrow a a',Sub a' b c) => Sub (O a) (I b) (I c)
211
212  class Borrow a b | a -> b
213  instance               Borrow (I a) (O a)
214  instance Borrow a b => Borrow (O a) (I b)
215-}
216
217
218class Trichotomy n m lt eq gt z | n m lt eq gt -> z
219instance (DoSub n m p a, DoSub m n q b, DoTrichotomy a b lt eq gt z) => Trichotomy n m lt eq gt z
220
221class DoTrichotomy a b lt eq gt z | a b lt eq gt -> z
222instance DoTrichotomy CantSubtract () lt eq gt lt
223instance DoTrichotomy () () lt eq gt eq
224instance DoTrichotomy () CantSubtract lt eq gt gt
225
226
227-- comparison relations on naturals, defined
228-- in terms of subtraction
229
230-- | The less-than-or-equal-to relation
231class LEqNat a b
232instance (DoSub b a c ())           => LEqNat a b
233
234-- | The greater-than-or-equal-to relation
235class GEqNat a b
236instance (DoSub a b c ())           => GEqNat a b
237
238-- | The less-than relation
239class LTNat a b
240instance (DoSub a b c CantSubtract) => LTNat a b
241
242-- | The greater-than relation
243class GTNat a b
244instance (DoSub b a c CantSubtract) => GTNat a b
245
246
247-- | Binary multiplication. This is a
248--   simple shift and add peasant multiplier.
249
250class Mul a b c | a b -> c
251instance Mul a Z Z
252instance (Mul (O a) b x)               => Mul a (O b) x
253instance (Mul (O a) b c,Add a c x)     => Mul a (I b) x
254
255mul :: Mul a b c => a -> b -> c
256mul = undefined
257
258
259
260
261-- | Division by 2.
262--   This is real easy, just throw away the outermost
263--   type constructor.
264
265class (Natural a,Natural b) => Div2 a b | a -> b
266instance                   Div2 Z Z
267instance Natural a      => Div2 (O a) a
268instance Natural a      => Div2 (I a) a
269
270div2 :: Div2 a b => a -> b
271div2 = undefined
272
273
274-- | Normalize a nat; that is, remove all leading zeros.
275
276class NatNormalize a b | a -> b
277
278instance (NatRev a Z c
279         ,NatNorm c c'
280         ,NatRev c' Z a'
281         )
282     => NatNormalize a a'
283
284class NatRev a b c | a b -> c
285instance                       NatRev Z b b
286instance NatRev a (O b) c  =>  NatRev (O a) b c
287instance NatRev a (I b) c  =>  NatRev (I a) b c
288
289class NatNorm a b | a -> b
290instance                       NatNorm Z Z
291instance                       NatNorm (I a) (I a)
292instance NatNorm a b       =>  NatNorm (O a) b
293
294
295normalize :: NatNormalize a b => a -> b
296normalize = undefined
297
298
299
300-- | A distinguished error type returned when
301--   attempting to divide by zero.
302data DivideByZero
303
304-- | Binary division and modulus. This one is suprisingly difficult to implement.
305class DivMod a d q r | a d -> q r
306instance ( NatRev a Z a'
307         , NatRev d Z d'
308         , PreDivMod a' d' (q,r)
309         ) => DivMod a d q r
310
311-- here we throw away leading zeros and test for
312-- a zero divisor
313class PreDivMod a d z | a d -> z
314instance PreDivMod  Z     d         z => PreDivMod Z     (O d) z
315instance PreDivMod  a     d         z => PreDivMod (O a) (O d) z
316instance PreDivMod  (I a) d         z => PreDivMod (I a) (O d) z
317instance PreDivMod  a     (I d)     z => PreDivMod (O a) (I d) z
318instance PreDivMod2 Z     (I d) Z Z z => PreDivMod Z     (I d) z
319instance PreDivMod2 (I a) (I d) Z Z z => PreDivMod (I a) (I d) z
320instance                                 PreDivMod a     Z     DivideByZero
321
322-- now we begin to "unreverse" until all the divisor
323-- digits are in the correct order
324class PreDivMod2 a w d r z | a w d r -> z
325instance PreDivMod2 Z w (O d) r     z => PreDivMod2 Z     (O w) d r z
326instance PreDivMod2 a w (O d) (O r) z => PreDivMod2 (O a) (O w) d r z
327instance PreDivMod2 a w (O d) (I r) z => PreDivMod2 (I a) (O w) d r z
328instance PreDivMod2 Z w (I d) r     z => PreDivMod2 Z     (I w) d r z
329instance PreDivMod2 a w (I d) (O r) z => PreDivMod2 (O a) (I w) d r z
330instance PreDivMod2 a w (I d) (I r) z => PreDivMod2 (I a) (I w) d r z
331instance DoDivMod a d Z r z           => PreDivMod2 a     Z     d r z
332
333-- now we do binary long division
334-- first we do case analysis on the
335-- remining dividend, then case analysis
336-- on the difference between the current
337-- remainder and the dividend....
338
339class DoDivMod a d q r z | a d q r -> z
340instance ( DoSub r d x err
341         , DoDivModZ err x q r z
342         ) => DoDivMod Z d q r z
343
344instance ( DoSub r d x err
345         , DoDivModO err x a d q r z
346         ) => DoDivMod (O a) d q r z
347
348instance ( DoSub r d x err
349         , DoDivModI err x a d q r z
350         ) => DoDivMod (I a) d q r z
351
352
353class DoDivModZ err x q r z | err x q r -> z
354instance DoDivModZ () Z     q r (I q,r)
355instance DoDivModZ () (O x) q r (I q,O x)
356instance DoDivModZ () (I x) q r (I q,I x)
357instance DoDivModZ CantSubtract x q r (O q,r)
358
359class DoDivModO err x a d q r z | err x a d q r -> z
360instance DoDivMod a d (I q) Z         z => DoDivModO () Z     a d q r z
361instance DoDivMod a d (I q) (O (O x)) z => DoDivModO () (O x) a d q r z
362instance DoDivMod a d (I q) (O (I x)) z => DoDivModO () (I x) a d q r z
363instance DoDivMod a d (O q) (O r)     z => DoDivModO CantSubtract x a d q r z
364
365class DoDivModI err x a d q r z | err x a d q r -> z
366instance DoDivMod a d (I q) (I Z)     z => DoDivModI () Z     a d q r z
367instance DoDivMod a d (I q) (I (O x)) z => DoDivModI () (O x) a d q r z
368instance DoDivMod a d (I q) (I (I x)) z => DoDivModI () (I x) a d q r z
369instance DoDivMod a d (O q) (I r)     z => DoDivModI CantSubtract x a d q r z
370
371
372natDivMod :: DivMod a b q r => a -> b -> (q,r)
373natDiv    :: DivMod a b q r => a -> b -> q
374natMod    :: DivMod a b q r => a -> b -> r
375
376natDivMod = undefined
377natDiv    = undefined
378natMod    = undefined
379
380
381-- | A distinguished error type returned when
382--   an attempt is made to take the GCD of 0 and 0.
383data GCDZeroZero
384
385-- | Greatest Common Divisor (GCD).
386--   Here we use the binary euclidian algorithm.
387
388--   there is a little fancy dancing to with DoGCD2
389--     in order to replace the largest argument with
390--     their difference
391
392class GCD a b c | a b -> c
393instance ( NatNormalize a a'
394         , NatNormalize b b'
395         , DoGCD a' b' c
396         )  => GCD a b c
397
398class DoGCD a b c | a b -> c
399instance                            DoGCD Z     Z     GCDZeroZero
400instance                            DoGCD (O a) Z     (O a)
401instance                            DoGCD (I a) Z     (I a)
402instance                            DoGCD Z     (O a) (O a)
403instance                            DoGCD Z     (I a) (I a)
404instance DoGCD a b c             => DoGCD (O a) (O b) (O c)
405instance DoGCD a (I b) c         => DoGCD (O a) (I b) c
406instance DoGCD (I a) b c         => DoGCD (I a) (O b) c
407
408-- in this branch we want to replace the largest argument with
409-- the absolute value of their difference.  All this nastyness
410-- is necessary to be able to figure out which one is bigger and
411-- subtract the correct way.
412
413instance (DoSub a b x1 f1
414         ,DoSub b a x2 f2
415         ,DoGCD2 x1 x2 f1 f2
416           (I a) (I b) c)        => DoGCD (I a) (I b) c
417
418
419class DoGCD2 x1 x2 f1 f2 a b c | x1 x2 f1 f2 a b -> c
420
421-- handle GCD(x,x) case.  x and y must be (possibly distinct) representations of zero
422instance (IsZero x,IsZero y)          => DoGCD2 x  y  () () a b a
423
424-- replace the larger with the difference
425instance DoGCD (O x1) b c             => DoGCD2 x1 x2 () CantSubtract a b c
426instance DoGCD a (O x2) c             => DoGCD2 x1 x2 CantSubtract () a b c
427
428
429natGCD :: GCD a b c => a -> b -> c
430natGCD = undefined
431
432
433
434-- define a bunch of useful naturals
435
436zero      :: Zero
437one       :: One
438two       :: Two
439three     :: Three
440four      :: Four
441five      :: Five
442six       :: Six
443seven     :: Seven
444eight     :: Eight
445nine      :: Nine
446ten       :: Ten
447eleven    :: Eleven
448twelve    :: Twelve
449thirteen  :: Thirteen
450fourteen  :: Fourteen
451fifteen   :: Fifteen
452sixteen   :: Sixteen
453seventeen :: Seventeen
454eighteen  :: Eighteen
455nineteen  :: Nineteen
456
457twenty    :: Add Twenty  b c => b -> c
458twenty_   :: Twenty
459thirty    :: Add Thirty  b c => b -> c
460thirty_   :: Thirty
461fourty    :: Add Fourty  b c => b -> c
462fourty_   :: Fourty
463fifty     :: Add Fifty   b c => b -> c
464fifty_    :: Fifty
465sixty     :: Add Sixty   b c => b -> c
466sixty_    :: Sixty
467seventy   :: Add Seventy b c => b -> c
468seventy_  :: Seventy
469eighty    :: Add Eighty  b c => b -> c
470eighty_   :: Eighty
471ninety    :: Add Ninety  b c => b -> c
472ninety_   :: Ninety
473
474hundred   :: (Mul Hundred  a b,Add b x y) => a -> x -> y
475thousand  :: (Mul Thousand a b,Add b x y) => a -> x -> y
476million   :: (Mul Million  a b,Add b x y) => a -> x -> y
477billion   :: (Mul Billion  a b,Add b x y) => a -> x -> y
478
479infixr 5 `billion`
480infixr 5 `million`
481infixr 5 `thousand`
482infix  6 `hundred`
483
484zero      = undefined
485one       = undefined
486two       = undefined
487three     = undefined
488four      = undefined
489five      = undefined
490six       = undefined
491seven     = undefined
492eight     = undefined
493nine      = undefined
494ten       = undefined
495eleven    = undefined
496twelve    = undefined
497thirteen  = undefined
498fourteen  = undefined
499fifteen   = undefined
500sixteen   = undefined
501seventeen = undefined
502eighteen  = undefined
503nineteen  = undefined
504
505twenty    = undefined
506thirty    = undefined
507fourty    = undefined
508fifty     = undefined
509sixty     = undefined
510seventy   = undefined
511eighty    = undefined
512ninety    = undefined
513twenty_   = undefined
514thirty_   = undefined
515fourty_   = undefined
516fifty_    = undefined
517sixty_    = undefined
518seventy_  = undefined
519eighty_   = undefined
520ninety_   = undefined
521
522hundred   = undefined
523thousand  = undefined
524million   = undefined
525billion   = undefined