Compare commits
No commits in common. "298cf6599c8990f779a25880f3ad609269f283a2" and "ba141031dd8d0968469f15f57175f34a3c158464" have entirely different histories.
298cf6599c
...
ba141031dd
|
@ -1,21 +0,0 @@
|
|||
takeUntilMax :: [Int] -> Int -> (Int, [Int])
|
||||
takeUntilMax [] m = (m, [])
|
||||
takeUntilMax [x] _ = (x, [x])
|
||||
takeUntilMax (x:xs) m
|
||||
| x == m = (x, [x])
|
||||
| otherwise =
|
||||
let (m', xs') = takeUntilMax xs m
|
||||
in (max m' x, x:xs')
|
||||
|
||||
doTakeUntilMax :: [Int] -> [Int]
|
||||
doTakeUntilMax l = l'
|
||||
where (m, l') = takeUntilMax l m
|
||||
|
||||
takeUntilMax' :: [Int] -> Int -> (Int, [Int])
|
||||
takeUntilMax' [] m = (m, [])
|
||||
takeUntilMax' [x] _ = (x, [x])
|
||||
takeUntilMax' (x:xs) m
|
||||
| x == m = (maximum (x:xs), [x])
|
||||
| otherwise =
|
||||
let (m', xs') = takeUntilMax' xs m
|
||||
in (max m' x, x:xs')
|
|
@ -1,28 +0,0 @@
|
|||
import Data.Map as Map
|
||||
import Data.Maybe
|
||||
import Control.Applicative
|
||||
|
||||
data Element = A | B | C | D
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
addElement :: Element -> Map Element Int -> Map Element Int
|
||||
addElement = alter ((<|> Just 1) . fmap (+1))
|
||||
|
||||
getScore :: Element -> Map Element Int -> Float
|
||||
getScore e m = fromMaybe 1.0 $ ((1.0/) . fromIntegral) <$> Map.lookup e m
|
||||
|
||||
data BinaryTree a = Empty | Node a (BinaryTree a) (BinaryTree a) deriving Show
|
||||
type ElementTree = BinaryTree Element
|
||||
type ScoredElementTree = BinaryTree (Element, Float)
|
||||
|
||||
assignScores :: ElementTree -> Map Element Int -> (Map Element Int, ScoredElementTree)
|
||||
assignScores Empty m = (Map.empty, Empty)
|
||||
assignScores (Node e t1 t2) m = (m', Node (e, getScore e m) t1' t2')
|
||||
where
|
||||
(m1, t1') = assignScores t1 m
|
||||
(m2, t2') = assignScores t2 m
|
||||
m' = addElement e $ unionWith (+) m1 m2
|
||||
|
||||
doAssignScores :: ElementTree -> ScoredElementTree
|
||||
doAssignScores t = t'
|
||||
where (m, t') = assignScores t m
|
|
@ -1,120 +0,0 @@
|
|||
data ExprType
|
||||
= IntType
|
||||
| BoolType
|
||||
| StringType
|
||||
| PairType ExprType ExprType
|
||||
|
||||
repr : ExprType -> Type
|
||||
repr IntType = Int
|
||||
repr BoolType = Bool
|
||||
repr StringType = String
|
||||
repr (PairType t1 t2) = Pair (repr t1) (repr t2)
|
||||
|
||||
decEq : (a : ExprType) -> (b : ExprType) -> Maybe (a = b)
|
||||
decEq IntType IntType = Just Refl
|
||||
decEq BoolType BoolType = Just Refl
|
||||
decEq StringType StringType = Just Refl
|
||||
decEq (PairType lt1 lt2) (PairType rt1 rt2) = do
|
||||
subEq1 <- decEq lt1 rt1
|
||||
subEq2 <- decEq lt2 rt2
|
||||
let firstEqual = replace {P = \t1 => PairType lt1 lt2 = PairType t1 lt2} subEq1 Refl
|
||||
let secondEqual = replace {P = \t2 => PairType lt1 lt2 = PairType rt1 t2} subEq2 firstEqual
|
||||
pure secondEqual
|
||||
decEq _ _ = Nothing
|
||||
|
||||
data Op
|
||||
= Add
|
||||
| Subtract
|
||||
| Multiply
|
||||
| Divide
|
||||
|
||||
data Expr
|
||||
= IntLit Int
|
||||
| BoolLit Bool
|
||||
| StringLit String
|
||||
| BinOp Op Expr Expr
|
||||
| IfElse Expr Expr Expr
|
||||
| Pair Expr Expr
|
||||
| Fst Expr
|
||||
| Snd Expr
|
||||
|
||||
data SafeExpr : ExprType -> Type where
|
||||
IntLiteral : Int -> SafeExpr IntType
|
||||
BoolLiteral : Bool -> SafeExpr BoolType
|
||||
StringLiteral : String -> SafeExpr StringType
|
||||
BinOperation : (repr a -> repr b -> repr c) -> SafeExpr a -> SafeExpr b -> SafeExpr c
|
||||
IfThenElse : SafeExpr BoolType -> SafeExpr t -> SafeExpr t -> SafeExpr t
|
||||
NewPair : SafeExpr t1 -> SafeExpr t2 -> SafeExpr (PairType t1 t2)
|
||||
First : SafeExpr (PairType t1 t2) -> SafeExpr t1
|
||||
Second : SafeExpr (PairType t1 t2) -> SafeExpr t2
|
||||
|
||||
typecheckOp : Op -> (a : ExprType) -> (b : ExprType) -> Either String (c : ExprType ** repr a -> repr b -> repr c)
|
||||
typecheckOp Add IntType IntType = Right (IntType ** (+))
|
||||
typecheckOp Subtract IntType IntType = Right (IntType ** (-))
|
||||
typecheckOp Multiply IntType IntType = Right (IntType ** (*))
|
||||
typecheckOp Divide IntType IntType = Right (IntType ** div)
|
||||
typecheckOp _ _ _ = Left "Invalid binary operator application"
|
||||
|
||||
requireBool : (n : ExprType ** SafeExpr n) -> Either String (SafeExpr BoolType)
|
||||
requireBool (BoolType ** e) = Right e
|
||||
requireBool _ = Left "Not a boolean."
|
||||
|
||||
typecheck : Expr -> Either String (n : ExprType ** SafeExpr n)
|
||||
typecheck (IntLit i) = Right (_ ** IntLiteral i)
|
||||
typecheck (BoolLit b) = Right (_ ** BoolLiteral b)
|
||||
typecheck (StringLit s) = Right (_ ** StringLiteral s)
|
||||
typecheck (BinOp o l r) = do
|
||||
(lt ** le) <- typecheck l
|
||||
(rt ** re) <- typecheck r
|
||||
(ot ** f) <- typecheckOp o lt rt
|
||||
pure (_ ** BinOperation f le re)
|
||||
typecheck (IfElse c t e) =
|
||||
do
|
||||
ce <- typecheck c >>= requireBool
|
||||
(tt ** te) <- typecheck t
|
||||
(et ** ee) <- typecheck e
|
||||
case decEq tt et of
|
||||
Just p => pure (_ ** IfThenElse ce (replace p te) ee)
|
||||
Nothing => Left "Incompatible branch types."
|
||||
typecheck (Pair l r) =
|
||||
do
|
||||
(lt ** le) <- typecheck l
|
||||
(rt ** re) <- typecheck r
|
||||
pure (_ ** NewPair le re)
|
||||
typecheck (Fst p) =
|
||||
do
|
||||
(pt ** pe) <- typecheck p
|
||||
case pt of
|
||||
PairType _ _ => pure $ (_ ** First pe)
|
||||
_ => Left "Applying fst to non-pair."
|
||||
typecheck (Snd p) =
|
||||
do
|
||||
(pt ** pe) <- typecheck p
|
||||
case pt of
|
||||
PairType _ _ => pure $ (_ ** Second pe)
|
||||
_ => Left "Applying snd to non-pair."
|
||||
|
||||
eval : SafeExpr t -> repr t
|
||||
eval (IntLiteral i) = i
|
||||
eval (BoolLiteral b) = b
|
||||
eval (StringLiteral s) = s
|
||||
eval (BinOperation f l r) = f (eval l) (eval r)
|
||||
eval (IfThenElse c t e) = if (eval c) then (eval t) else (eval e)
|
||||
eval (NewPair l r) = (eval l, eval r)
|
||||
eval (First p) = fst (eval p)
|
||||
eval (Second p) = snd (eval p)
|
||||
|
||||
resultStr : {t : ExprType} -> repr t -> String
|
||||
resultStr {t=IntType} i = show i
|
||||
resultStr {t=BoolType} b = show b
|
||||
resultStr {t=StringType} s = show s
|
||||
resultStr {t=PairType t1 t2} (l,r) = "(" ++ resultStr l ++ ", " ++ resultStr r ++ ")"
|
||||
|
||||
tryEval : Expr -> String
|
||||
tryEval ex =
|
||||
case typecheck ex of
|
||||
Left err => "Type error: " ++ err
|
||||
Right (t ** e) => resultStr $ eval {t} e
|
||||
|
||||
main : IO ()
|
||||
main = putStrLn $ tryEval $ BinOp Add (Fst (IfElse (BoolLit True) (Pair (IntLit 6) (BoolLit True)) (Pair (IntLit 7) (BoolLit False)))) (BinOp Multiply (IntLit 160) (IntLit 2))
|
|
@ -1,7 +1,8 @@
|
|||
---
|
||||
title: "Time Traveling In Haskell: How It Works And How To Use It"
|
||||
date: 2020-07-30T00:58:10-07:00
|
||||
date: 2020-05-03T20:05:29-07:00
|
||||
tags: ["Haskell"]
|
||||
draft: true
|
||||
---
|
||||
|
||||
I recently got to use a very curious Haskell technique
|
||||
|
@ -9,7 +10,8 @@ I recently got to use a very curious Haskell technique
|
|||
As production as research code gets, anyway!
|
||||
{{< /sidenote >}} time traveling. I say this with
|
||||
the utmost seriousness. This technique worked like
|
||||
magic for the problem I was trying to solve, and so
|
||||
magic for the problem I was trying to solve (which isn't
|
||||
interesting enough to be presented here in itself), and so
|
||||
I thought I'd share what I learned. In addition
|
||||
to the technique and its workings, I will also explain how
|
||||
time traveling can be misused, yielding computations that
|
||||
|
@ -67,7 +69,7 @@ value even come from?
|
|||
|
||||
Thus far, nothing too magical has happened. It's a little
|
||||
strange to expect the result of the computation to be
|
||||
given to us; it just looks like wishful
|
||||
given to us; however, thus far, it looks like wishful
|
||||
thinking. The real magic happens in Csongor's `doRepMax`
|
||||
function:
|
||||
|
||||
|
@ -93,9 +95,8 @@ Why is it called graph reduction, you may be wondering, if the runtime is
|
|||
manipulating syntax trees? To save on work, if a program refers to the
|
||||
same value twice, Haskell has both of those references point to the
|
||||
exact same graph. This violates the tree's property of having only one path
|
||||
from the root to any node, and makes our program a DAG (at least). Graph nodes that
|
||||
refer to themselves (which are also possible in the model) also violate the properties of a
|
||||
a DAG, and thus, in general, we are working with graphs.
|
||||
from the root to any node, and makes our program a graph. Graphs that
|
||||
refer to themselves also violate the properties of a tree.
|
||||
{{< /sidenote >}} performing
|
||||
substitutions and simplifications as necessary until it reaches a final answer.
|
||||
What the lazy part means is that parts of the syntax tree that are not yet
|
||||
|
@ -125,7 +126,7 @@ length ((:) 1 [])
|
|||
We're now ready to draw the graph; in this case, it's pretty much identical
|
||||
to the syntax tree of the last form of our expression:
|
||||
|
||||
{{< figure src="length_1.png" caption="The initial graph of `length [1]`." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
In this image, the `@` nodes represent function application. The
|
||||
root node is an application of the function `length` to the graph that
|
||||
|
@ -136,7 +137,7 @@ list, and function applications in Haskell are
|
|||
in the process of evaluation, the body of `length` will be reached,
|
||||
and leave us with the following graph:
|
||||
|
||||
{{< figure src="length_2.png" caption="The graph of `length [1]` after the body of `length` is expanded." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Conceptually, we only took one reduction step, and thus, we haven't yet gotten
|
||||
to evaluating the recursive call to `length`. Since `(+)`
|
||||
|
@ -168,17 +169,17 @@ let x = square 5 in x + x
|
|||
|
||||
Here, the initial graph looks as follows:
|
||||
|
||||
{{< figure src="square_1.png" caption="The initial graph of `let x = square 5 in x + x`." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
As you can see, this _is_ a graph, but not a tree! Since both
|
||||
As you can see, this _is_ a graph, not a tree! Since both
|
||||
variables `x` refer to the same expression, `square 5`, they
|
||||
are represented by the same subgraph. Then, when we evaluate `square 5`
|
||||
for the first time, and replace its root node with an indirection,
|
||||
we end up with the following:
|
||||
|
||||
{{< figure src="square_2.png" caption="The graph of `let x = square 5 in x + x` after `square 5` is reduced." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
There are two `25`s in the graph, and no more `square`s! We only
|
||||
There are two `25`s in the tree, and no more `square`s! We only
|
||||
had to evaluate `square 5` exactly once, even though `(+)`
|
||||
will use it twice (once for the left argument, and once for the right).
|
||||
|
||||
|
@ -201,22 +202,21 @@ fix f = let x = f x in x
|
|||
See how the definition of `x` refers to itself? This is what
|
||||
it looks like in graph form:
|
||||
|
||||
{{< figure src="fixpoint_1.png" caption="The initial graph of `let x = f x in x`." class="tiny" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
I think it's useful to take a look at how this graph is processed. Let's
|
||||
pick `f = (1:)`. That is, `f` is a function that takes a list,
|
||||
and prepends `1` to it. Then, after constructing the graph of `f x`,
|
||||
we end up with the following:
|
||||
|
||||
{{< figure src="fixpoint_2.png" caption="The graph of `fix (1:)` after it's been reduced." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
We see the body of `f`, which is the application of `(:)` first to the
|
||||
constant `1`, and then to `f`'s argument (`x`, in this case). As
|
||||
before, once we evaluated `f x`, we replaced the application with
|
||||
an indirection; in the image, this indirection is the top box. But the
|
||||
argument, `x`, is itself an indirection which points to the root of `f x`,
|
||||
thereby creating a cycle in our graph. Traversing this graph looks like
|
||||
traversing an infinite list of `1`s.
|
||||
thereby creating a cycle in our graph.
|
||||
|
||||
Almost there! A node can refer to itself, and, when evaluated, it
|
||||
is replaced with its own value. Thus, a node can effectively reference
|
||||
|
@ -247,23 +247,25 @@ of using application nodes `@`, let's draw an application of a
|
|||
function `f` to arguments `x1` through `xn` as a subgraph with root `f`
|
||||
and children `x`s. The below figure demonstrates what I mean:
|
||||
|
||||
{{< figure src="notation.png" caption="The new visual notation used in this section." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Now, let's write the initial graph for `doRepMax [1,2]`:
|
||||
|
||||
{{< figure src="repmax_1.png" caption="The initial graph of `doRepMax [1,2]`." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Other than our new notation, there's nothing too surprising here.
|
||||
The first step of our hypothetical reduction would replace the application of `doRepMax` with its
|
||||
body, and create our graph's first cycle. At a high level, all we want is the second element of the tuple
|
||||
At a high level, all we want is the second element of the tuple
|
||||
returned by `repMax`, which contains the output list. To get
|
||||
the tuple, we apply `repMax` to the list `[1,2]` and the first element
|
||||
of its result. The list `[1,2]` itself
|
||||
the tuple, we apply `repMax` to the list `[1,2]`, which itself
|
||||
consists of two uses of the `(:)` function.
|
||||
|
||||
{{< figure src="repmax_2.png" caption="The first step of reducing `doRepMax [1,2]`." class="small" >}}
|
||||
The first step
|
||||
of our hypothetical reduction would replace the application of `doRepMax` with its
|
||||
body, and create our graph's first cycle:
|
||||
|
||||
Next, we would also expand the body of `repMax`. In
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Next, we would do the same for the body of `repMax`. In
|
||||
the following diagram, to avoid drawing a noisy amount of
|
||||
crossing lines, I marked the application of `fst` with
|
||||
a star, and replaced the two edges to `fst` with
|
||||
|
@ -271,7 +273,7 @@ edges to similar looking stars. This is merely
|
|||
a visual trick; an edge leading to a little star is
|
||||
actually an edge leading to `fst`. Take a look:
|
||||
|
||||
{{< figure src="repmax_3.png" caption="The second step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Since `(,)` is a constructor, let's say that it doesn't
|
||||
need to be evaluated, and that its
|
||||
|
@ -287,11 +289,9 @@ thus replace the application of `snd` with an
|
|||
indirection to this subgraph. This leaves us
|
||||
with the following:
|
||||
|
||||
{{< figure src="repmax_4.png" caption="The third step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Since it's becoming hard to keep track of what part of the graph
|
||||
is actually being evaluated, I marked the former root of `doRepMax [1,2]` with
|
||||
a blue star. If our original expression occured at the top level,
|
||||
If our original `doRepMax [1, 2]` expression occured at the top level,
|
||||
the graph reduction would probably stop here. After all,
|
||||
we're evaluating our graphs using call-by-need, and there
|
||||
doesn't seem to be a need for knowing the what the arguments of `(:)` are.
|
||||
|
@ -307,7 +307,7 @@ of `fst`. We evaluate it in a similar manner to `snd`. That is,
|
|||
we replace this `fst` with an indirection to the first element
|
||||
of the argument tuple, which happens to be the subgraph starting with `max`:
|
||||
|
||||
{{< figure src="repmax_5.png" caption="The fourth step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
Phew! Next, we need to evaluate the body of `max`. Let's make one more
|
||||
simplification here: rather than substitututing `max` for its body
|
||||
|
@ -319,23 +319,23 @@ a call to `fst`, needs to be processed. To do so, we need to
|
|||
evaluate the call to `repMax`. We thus replace `repMax`
|
||||
with its body:
|
||||
|
||||
{{< figure src="repmax_6.png" caption="The fifth step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
We've reached one of the base cases here, and there
|
||||
are no more calls to `max` or `repMax`. The whole reason
|
||||
we're here is to evaluate the call to `fst` that's one
|
||||
of the arguments to `max`. Given this graph, doing so is easy.
|
||||
of the arguments to `max`. Given this graph, this is easy.
|
||||
We can clearly see that `2` is the first element of the tuple
|
||||
returned by `repMax [2]`. We thus replace `fst` with
|
||||
an indirection to this node:
|
||||
|
||||
{{< figure src="repmax_7.png" caption="The sixth step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
This concludes our task of evaluating the arguments to `max`.
|
||||
Comparing them, we see that `2` is greater than `1`, and thus,
|
||||
we replace `max` with an indirection to `2`:
|
||||
|
||||
{{< figure src="repmax_8.png" caption="The seventh step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
The node that we starred in our graph is now an indirection (the
|
||||
one that used to be the call to `fst`) which points to
|
||||
|
@ -351,213 +351,48 @@ which is the call to `snd`. This `snd` is applied to an instance of `(,)`, which
|
|||
can't be reduced any further. Thus, all we have to do is take the second
|
||||
element of the tuple, and replace `snd` with an indirection to it:
|
||||
|
||||
{{< figure src="repmax_9.png" caption="The eighth step of reducing `doRepMax [1,2]`." class="medium" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
The second element of the tuple was a call to `(:)`, and that's what the mysterious
|
||||
force is processing now. Just like it did before, it starts by looking at the
|
||||
first argument of this list, which is the list's head. This argument is a reference to
|
||||
first argument of this list, which is head. This argument is a reference to
|
||||
the starred node, which, as we've established, eventually points to `2`.
|
||||
Another `2` pops up on the console.
|
||||
|
||||
Finally, the mysterious force reaches the second argument of the `(:)`,
|
||||
which is the empty list. The empty list also cannot be evaluated any
|
||||
further, so that's what the mysterious force receives. Just like that,
|
||||
there's nothing left to print to the console. The mysterious force ceases.
|
||||
After removing the unused nodes, we are left with the following graph:
|
||||
there's nothing left to print to the console. The mysterious force ceases,
|
||||
and we're left with the following graph:
|
||||
|
||||
{{< figure src="repmax_10.png" caption="The result of reducing `doRepMax [1,2]`." class="small" >}}
|
||||
{{< todo >}}Add image!{{< /todo >}}
|
||||
|
||||
As we would have expected, two `2`s were printed to the console, and our
|
||||
final graph represents the list `[2,2]`.
|
||||
As we would have expected, two `2`s are printed to the console.
|
||||
|
||||
### Using Time Traveling
|
||||
Is time tarveling even useful? I would argue yes, especially
|
||||
in cases where Haskell's purity can make certain things
|
||||
difficult.
|
||||
|
||||
As a first example, Csongor provides an assembler that works
|
||||
in a single pass. The challenge in this case is to resolve
|
||||
jumps to code segments occuring _after_ the jump itself;
|
||||
in essence, the address of the target code segment needs to be
|
||||
known before the segment itself is processed. Csongor's
|
||||
code uses the [Tardis monad](https://hackage.haskell.org/package/tardis-0.4.1.0/docs/Control-Monad-Tardis.html),
|
||||
which combines regular state, to which you can write and then
|
||||
later read from, and future state, from which you can
|
||||
read values before your write them. Check out
|
||||
[his complete example](https://kcsongor.github.io/time-travel-in-haskell-for-dummies/#a-single-pass-assembler-an-example) here.
|
||||
|
||||
Alternatively, here's an example from my research. I'll be fairly
|
||||
vague, since all of this is still in progress. The gist is that
|
||||
we have some kind of data structure (say, a list or a tree),
|
||||
and we want to associate with each element in this data
|
||||
structure a 'score' of how useful it is. There are many possible
|
||||
heuristics of picking 'scores'; a very simple one is
|
||||
to make it inversely propertional to the number of times
|
||||
an element occurs. To be more concrete, suppose
|
||||
we have some element type `Element`:
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/ValueScore.hs" 5 6 >}}
|
||||
|
||||
Suppose also that our data structure is a binary tree:
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/ValueScore.hs" 14 16 >}}
|
||||
|
||||
We then want to transform an input `ElementTree`, such as:
|
||||
|
||||
```Haskell
|
||||
Node A (Node A Empty Empty) Empty
|
||||
```
|
||||
|
||||
Into a scored tree, like:
|
||||
|
||||
```Haskell
|
||||
Node (A,0.5) (Node (A,0.5) Empty Empty) Empty
|
||||
```
|
||||
|
||||
Since `A` occured twice, its score is `1/2 = 0.5`.
|
||||
|
||||
Let's define some utility functions before we get to the
|
||||
meat of the implementation:
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/ValueScore.hs" 8 12 >}}
|
||||
|
||||
The `addElement` function simply increments the counter for a particular
|
||||
element in the map, adding the number `1` if it doesn't exist. The `getScore`
|
||||
function computes the score of a particular element, defaulting to `1.0` if
|
||||
it's not found in the map.
|
||||
|
||||
Just as before -- noticing that passing around the future values is getting awfully
|
||||
bothersome -- we write our scoring function as though we have
|
||||
a 'future value'.
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/ValueScore.hs" 18 24 >}}
|
||||
|
||||
The actual `doAssignScores` function is pretty much identical to
|
||||
`doRepMax`:
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/ValueScore.hs" 26 28 >}}
|
||||
|
||||
There's quite a bit of repetition here, especially in the handling
|
||||
of future values - all of our functions now accept an extra
|
||||
future argument, and return a work-in-progress future value.
|
||||
This is what the `Tardis` monad, and its corresponding
|
||||
`TardisT` monad transformer, aim to address. Just like the
|
||||
`State` monad helps us avoid writing plumbing code for
|
||||
forward-traveling values, `Tardis` helps us do the same
|
||||
for backward-traveling ones.
|
||||
|
||||
#### Cycles in Monadic Bind
|
||||
|
||||
We've seen that we're able to write code like the following:
|
||||
|
||||
```Haskell
|
||||
(a, b) = f a c
|
||||
```
|
||||
|
||||
That is, we were able to write function calls that referenced
|
||||
their own return values. What if we try doing this inside
|
||||
a `do` block? Say, for example, we want to sprinkle some time
|
||||
traveling into our program, but don't want to add a whole new
|
||||
transformer into our monad stack. We could write code as follows:
|
||||
|
||||
```Haskell
|
||||
do
|
||||
(a, b) <- f a c
|
||||
return b
|
||||
```
|
||||
|
||||
Unfortunately, this doesn't work. However, it's entirely
|
||||
possible to enable this using the `RecursiveDo` language
|
||||
extension:
|
||||
|
||||
```Haskell
|
||||
{-# LANGUAGE RecursiveDo #-}
|
||||
```
|
||||
|
||||
Then, we can write the above as follows:
|
||||
|
||||
```Haskell
|
||||
do
|
||||
rec (a, b) <- f a c
|
||||
return b
|
||||
```
|
||||
|
||||
This power, however, comes at a price. It's not as straightforward
|
||||
to build graphs from recursive monadic computations; in fact,
|
||||
it's not possible in general. The translation of the above
|
||||
code uses `MonadFix`. A monad that satisfies `MonadFix` has
|
||||
an operation `mfix`, which is the monadic version of the `fix`
|
||||
function we saw earlier:
|
||||
|
||||
```Haskell
|
||||
mfix :: Monad m => (a -> m a) -> m a
|
||||
-- Regular fix, for comparison
|
||||
fix :: (a -> a) -> a
|
||||
```
|
||||
|
||||
To really understand how the translation works, check out the
|
||||
[paper on recursive do notation](http://leventerkok.github.io/papers/recdo.pdf).
|
||||
{{< todo >}}This whole section {{< /todo >}}
|
||||
|
||||
### Beware The Strictness
|
||||
Though Csongor points out other problems with the
|
||||
time traveling approach, I think he doesn't mention
|
||||
an important idea: you have to be _very_ careful about introducing
|
||||
strictness into your programs when running time-traveling code.
|
||||
For example, suppose we wanted to write a function,
|
||||
`takeUntilMax`, which would return the input list,
|
||||
cut off after the first occurence of the maximum number.
|
||||
Following the same strategy, we come up with:
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/TakeMax.hs" 1 12 >}}
|
||||
{{< todo >}}This whole section, too. {{< /todo >}}
|
||||
|
||||
In short, if we encounter our maximum number, we just return
|
||||
a list of that maximum number, since we do not want to recurse
|
||||
further. On the other hand, if we encounter a number that's
|
||||
_not_ the maximum, we continue our recursion.
|
||||
### Leftovers
|
||||
|
||||
Unfortunately, this doesn't work; our program never terminates.
|
||||
You may be thinking:
|
||||
This is
|
||||
what allows us to write the code above: the graph of `repMax xs largest`
|
||||
effectively refers to itself. While traversing the list, it places references
|
||||
to itself in place of each of the elements, and thanks to laziness, these
|
||||
references are not evaluated.
|
||||
|
||||
> Well, obviously this doesn't work! We didn't actually
|
||||
compute the maximum number properly, since we stopped
|
||||
recursing too early. We need to traverse the whole list,
|
||||
and not just the part before the maximum number.
|
||||
Let's try a more complicated example. How about instead of creating a new list,
|
||||
we return a `Map` containing the number of times each number occured, but only
|
||||
when those numbers were a factor of the maximum numbers. Our expected output
|
||||
will be:
|
||||
|
||||
To address this, we can reformulate our `takeUntilMax`
|
||||
function as follows:
|
||||
```
|
||||
>>> countMaxFactors [1,3,3,9]
|
||||
|
||||
{{< codelines "Haskell" "time-traveling/TakeMax.hs" 14 21 >}}
|
||||
fromList [(1, 1), (3, 2), (9, 1)]
|
||||
```
|
||||
|
||||
Now we definitely compute the maximum correctly! Alas,
|
||||
this doesn't work either. The issue lies on lines 5 and 18,
|
||||
more specifically in the comparison `x == m`. Here, we
|
||||
are trying to base the decision of what branch to take
|
||||
on a future value. This is simply impossible; to compute
|
||||
the value, we need to know the value!
|
||||
|
||||
This is no 'silly mistake', either! In complicated programs
|
||||
that use time traveling, strictness lurks behind every corner.
|
||||
In my research work, I was at one point inserting a data structure into
|
||||
a set; however, deep in the structure was a data type containing
|
||||
a 'future' value, and using the default `Eq` instance!
|
||||
Adding the data structure to a set ended up invoking `(==)` (or perhaps
|
||||
some function from the `Ord` typeclass),
|
||||
which, in turn, tried to compare the lazily evaluated values.
|
||||
My code therefore didn't terminate, much like `takeUntilMax`.
|
||||
|
||||
Debugging time traveling code is, in general,
|
||||
a pain. This is especially true since future values don't look any different
|
||||
from regular values. You can see it in the type signatures
|
||||
of `repMax` and `takeUntilMax`: the maximum number is just an `Int`!
|
||||
And yet, trying to see what its value is will kill the entire program.
|
||||
As always, remember Brian W. Kernighan's wise words:
|
||||
|
||||
> Debugging is twice as hard as writing the code in the first place.
|
||||
Therefore, if you write the code as cleverly as possible, you are,
|
||||
by definition, not smart enough to debug it.
|
||||
|
||||
### Conclusion
|
||||
This is about it! In a way, time traveling can make code performing
|
||||
certain operations more expressive. Furthermore, even if it's not groundbreaking,
|
||||
thinking about time traveling is a good exercise to get familiar
|
||||
with lazy evaluation in general. I hope you found this useful!
|
Before Width: | Height: | Size: 27 KiB |
Before Width: | Height: | Size: 48 KiB |
Before Width: | Height: | Size: 54 KiB |
Before Width: | Height: | Size: 72 KiB |
Before Width: | Height: | Size: 99 KiB |
Before Width: | Height: | Size: 44 KiB |
Before Width: | Height: | Size: 53 KiB |
Before Width: | Height: | Size: 70 KiB |
Before Width: | Height: | Size: 130 KiB |
Before Width: | Height: | Size: 123 KiB |
Before Width: | Height: | Size: 118 KiB |
Before Width: | Height: | Size: 122 KiB |
Before Width: | Height: | Size: 132 KiB |
Before Width: | Height: | Size: 125 KiB |
Before Width: | Height: | Size: 102 KiB |
Before Width: | Height: | Size: 58 KiB |
Before Width: | Height: | Size: 45 KiB |
|
@ -241,18 +241,6 @@ figure {
|
|||
figcaption {
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
&.tiny img {
|
||||
max-height: 15rem;
|
||||
}
|
||||
|
||||
&.small img {
|
||||
max-height: 20rem;
|
||||
}
|
||||
|
||||
&.medium img {
|
||||
max-height: 30rem;
|
||||
}
|
||||
}
|
||||
|
||||
.twitter-tweet {
|
||||
|
|