Types and Programming Languages. Chapter 20. Recursive Types - 20.1. Examples

recursive.hs

{-# LANGUAGE ScopedTypeVariables #-}

type Nat = Int

----------------------------------------
-- Lists
----------------------------------------

data NatList = Nil () | Cons (Nat, NatList)
  deriving (Eq, Show)

nil :: NatList
nil = Nil ()

cons :: Nat -> NatList -> NatList
cons = \n -> \l -> Cons (n, l)

isnil :: NatList -> Bool
isnil = \l -> case l of
                Nil _ -> True
                Cons _ -> False

hd :: NatList -> Nat
hd = \l -> case l of
             Nil _ -> 0
             Cons p -> fst p

tl :: NatList -> NatList
tl = \l -> case l of
             Nil _ -> l
             Cons p -> snd p

sumlist :: NatList -> Nat
sumlist = \l -> if isnil l then 0 else hd l + sumlist (tl l)

-- main = let mylist = cons 2 (cons 3 (cons 5 nil)) in print $ sumlist mylist

----------------------------------------
-- Hungry Functions
----------------------------------------

data Hungry = Hungry (Nat -> Hungry)

-- hungry = \(Hungry n) -> hungry

-- variable-length argument function:
-- http://d.hatena.ne.jp/goth_wrist_cut/20081204/1228374214

----------------------------------------
-- Streams
----------------------------------------

data Stream a = Stream (() -> (Nat, Stream a))

hd_s :: Stream Nat -> Nat
hd_s = \(Stream s) -> fst (s ())

tl_s :: Stream Nat -> Stream Nat
tl_s = \(Stream s) -> snd (s ())

upfrom0 :: Stream Int
upfrom0 = f 0
  where
    f n = Stream (\_ -> (n, f (n+1)))

-- main = print $ hd_s (tl_s (tl_s upfrom0))

----------------------------------------
-- Processes
----------------------------------------

data Process a = Process (Nat -> (Nat, Process a))

curr :: Process a -> Nat
curr = \(Process s) -> fst (s 0)

send :: Nat -> Process a -> Process a
send = \n -> \(Process s) -> snd (s n)

process :: Process a
process = f 0
  where
    f acc = Process (\n -> (acc+n, f (acc+n)))

-- main = print $ curr (send 20 (send 3 (send 5 process)))

----------------------------------------
-- Objects
----------------------------------------

data Counter = Counter
  { get :: Nat,
    inc :: () -> Counter,
    dec :: () -> Counter
  }
data X = X { x :: Nat }

counter :: Counter
counter = create $ X { x = 0 }
  where
    create s = Counter {
      get = x s,
      inc = \_ -> create $ X { x = x s + 1 },
      dec = \_ -> create $ X { x = x s - 1 }
    }

-- main = let c1 = (inc counter) ()
--            c2 = (inc c1) ()
--        in print $ get c2

----------------------------------------
-- Recursive Values from Recursive Types
----------------------------------------

-- Fun t a = \mu a. a -> t
data Fun t a = Fun (Fun t a -> t)

-- fix :: (t -> t) -> (Fun t a -> t)
-- fix = \(f :: t -> t) -> (\(x :: Fun t a) -> f $ x x) (\(x :: Fun t a) -> f $ x x)