a-voronov/reasonably-polymorphic-test.hs

## reasonably-polymorphic-test.hs
let swap = Tape Nil EnterLoop ( Cons MoveRight -- →
                              $ Cons EnterLoop -- [
                              $ Cons Decrement -- -
                              $ Cons MoveRight -- →
                              $ Cons Increment -- +
                              $ Cons MoveLeft  -- ←
                              $ Cons ExitLoop  -- ]
                              $ Cons MoveLeft  -- ←
                              $ Cons EnterLoop -- [
                              $ Cons Decrement -- -
                              $ Cons MoveRight -- →
                              $ Cons Increment -- +
                              $ Cons MoveLeft  -- ←
                              $ Cons ExitLoop  -- ]
                              $ Cons MoveRight -- →
                              $ Cons MoveRight -- →
                              $ Cons EnterLoop -- [
                              $ Cons Decrement -- -
                              $ Cons MoveLeft  -- ←
                              $ Cons MoveLeft  -- ←
                              $ Cons Increment -- +
                              $ Cons MoveRight -- →
                              $ Cons MoveRight -- →
                              $ Cons ExitLoop  -- ]
                              $ Cons ExitLoop  -- ]
                              $ Cons Halt      -- ¤
                              $ Nil
                              )

let tape = Tape Nil (Succ $ Succ $ Succ Zero) (Cons (Succ $ Succ Zero) $ Cons Zero Nil)
-- Tape [] 3 [2, 0]

memTape $ snd $ pipeline (P'' swap tape)
-- Tape [3, 2] 0 []

-- It swaps 3 and 2, and uses 0 as a temp var.
-- To simplify moveRight logic element is appended to the head of the list instead of end of the tail
-- And to simplify moveLeft logic element is taken from the head of the list instead of end of the tail
-- So-to-say move logic is reversed not to make it recursively append to the end and take from the end

--                                                          ↓
-- [ → [ - → + ← ] ← [ - → + ← ] → → [ - ← ← + → → ] ] ¤ : (3 2 0)
-- 3 2
--       1 0 1 1                                              ↓
--       0 1 2 0                                         : (3 0 2)
--                 3   2 0 1 2
--                     1 1 2 1                              ↓
--                     0 2 3 0                           : (0 3 2)
--                               3 2
--                                     1 3 0 1 3 1              ↓
--                                     0 3 1 2 3 0       : (2 3 0)

-- TL;DR 3 2 0 becomes 2 3 0

## reasonably-polymorphic.hs
{-# LANGUAGE TypeSynonymInstances #-}

import Debug.Trace

-- * Base

data Unit = Unit deriving Show

data Nat = Succ Nat
         | Zero

instance Show Nat where
  show n = show $ go n
    where
       go Zero = 0
       go (Succ x) = 1 + go x

data List a = Nil
            | Cons a (List a)

instance Show a => Show (List a) where
  show xs = "[" ++ go xs
    where
      go Nil          = "]"
      go (Cons x Nil) = show x ++ "]"
      go (Cons x xs)  = show x ++ ", " ++ go xs

-- * State

-- not proving State is a custom Kleisli class from the book because Haskell doesn't allow partially aplied type synonims
-- also not using do-notation as in the book, because we'd need to prove State is a Monad or Applicative
type State s a = s -> (a, s)

injectState :: a -> State s a
injectState a s = (a, s)

composeState :: (a -> s -> (b, s))
             -> (b -> s -> (c, s))
             -> a
             -> s
             -> (c, s)
composeState m1 m2 a state = (c, finalState)
  where
    (b, newState)   = m1 a state
    (c, finalState) = m2 b newState

get :: State s s
get state = (state, state)

set :: s -> State s Unit
set newState _ = (Unit, newState)

modify :: (s -> s) -> State s Unit
modify f state = set (f state) state

always :: x -> y -> x
always x _ = x

bind :: State s a
     -> (a -> State s b)
     -> State s b
bind ma f = composeState (always ma) f Unit

-- can' use >>= because of already existing monadic operator
(>>-) = bind

ignoring :: State s a
         -> State s b
         -> State s b
ignoring ma mb =        ma
              >>- \_ -> mb

-- can' use >> because of already existing monadic operator
(>>>) = ignoring

hold :: Bool -> State Bool Bool
hold val =  get
        >>- \s -> set (val || s)
        >>> get

-- * P''

data Tape a = Tape (List a) a (List a) deriving Show

class Point a where
  point :: a

readHead :: Tape a -> a
readHead (Tape _ a _) = a

-- might feel odd as it takes first element instead of last
moveLeft :: Point a => Tape a -> Tape a
moveLeft (Tape (Cons l ls) a rs) = Tape ls  l     (Cons a rs)
moveLeft (Tape Nil         a rs) = Tape Nil point (Cons a rs)

-- might feel odd as it puts element as a head instead of last
moveRight :: Point a => Tape a -> Tape a
moveRight (Tape ls a (Cons r rs)) = Tape (Cons a ls) r     rs
moveRight (Tape ls a Nil)         = Tape (Cons a ls) point Nil

data Instr = MoveLeft
           | MoveRight
           | Increment
           | Decrement
           | EnterLoop
           | ExitLoop
           | Halt
     deriving Show

instance Point Instr where
  point = Halt

instance Point Nat where
  point = Zero

instance Point (Maybe a) where
  point = Nothing

data P'' = P'' (Tape Instr) (Tape Nat) deriving Show

memTape :: P'' -> Tape Nat
memTape (P'' _ mem) = mem

progTape :: P'' -> Tape Instr
progTape (P'' prog _) = prog

readInstr :: State P'' Instr
readInstr = get
    >>- \(P'' progTape _) -> injectState (readHead progTape)

advance :: State P'' Unit
advance = get
    >>- \(P'' progTape memTape) -> set (P'' (moveRight progTape) memTape)

-- * P'' Instructions

instrHalt :: State P'' Bool
instrHalt = injectState False

withMemTape :: (Tape Nat -> Tape Nat) -> State P'' Unit
withMemTape f = get
    >>- \(P'' progTape memTape) -> set (P'' progTape (f memTape))

withProgTape :: (Tape Instr -> Tape Instr) -> State P'' Unit
withProgTape f = get
    >>- \(P'' progTape memTape) -> set (P'' (f progTape) memTape)

instrMoveLeft :: State P'' Bool
instrMoveLeft = withMemTape moveLeft >>> injectState True

instrMoveRight :: State P'' Bool
instrMoveRight = withMemTape moveRight >>> injectState True

modHead :: (a -> a) -> Tape a -> Tape a
modHead f (Tape ls a rs) = Tape ls (f a) rs

instrIncrement :: State P'' Bool
instrIncrement = withMemTape (modHead Succ) >>> injectState True

instrDecrement :: State P'' Bool
instrDecrement = get
    >>- \(P'' progTape memTape) -> attemptDecr (readHead memTape)
  where
    attemptDecr :: Nat -> State P'' Bool
    attemptDecr Zero       = injectState False
    attemptDecr (Succ num) = withMemTape (modHead $ always num) >>> injectState True

gotoExit :: Nat -> State P'' Unit
gotoExit n = withProgTape moveRight
    >>> get
    >>- \(P'' progTape _) -> decide (readHead progTape) n
  where
    decide :: Instr -> Nat -> State P'' Unit
    decide EnterLoop n          = gotoExit (Succ n)
    decide ExitLoop Zero        = injectState Unit
    decide ExitLoop (Succ prev) = gotoExit prev
    decide _        n           = gotoExit n

instrEnter :: State P'' Bool
instrEnter = get
    >>- \(P'' progTape memTape) -> decide (readHead memTape)
  where
    decide :: Nat -> State P'' Bool
    decide Zero = gotoExit Zero >>> injectState True
    decide _    = injectState True

gotoEnter :: Nat -> State P'' Unit
gotoEnter n = withProgTape moveLeft
    >>> get
    >>- \(P'' progTape _) -> decide (readHead progTape) n
  where
    decide :: Instr -> Nat -> State P'' Unit
    decide ExitLoop  n           = gotoEnter (Succ n)
    decide EnterLoop Zero        = injectState Unit
    decide EnterLoop (Succ prev) = gotoEnter prev
    decide _         n           = gotoEnter n

instrExit :: State P'' Bool
instrExit = get
    >>- \(P'' progTape memTape) -> decide (readHead memTape)
  where
    decide :: Nat -> State P'' Bool
    decide (Succ n) = gotoEnter Zero >>> injectState True
    decide Zero    = injectState True

run :: Instr -> State P'' Bool
run Halt      = instrHalt
run MoveLeft  = instrMoveLeft
run MoveRight = instrMoveRight
run Increment = instrIncrement
run Decrement = instrDecrement
run EnterLoop = instrEnter
run ExitLoop  = instrExit

pipeline :: State P'' Unit
pipeline s = (readInstr
    >>- \instr -> trace (show instr ++ ": " ++ show (memTape s)) run instr
    >>- \stillRunning -> advanceAndRepeat stillRunning) s
  where
    advanceAndRepeat :: Bool -> State P'' Unit
    advanceAndRepeat True  = advance >>> pipeline
    advanceAndRepeat False = injectState Unit

execute :: Tape Instr -> Tape Nat
execute program = memTape $ snd $ pipeline (P'' program emptyTape)
  where
    emptyTape :: Point m => Tape m
    emptyTape = Tape Nil point Nil
	let swap = Tape Nil EnterLoop ( Cons MoveRight -- →
	$ Cons EnterLoop -- [
	$ Cons Decrement -- -
	$ Cons MoveRight -- →
	$ Cons Increment -- +
	$ Cons MoveLeft -- ←
	$ Cons ExitLoop -- ]
	$ Cons MoveLeft -- ←
	$ Cons EnterLoop -- [
	$ Cons Decrement -- -
	$ Cons MoveRight -- →
	$ Cons Increment -- +
	$ Cons MoveLeft -- ←
	$ Cons ExitLoop -- ]
	$ Cons MoveRight -- →
	$ Cons MoveRight -- →
	$ Cons EnterLoop -- [
	$ Cons Decrement -- -
	$ Cons MoveLeft -- ←
	$ Cons MoveLeft -- ←
	$ Cons Increment -- +
	$ Cons MoveRight -- →
	$ Cons MoveRight -- →
	$ Cons ExitLoop -- ]
	$ Cons ExitLoop -- ]
	$ Cons Halt -- ¤
	$ Nil
	)

	let tape = Tape Nil (Succ $ Succ $ Succ Zero) (Cons (Succ $ Succ Zero) $ Cons Zero Nil)
	-- Tape [] 3 [2, 0]

	memTape $ snd $ pipeline (P'' swap tape)
	-- Tape [3, 2] 0 []

	-- It swaps 3 and 2, and uses 0 as a temp var.
	-- To simplify moveRight logic element is appended to the head of the list instead of end of the tail
	-- And to simplify moveLeft logic element is taken from the head of the list instead of end of the tail
	-- So-to-say move logic is reversed not to make it recursively append to the end and take from the end

	-- ↓
	-- [ → [ - → + ← ] ← [ - → + ← ] → → [ - ← ← + → → ] ] ¤ : (3 2 0)
	-- 3 2
	-- 1 0 1 1 ↓
	-- 0 1 2 0 : (3 0 2)
	-- 3 2 0 1 2
	-- 1 1 2 1 ↓
	-- 0 2 3 0 : (0 3 2)
	-- 3 2
	-- 1 3 0 1 3 1 ↓
	-- 0 3 1 2 3 0 : (2 3 0)

	-- TL;DR 3 2 0 becomes 2 3 0
	{-# LANGUAGE TypeSynonymInstances #-}

	import Debug.Trace

	-- * Base

	data Unit = Unit deriving Show

	data Nat = Succ Nat
	\| Zero

	instance Show Nat where
	show n = show $ go n
	where
	go Zero = 0
	go (Succ x) = 1 + go x

	data List a = Nil
	\| Cons a (List a)

	instance Show a => Show (List a) where
	show xs = "[" ++ go xs
	where
	go Nil = "]"
	go (Cons x Nil) = show x ++ "]"
	go (Cons x xs) = show x ++ ", " ++ go xs

	-- * State

	-- not proving State is a custom Kleisli class from the book because Haskell doesn't allow partially aplied type synonims
	-- also not using do-notation as in the book, because we'd need to prove State is a Monad or Applicative
	type State s a = s -> (a, s)

	injectState :: a -> State s a
	injectState a s = (a, s)

	composeState :: (a -> s -> (b, s))
	-> (b -> s -> (c, s))
	-> a
	-> s
	-> (c, s)
	composeState m1 m2 a state = (c, finalState)
	where
	(b, newState) = m1 a state
	(c, finalState) = m2 b newState

	get :: State s s
	get state = (state, state)

	set :: s -> State s Unit
	set newState _ = (Unit, newState)

	modify :: (s -> s) -> State s Unit
	modify f state = set (f state) state

	always :: x -> y -> x
	always x _ = x

	bind :: State s a
	-> (a -> State s b)
	-> State s b
	bind ma f = composeState (always ma) f Unit

	-- can' use >>= because of already existing monadic operator
	(>>-) = bind

	ignoring :: State s a
	-> State s b
	-> State s b
	ignoring ma mb = ma
	>>- \_ -> mb

	-- can' use >> because of already existing monadic operator
	(>>>) = ignoring

	hold :: Bool -> State Bool Bool
	hold val = get
	>>- \s -> set (val \|\| s)
	>>> get

	-- * P''

	data Tape a = Tape (List a) a (List a) deriving Show

	class Point a where
	point :: a

	readHead :: Tape a -> a
	readHead (Tape _ a _) = a

	-- might feel odd as it takes first element instead of last
	moveLeft :: Point a => Tape a -> Tape a
	moveLeft (Tape (Cons l ls) a rs) = Tape ls l (Cons a rs)
	moveLeft (Tape Nil a rs) = Tape Nil point (Cons a rs)

	-- might feel odd as it puts element as a head instead of last
	moveRight :: Point a => Tape a -> Tape a
	moveRight (Tape ls a (Cons r rs)) = Tape (Cons a ls) r rs
	moveRight (Tape ls a Nil) = Tape (Cons a ls) point Nil

	data Instr = MoveLeft
	\| MoveRight
	\| Increment
	\| Decrement
	\| EnterLoop
	\| ExitLoop
	\| Halt
	deriving Show

	instance Point Instr where
	point = Halt

	instance Point Nat where
	point = Zero

	instance Point (Maybe a) where
	point = Nothing

	data P'' = P'' (Tape Instr) (Tape Nat) deriving Show

	memTape :: P'' -> Tape Nat
	memTape (P'' _ mem) = mem

	progTape :: P'' -> Tape Instr
	progTape (P'' prog _) = prog

	readInstr :: State P'' Instr
	readInstr = get
	>>- \(P'' progTape _) -> injectState (readHead progTape)

	advance :: State P'' Unit
	advance = get
	>>- \(P'' progTape memTape) -> set (P'' (moveRight progTape) memTape)

	-- * P'' Instructions

	instrHalt :: State P'' Bool
	instrHalt = injectState False

	withMemTape :: (Tape Nat -> Tape Nat) -> State P'' Unit
	withMemTape f = get
	>>- \(P'' progTape memTape) -> set (P'' progTape (f memTape))

	withProgTape :: (Tape Instr -> Tape Instr) -> State P'' Unit
	withProgTape f = get
	>>- \(P'' progTape memTape) -> set (P'' (f progTape) memTape)

	instrMoveLeft :: State P'' Bool
	instrMoveLeft = withMemTape moveLeft >>> injectState True

	instrMoveRight :: State P'' Bool
	instrMoveRight = withMemTape moveRight >>> injectState True

	modHead :: (a -> a) -> Tape a -> Tape a
	modHead f (Tape ls a rs) = Tape ls (f a) rs

	instrIncrement :: State P'' Bool
	instrIncrement = withMemTape (modHead Succ) >>> injectState True

	instrDecrement :: State P'' Bool
	instrDecrement = get
	>>- \(P'' progTape memTape) -> attemptDecr (readHead memTape)
	where
	attemptDecr :: Nat -> State P'' Bool
	attemptDecr Zero = injectState False
	attemptDecr (Succ num) = withMemTape (modHead $ always num) >>> injectState True

	gotoExit :: Nat -> State P'' Unit
	gotoExit n = withProgTape moveRight
	>>> get
	>>- \(P'' progTape _) -> decide (readHead progTape) n
	where
	decide :: Instr -> Nat -> State P'' Unit
	decide EnterLoop n = gotoExit (Succ n)
	decide ExitLoop Zero = injectState Unit
	decide ExitLoop (Succ prev) = gotoExit prev
	decide _ n = gotoExit n

	instrEnter :: State P'' Bool
	instrEnter = get
	>>- \(P'' progTape memTape) -> decide (readHead memTape)
	where
	decide :: Nat -> State P'' Bool
	decide Zero = gotoExit Zero >>> injectState True
	decide _ = injectState True

	gotoEnter :: Nat -> State P'' Unit
	gotoEnter n = withProgTape moveLeft
	>>> get
	>>- \(P'' progTape _) -> decide (readHead progTape) n
	where
	decide :: Instr -> Nat -> State P'' Unit
	decide ExitLoop n = gotoEnter (Succ n)
	decide EnterLoop Zero = injectState Unit
	decide EnterLoop (Succ prev) = gotoEnter prev
	decide _ n = gotoEnter n

	instrExit :: State P'' Bool
	instrExit = get
	>>- \(P'' progTape memTape) -> decide (readHead memTape)
	where
	decide :: Nat -> State P'' Bool
	decide (Succ n) = gotoEnter Zero >>> injectState True
	decide Zero = injectState True

	run :: Instr -> State P'' Bool
	run Halt = instrHalt
	run MoveLeft = instrMoveLeft
	run MoveRight = instrMoveRight
	run Increment = instrIncrement
	run Decrement = instrDecrement
	run EnterLoop = instrEnter
	run ExitLoop = instrExit

	pipeline :: State P'' Unit
	pipeline s = (readInstr
	>>- \instr -> trace (show instr ++ ": " ++ show (memTape s)) run instr
	>>- \stillRunning -> advanceAndRepeat stillRunning) s
	where
	advanceAndRepeat :: Bool -> State P'' Unit
	advanceAndRepeat True = advance >>> pipeline
	advanceAndRepeat False = injectState Unit

	execute :: Tape Instr -> Tape Nat
	execute program = memTape $ snd $ pipeline (P'' program emptyTape)
	where
	emptyTape :: Point m => Tape m
	emptyTape = Tape Nil point Nil