Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Types and Programming Languages. Chapter 20. Recursive Types - 20.1. Examples
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.