107 lines
2.8 KiB
Haskell
107 lines
2.8 KiB
Haskell
{-# OPTIONS_GHC -XNPlusKPatterns #-}
|
|
|
|
-- (c) MP-I (1998/9-2006/7) and CP (2005/6-2022/23)
|
|
|
|
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 -------------------------------------------------------
|
|
|
|
recNat f = id -|- f -- this is F f for this datatype
|
|
|
|
cataNat g = g . recNat (cataNat g) . outNat
|
|
|
|
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 ----------------------------------------------------------------
|
|
|
|
-- (4.1) for is the "fold" of natural numbers
|
|
|
|
for b i = cataNat (either (const i) b)
|
|
|
|
somar a = cataNat (either (const a) succ) -- for succ a
|
|
|
|
multip a = cataNat (either (const 0) (a+)) -- for (a+) 0
|
|
|
|
exp a = cataNat (either (const 1) (a*)) -- for (a*) 1
|
|
|
|
-- (4.2) 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)
|
|
|
|
-- (4.3) 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
|
|
|
|
-- (4.4) integer division as an anamorphism --------------
|
|
|
|
idiv :: Integer -> Integer -> Integer
|
|
{-- pointwise
|
|
x `idiv` y | x < y = 0
|
|
| x >= y = (x - y) `idiv` y + 1
|
|
--}
|
|
|
|
idiv = flip aux
|
|
|
|
aux y = anaNat divide where
|
|
divide x | x < y = i1 ()
|
|
| x >= y = i2 (x - y)
|
|
|
|
--- (4.5) bubble sort -----------------------------------
|
|
|
|
bSort xs = for bubble xs (length xs) where
|
|
bubble (x:y:xs)
|
|
| x > y = y : bubble (x:xs)
|
|
| otherwise = x : bubble (y:xs)
|
|
bubble x = x
|
|
|
|
--- (5) While loop -------------------------------------
|
|
|
|
{-- pointwise
|
|
|
|
while p f x | not (p x) = x
|
|
| otherwise = while p f (f x)
|
|
--}
|
|
|
|
while :: (a -> Bool) -> (a -> a) -> a -> a
|
|
while p f = w where w = (either id id) . (w -|- id) . (f -|- id) . (grd p)
|
|
|
|
--- (5) Monadic for -------------------------------------
|
|
|
|
mfor b i 0 = i
|
|
mfor b i (n+1) = do {x <- mfor b i n ; b x}
|
|
|
|
--- end of Nat.hs ----------------------------------------
|