{-# OPTIONS_GHC -XNPlusKPatterns #-} -- (c) MP-I (1998/9-2006/7) and CP (2005/6-2014/5) module Nat where import Cp -- (1) Datatype definition ----------------------------------------------------- -- "data Nat = 0 | succ Nat" -- in fact: Haskell Integer is used as carrier type inNat = either (const 0) succ outNat 0 = i1 () outNat (n+1) = i2 n -- NB: inNat and outNat are isomorphisms only if restricted to non-negative integers -- (2) Ana + cata + hylo ------------------------------------------------------- cataNat g = g . recNat (cataNat g) . outNat recNat f = id -|- f anaNat h = inNat . (recNat (anaNat h) ) . h hyloNat g h = cataNat g . anaNat h -- paraNat g = g . recNat (split id (paraNat g)) . outNat -- (3) Map --------------------------------------------------------------------- -- (4) Examples ---------------------------------------------------------------- for :: (Integral b) => (a -> a) -> a -> b -> a -- -- for is the "fold" of natural numbers -- for b i = cataNat (either (const i) b) somar a = cataNat (either (const a) succ) multip a = cataNat (either (const 0) (a+)) exp a = cataNat (either (const 1) (a*)) -- sq (square of a natural number) sq 0 = 0 sq (n+1) = oddn n + sq n where oddn n = 2*n+1 -- sq = paraNat (either (const 0) g)i sq' = p1 . aux -- this is the outcome of calculating sq as a for loop using the -- mutual recursion law where aux = cataNat (either (split (const 0)(const 1)) (split (uncurry (+))((2+).p2))) sq'' n = -- the same as a for loop (putting variables in) p1 (for body (0,1) n) where body(s,o) = (s+o,2+o) -- factorial fac = p2. facfor facfor = for (split (succ.p1) mul) (1,1) -- factorial = paraNat (either (const 1) g) where g(n,r) = (n+1) * r -- Integer division as an anamorphism -------------- idiv :: Integer -> Integer -> Integer {-- pointwise x `wdiv` y | x < y = 0 | x >= y = (x - y) `wdiv` y + 1 --} idiv = flip aux aux y = anaNat divide where divide x | x < y = i1 () | x >= y = i2 (x - y) --- end of Nat.hs