{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# GHC_OPTIONS -fcontext-stack400 #-}
module Multi where

import Prelude hiding (sum)

{-
Suppose we want to define n-ary sum.

We might define a family of functions:

Sum[0]   = Int
Sum[n+1] = Int -> Sum[n]

sum[n]  :: Sum[n]
sum[n]   = sum'[n] 0 where

sum'[n]      :: Integer -> Sum[n]
sum'[0]   acc = acc
sum'[n+1] acc = \x -> sum[n] (x + acc)

What are their types?

Sum is a family of types -- even more, it's a function from
nat -> types in this family:
-}

-- We need Peano numerals:
data Z   = Z
data S n = S n

class Sum nat x | nat -> x where
  sumacc          :: nat -> Integer -> x

instance Sum Z Integer where
  sumacc Z acc     = acc

instance Sum nat x => Sum (S nat) (Integer -> x) where
  sumacc (S n) acc = \x -> sumacc n (acc + x)

sum  :: Sum nat x => nat -> x
sum n = sumacc n 0

-- we don't even need the values:
class Sum' nat x | nat -> x where
  sumacc'      :: nat -> Integer -> x
instance Sum' Z Integer where
  sumacc' _ acc = acc
instance Sum' nat x => Sum' (S nat) (Integer -> x) where
  sumacc' _ acc = \x -> sumacc' (bot::nat) (acc + x)

sum' (_::t) = sumacc' (bot::t) 0
bot = bot

{-
Prolog:
add(zero, B, B).
add(succ(A), B, C) :- add(A, succ(B), C).

mul(zero, A, zero).
mul(succ(A), B, C) :- mul(A, B, D), add(B, D, C).

These are Horn-clause programs.  The class declaration provides
a declaration and "type" for the predicate, and the fundeps are
in/out modes.
-}

class Add a b c | a b -> c where
  (/+/)    :: a -> b -> c
instance Add Z a a where
  Z /+/ n   = n
instance Add a b c => Add (S a) b (S c) where
  S a /+/ b = S (a /+/ b)

class Mul a b c | a b -> c where
  (/*/)    :: a -> b -> c
instance Mul Z a Z where
  Z /*/ _   = Z
instance (Mul a b ab, Add b ab c) => Mul (S a) b c where
  S a /*/ b =  b /+/ (a /*/ b)

class Reify x f r | f -> r where
  reify      :: f -> r -> x -> r
instance Reify Z (r -> r) r where
  reify f r _ = r
instance Reify n (r -> r) r => Reify (S n) (r -> r) r  where
  reify f r _ = f (reify f r (bot::n))

toNum :: (Num a, Reify x (a -> a) a) => x -> a
toNum  = reify (+1) 0

class Add' a b c | a b -> c where
  (/++/) :: a -> b -> c
  (/++/)  = bot
instance Add' Z a a where
instance Add' a b c => Add' (S a) b (S c) where

class Mul' a b c | a b -> c where
  (/**/) :: a -> b -> c
  (/**/)  = bot
instance Mul' Z a Z where
instance (Mul' a b ab, Add' b ab c) => Mul' (S a) b c where

class Fact a b | a -> b where
  fact :: a -> b
  fact  = bot
instance Fact Z (S Z) where
instance (Fact a c, Mul' (S a) c b) => Fact (S a) b where

p0  = Z
p1  = S p0
p2  = S p1
p3  = S p2
p4  = S p3
p5  = S p4
p20 = p4 /**/ p5

-- Now I can "conveniently" make a nine-place sum:
sum9'  = sum' (S (S (S Z)) /**/ S (S (S Z)))
sum9'' = sum' (S (S (S (S (S (S (S (S (S Z)))))))))

class FoldN nat a r x | nat a r -> x where
  foldlN, foldrN :: nat -> (a -> r -> r) -> r -> x
  foldrNk        :: nat -> (a -> r -> r) -> r -> (r -> r) -> x
  foldrN n f z    = foldrNk n f z id
instance FoldN Z a r r where
  foldlN  _ _  r    = r
  foldrNk _ _  z k  = k z
instance FoldN nat a r x => FoldN (S nat) a r (a -> x) where
  foldlN  _ f z   a = foldlN  (bot::nat) f (f a z)
  foldrNk _ f z k a = foldrNk (bot::nat) f z (\r -> k (f a r))

sumN n     = foldlN n (+) 0
prodN n    = foldlN n (*) 1
reverseN n = foldlN n (:) []

-- How would we write listN?  We need foldrN
listN n    = foldrN n (:) []

-- Extensible printf -- cool.  Uses accumulator like foldrNk.

-- now zipWithN:
class ZWH nat a x | nat a -> x where
  zwh         :: nat -> a -> x
instance ZWH Z [a] [a] where
  zwh _ lst    = lst
instance ZWH n [b] x => ZWH (S n) [a -> b] ([a] -> x) where
  zwh _ l1 l2  = zwh (bot::n) (zipWith ($) l1 l2)

zipWithN n f = zwh n (repeat f)

n1 = zipWithN p1 (+2) [1,2,3,4]
n2 = zipWithN p2 (+)  [1,2,3,4] [50,40,30,20]
n3 = zipWithN p3 (,,) [True, False, False] ['a', 'c', 'e'] [6,7,8]
n4 = zipWithN p4 (reverseN p4) [1,2,3,4] [5,6,7,8] [9,10,11,12] [13,14,15,16]

-- Do we need N?  Not if we're willing to specify write a type:
class ZWA a x | x -> a where
  zwa       :: a -> x
instance ZWA [a] [a] where
  zwa lst    = lst
instance ZWA [b] (c x) => ZWA [a -> b] ([a] -> c x) where
  zwa l1 l2  = zwa (zipWith ($) l1 l2)

zipWithA f = zwa (repeat f)

a1, a2 :: [Bool]
a3 :: [(Bool, Char, Ordering)]
a4 :: [[Integer]]
a1 = zipWithA not [True, False, False, True]
a2 = zipWithA (&&) [True, True, False] [True, False, False]
a3 = zipWithA (,,) [True, False, False] ['a', 'c', 'e'] [EQ, LT, LT]
a4 = zipWithA (reverseN p4) [1,2,3,4] [5,6,7,8] [9,10,11,12] [13,14,15,16]

a5 = concat (zipWithA (:) "ABCD" ["bcd", "cde", "def", "efg"])