Add links in part 0 of compiler series.

This one uses line highlights!

code/time-traveling/TakeMax.hs

@@ -0,0 +1,21 @@
+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')

code/time-traveling/ValueScore.hs

@@ -0,0 +1,28 @@
+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

code/typesafe-interpreter/TypesafeIntrV2.idr

@@ -18,15 +18,15 @@ boolStringImpossible : BoolType = StringType -> Void
 boolStringImpossible Refl impossible
 
 decEq : (a : ExprType) -> (b : ExprType) -> Dec (a = b)
-decEq {a = IntType} {b = IntType} = Yes Refl
-decEq {a = BoolType} {b = BoolType} = Yes Refl
-decEq {a = StringType} {b = StringType} = Yes Refl
-decEq {a = IntType} {b = BoolType} = No intBoolImpossible
-decEq {a = BoolType} {b = IntType} = No $ intBoolImpossible . sym
-decEq {a = IntType} {b = StringType} = No intStringImpossible
-decEq {a = StringType} {b = IntType} = No $ intStringImpossible . sym
-decEq {a = BoolType} {b = StringType} = No boolStringImpossible 
-decEq {a = StringType} {b = BoolType} = No $ boolStringImpossible . sym
+decEq IntType IntType = Yes Refl
+decEq BoolType BoolType = Yes Refl
+decEq StringType StringType = Yes Refl
+decEq IntType BoolType = No intBoolImpossible
+decEq BoolType IntType = No $ intBoolImpossible . sym
+decEq IntType StringType = No intStringImpossible
+decEq StringType IntType = No $ intStringImpossible . sym
+decEq BoolType StringType = No boolStringImpossible 
+decEq StringType BoolType = No $ boolStringImpossible . sym
 
 data Op
   = Add

code/typesafe-interpreter/TypesafeIntrV3.idr

@@ -0,0 +1,120 @@
+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))

config.toml

@@ -1,9 +1,8 @@
-baseURL = "https://danilafe.com"
-languageCode = "en-us"
+languageCode = "en"
 title = "Daniel's Blog"
 theme = "vanilla"
 pygmentsCodeFences = true
-pygmentsStyle = "github"
+pygmentsUseClasses = true
 summaryLength = 20
 
 [markup]
@@ -11,3 +10,9 @@ summaryLength = 20
     endLevel = 4
     ordered = false
     startLevel = 3
+
+[languages]
+  [languages.en]
+    baseURL = "https://danilafe.com"
+  [languages.ru]
+    baseURL = "https://ru.danilafe.com"

content/_index.ru.md

@@ -0,0 +1,8 @@
+---
+title: Daniel's Blog
+description: Персональный блог Данилы Федорина о функциональном программировании, дизайне компиляторов, и многом другом! 
+---
+## Привет!
+Добро пожаловать на мой сайт. Здесь, я пишу на многие темы, включая фунциональное программирование, дизайн компилляторов, теорию языков программирования, и иногда компьютерные игры. Я надеюсь, что здесь вы найдете что-нибуть интересное!
+
+Вы читаете русскою версию моего сайта. Я только недавно занялся его переводом, и до этого времени редко писал на русском. Я заранеее извиняюсь за присутствие орфографических или грамматических ошибок.

content/blog/00_compiler_intro.ru.md

@@ -0,0 +1,97 @@
+---
+title: Пишем Компилятор Для Функционального Языка на С++, Часть 0 - Вступление
+date: 2019-08-03T01:02:30-07:00
+tags: ["C and C++", "Functional Languages", "Compilers"]
+description: "todo"
+---
+Год назад, я был записан на курс по компиляторам. Я ждал этого момента почти два учебных года: еще со времени школы меня интересовало создание языков программирования. Однако я был разочарован - заданный нам финальный проект полностью состоял из склеивания вместе написанных профессором кусочков кода. Склеив себе такой грустный компилятор, я не почувствовал бы никакой гордости. А я хотел бы гордиться всеми своими проектами.
+
+Вместо стандартного задания, я решил -- с разрешением профессора -- написать компилятор для ленивого функционального языка, используя отличную книгу Саймона Пейтона Джоунса, _Implementing functional languages: a tutorial_. На курсе мы пользовались С++, и мой проект не был исключением. Получился прикольный маленький язык, и теперь я хочу рассказать вам, как вы тоже можете создать ваш собственный функциональный язык.  
+
+### Примечание к Русской Версии
+Вы читаете русскою версию этой статьи. Оригинал ее был написан год назад, и с тех пор объем всей серии немного изменился. Я планировал описать только те части компилятора, которые я успел закончить и сдать профессору: лексический анализ, синтаксический разбор, мономорфную проверку типов, и компиляцию простых выражений с помощью LLVM. Закончив и описав все эти части, я решил продолжать разрабатывать компилятор, и описал сборку мусора, полиморфную проверку типов, полиморфные структуры данных, а также компиляцию более сложных выражений. Вместо того чтобы писать наивный перевод английской версии -- притворяясь что я не знаю о перемене моих планов -- я буду вносить в эту версию изменения соответствующие сегодняшнему состоянию компилятора. Части статей не затронутые этими изменениями я тоже не буду переводить слово в слово, иначе они будут звучать ненатурально. Тем не менее техническое содержание каждой статьи будет аналогично содержанию ее английской версии, и код будет тот же самый. 
+
+### Мотивация
+Начать эту серию меня подтолкнули две причины. 
+
+Во-первых, почти все учебники и вступления к созданию компиляторов, с которыми я сталкивался, были написаны об императивных языках, часто похожих на C, C++, Python, или JavaScript. Я считаю, что в компиляции функциональных языков -- особенно ленивых -- есть много чего интересного, и все это относительно редко упоминается. 
+
+Во-вторых, меня вдохновили книги, как Software Foundations. Все содержание Software Foundations, например, написано в форме комментариев языка Coq. Таким образом, можно не только читать саму книгу, но и сразу же запускать находящийся рядом с комментариями код. Когда описываемый код под рукой, легче экспериментировать и интереснее читать. Принимая это во внимание, я выкладываю вместе с каждой статьей соответствующую версию компилятора; в самой статье описывается код именно из этой версии. Все части написанной мною программы полностью доступны. 
+
+### Обзор
+Прежде чем начинать наш проект, давайте обсудим, чего мы будем добиваться, и какими способами. 
+
+#### “Классические” Стадии Компилятора
+Части большинства компиляторов достаточно независимы друг от друга (по крайней мере в теории). Мы можем разделить их на следующие шаги:
+
+* Лексический анализ
+* Синтаксический разбор
+* Анализ и оптимизация
+* Генерация кода
+
+Не все вышеописанные шаги встречаются в каждом компиляторе. Например, компилятор в моих статьях совсем не оптимизирует код. Также, в некоторых компиляторах присутствуют шаги не упомянутые в этом списке. Язык Idris  -- как и многие другие функциональные языки -- переводится сначала в упрощённый язык “TT”, и только после этого проходит через анализ. Иногда, с целью ускорить компиляцию, несколько шагов производятся одновременно. В целом, все эти стадии помогут нам сориентироваться, но никаким образом нас не ограничат.  
+
+#### Темы, Которые Мы Рассмотрим
+Мы начнем с нуля, и пошагово построим компилятор состоящий из следующих частей:
+
+* Лексического анализа с помощью программы Flex.
+* Синтаксического разбора с помощью программы Bison.
+* Сначала мономорфной, а позже полиморфной проверки типов.
+* Вычисления программ используя абстрактную машину G-machine.
+* Компиляции абстрактных инструкций G-machine используя LLVM.
+* Простого сбора мусора.
+
+Наша цель - создать ленивый, функциональный язык.
+
+#### Темы, Которые Мы Не Рассмотрим
+Для того, чтобы создать любую нетривиальную программу, нужно иметь значительный объем опыта и знаний; одному человеку было бы сложно научить всему этому. У меня буквально не хватило бы на это времени, да и исход такой попытки был бы неблагоприятным: опытным читателям было бы труднее извлечь из статей новую информацию, а неопытным читателям все равно было бы недостаточно подробно. Вместо того, чтобы портить таким образом свои статьи, я буду полагаться на то, что вы достаточно комфортно себя чувствуете с некоторыми темами. В число этих тем входят:
+
+* [Теория алгоритмов](https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B0%D0%BB%D0%B3%D0%BE%D1%80%D0%B8%D1%82%D0%BC%D0%BE%D0%B2),
+более конкретно [теория автоматов](https://ru.wikipedia.org/wiki/%D0%A2%D0%B5%D0%BE%D1%80%D0%B8%D1%8F_%D0%B0%D0%B2%D1%82%D0%BE%D0%BC%D0%B0%D1%82%D0%BE%D0%B2).
+Детерминированные и недетерминированные автоматы кратко упоминаются в первой статье во время лексического анализа, a синтаксический разбор мы выполним используя контекстно-свободную грамматику.
+* [Функциональное программирование](https://ru.wikipedia.org/wiki/%D0%A4%D1%83%D0%BD%D0%BA%D1%86%D0%B8%D0%BE%D0%BD%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B8%D1%80%D0%BE%D0%B2%D0%B0%D0%BD%D0%B8%D0%B5), с легкой примесью [лямбда-исчисления](https://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%B8%D1%81%D1%87%D0%B8%D1%81%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5).
+Мы будем пользоваться лямбда-функциями, каррированием, и системой типов Хиндли-Мильнер, которая часто встречается в языках семейства ML.
+* С++. Я стараюсь писать код правильно и по последним стандартам, но я не эксперт. Я не буду объяснять синтаксис или правила С++, но разумеется буду описывать что именно делает мой код с точки зрения компиляторов.
+
+#### Синтаксис Нашего Языка
+Саймон Пейтон Джоунс, в одном из своих [~~двух~~ многочисленных](https://www.reddit.com/r/ProgrammingLanguages/comments/dsu115/compiling_a_functional_language_using_c/f6t52mh?utm_source=share&utm_medium=web2x&context=3) трудов на тему функциональных языков, отметил что большинство из этих языков по сути очень похожи друг на друга; часто, главная разница состоит именно в их синтаксисе. На данный момент, выбор синтаксиса - наша главная степень свободы. Нам точно нужно предоставить доступ к следующим вещам:
+
+* Декларациям функций
+* Вызову функций
+* Арифметике
+* Aлгебраическим типам данных
+* Сопоставлению с образцом
+
+Позже, мы добавим к этому списку выражения let/in и лямбда-функции. С арифметикой разобраться не сложно - числа будут писаться просто как `3`, значения выражений как `1+2*3` будут высчитываться по обычным математическим правилам. Вызов функций ненамного сложнее. Выражение `f x` будет значить “вызов функции `f` с параметром `x`”, а `f x + g y` - “сумма значений `f x` и `g y`”. Заметьте, что вызов функций имеет приоритет выше приоритета арифметических операций.
+
+Теперь давайте придумаем синтаксис для деклараций функций. Я предлогаю следующий вариант:
+
+```
+defn f x = { x + x }
+```
+
+А для типов данных:
+
+```
+data List = { Nil, Cons Int List }
+```
+
+Заметьте, что мы пока пользуемся мономорфными декларациями типов данных. Позже, в одиннадцатой части, мы добавим синтаксис для полиморфных деклараций.
+
+В последнюю очередь, давайте определимся с синтаксисом сопоставления с образцом:
+
+```
+case l of {
+    Nil -> { 0 }
+    Cons x xs -> { x }
+}
+```
+
+Представленная выше распечатка читается как: “если лист `l` сопоставим с `Nil`, то все выражение возвращает значение `0`; иначе, если лист сопоставим с `Cons x xs` (что, опираясь на декларацию `List`, означает, что лист состоит из значений `x`, с типом `Int`, и `xs`, с типом `List`), то выражение возвращает `x`”.   
+
+Вот и конец нашего обзора! В следующей статье, мы начнем с лексического анализа, что является первым шагом в процессе трансформации программного текста в исполняемые файлы.
+
+### Список Статей
+* Ой! Тут как-то пусто.
+* Вы, наверно, читаете черновик.
+* Если нет, то пожалуйста напишите мне об этом!

content/blog/dell_is_horrible/index.md

@@ -1,7 +1,6 @@
 ---
 title: DELL Is A Horrible Company And You Should Avoid Them At All Costs
-date: 2020-07-17T16:23:34-07:00
-draft: true
+date: 2020-07-23T13:40:05-07:00
 tags: ["Electronics"]
 ---
 
@@ -230,13 +229,10 @@ I admit, I was angry. At the same time, the absurdity of it all was also
 unbearable. Was this constant loop of hardware damage, the endless number of
 support calls filled with hoarse jazz music, part of some kind of Kafkaesque
 dream? I didn't know. I was at the end of my wits as to what to do. As a last
-resort, I made a tweet from my almost-abandoned account. DELL Support's Twitter
-account quickly responded, eager as always to destroy any semblance of
-transparency by switching to private messages:
-
-{{< tweet 1268064691416334344 >}}
-
-I let them know my thoughts on the matter. I wanted a new machine.
+resort, I made [a tweet](https://twitter.com/DanilaTheWalrus/status/1268056637383692289)
+from my almost-abandoned account. DELL Support's Twitter
+account [quickly responded](https://twitter.com/DellCares/status/1268064691416334344), eager as always to destroy any semblance of
+transparency by switching to private messages. I let them know my thoughts on the matter. I wanted a new machine.
 
 {{< figure src="dm_1.png" caption="The first real exchange between me and DELL support." >}}
 
@@ -261,7 +257,8 @@ paper which included my name and email address. I obliged, and quickly got a res
 
 {{< figure src="dm_3.png" caption="If it was me who was silent for 4 days, my request would've long been cancelled. " >}}
 
-Thanks, Kalpana. Try to remember that name; you will never hear it again, not in this post.
+Thanks, Kalpana. You will never hear this name again, not in this post.
+Only one or two messages from DELL support are ever from the same person.
 About a week later, I get the following beauty:
 
 {{< figure src="dm_4.png" caption="Excuse me? What's going on?" >}}

content/blog/haskell_lazy_evaluation/index.md

@@ -1,8 +1,7 @@
 ---
 title: "Time Traveling In Haskell: How It Works And How To Use It"
-date: 2020-05-03T20:05:29-07:00
+date: 2020-07-30T00:58:10-07:00
 tags: ["Haskell"]
-draft: true
 ---
 
 I recently got to use a very curious Haskell technique
@@ -10,8 +9,7 @@ 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 (which isn't
-interesting enough to be presented here in itself), and so
+magic for the problem I was trying to solve, 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
@@ -69,7 +67,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; however, thus far, it looks like wishful
+given to us; it just looks like wishful
 thinking. The real magic happens in Csongor's `doRepMax`
 function:
 
@@ -95,8 +93,9 @@ 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 graph. Graphs that
-refer to themselves also violate the properties of a tree.
+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.
 {{< /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
@@ -126,7 +125,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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="length_1.png" caption="The initial graph of `length [1]`." class="small" >}}
 
 In this image, the `@` nodes represent function application. The
 root node is an application of the function `length` to the graph that
@@ -137,7 +136,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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="length_2.png" caption="The graph of `length [1]` after the body of `length` is expanded." class="small" >}}
 
 Conceptually, we only took one reduction step, and thus, we haven't yet gotten
 to evaluating the recursive call to `length`. Since `(+)`
@@ -169,17 +168,17 @@ let x = square 5 in x + x
 
 Here, the initial graph looks as follows:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="square_1.png" caption="The initial graph of `let x = square 5 in x + x`." class="small" >}}
 
-As you can see, this _is_ a graph, not a tree! Since both
+As you can see, this _is_ a graph, but 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="square_2.png" caption="The graph of `let x = square 5 in x + x` after `square 5` is reduced." class="small" >}}
 
-There are two `25`s in the tree, and no more `square`s! We only
+There are two `25`s in the graph, 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).
 
@@ -202,21 +201,22 @@ 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="fixpoint_1.png" caption="The initial graph of `let x = f x in x`." class="tiny" >}}
 
 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="fixpoint_2.png" caption="The graph of `fix (1:)` after it's been reduced." class="small" >}}
 
 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. 
+thereby creating a cycle in our graph. Traversing this graph looks like
+traversing an infinite list of `1`s.
 
 Almost there! A node can refer to itself, and, when evaluated, it
 is replaced with its own value. Thus, a node can effectively reference
@@ -232,7 +232,7 @@ doRepMax xs = snd t
   where t = repMax xs (fst t)
 ```
 
-### Detailed Example: Reducing `doRepMax`
+#### Detailed Example: Reducing `doRepMax`
 
 If the above examples haven't elucidated how `doRepMax` works,
 stick around in this section and we will go through it step-by-step.
@@ -247,25 +247,23 @@ 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="notation.png" caption="The new visual notation used in this section." class="small" >}}
 
 Now, let's write the initial graph for `doRepMax [1,2]`:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_1.png" caption="The initial graph of `doRepMax [1,2]`." class="small" >}}
 
 Other than our new notation, there's nothing too surprising here.
-At a high level, all we want is the second element of the tuple
+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
 returned by `repMax`, which contains the output list. To get
-the tuple, we apply `repMax` to the list `[1,2]`, which itself
+the tuple, we apply `repMax` to the list `[1,2]` and the first element
+of its result. The list `[1,2]` itself
 consists of two uses of the `(:)` function.
 
-The first step
-of our hypothetical reduction would replace the application of `doRepMax` with its
-body, and create our graph's first cycle:
+{{< figure src="repmax_2.png" caption="The first step of reducing `doRepMax [1,2]`." class="small" >}}
 
-{{< todo >}}Add image!{{< /todo >}}
-
-Next, we would do the same for the body of `repMax`. In
+Next, we would also expand 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
@@ -273,7 +271,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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_3.png" caption="The second step of reducing `doRepMax [1,2]`." class="medium" >}}
 
 Since `(,)` is a constructor, let's say that it doesn't
 need to be evaluated, and that its
@@ -289,9 +287,11 @@ thus replace the application of `snd` with an
 indirection to this subgraph. This leaves us
 with the following:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_4.png" caption="The third step of reducing `doRepMax [1,2]`." class="medium" >}}
 
-If our original `doRepMax [1, 2]` expression occured at the top level,
+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,
 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`:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_5.png" caption="The fourth step of reducing `doRepMax [1,2]`." class="medium" >}}
 
 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_6.png" caption="The fifth step of reducing `doRepMax [1,2]`." class="medium" >}}
 
 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, this is easy.
+of the arguments to `max`. Given this graph, doing so 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_7.png" caption="The sixth step of reducing `doRepMax [1,2]`." class="medium" >}}
 
 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`:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_8.png" caption="The seventh step of reducing `doRepMax [1,2]`." class="medium" >}}
 
 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,48 +351,214 @@ 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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_9.png" caption="The eighth step of reducing `doRepMax [1,2]`." class="medium" >}}
 
 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 head. This argument is a reference to
+first argument of this list, which is the list's 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,
-and we're left with the following graph:
+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:
 
-{{< todo >}}Add image!{{< /todo >}}
+{{< figure src="repmax_10.png" caption="The result of reducing `doRepMax [1,2]`." class="small" >}}
 
-As we would have expected, two `2`s are printed to the console.
+As we would have expected, two `2`s were printed to the console, and our
+final graph represents the list `[2,2]`.
 
 ### Using Time Traveling
+Is time tarveling even useful? I would argue yes, especially
+in cases where Haskell's purity can make certain things
+difficult.
 
-{{< todo >}}This whole section {{< /todo >}}
+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, which my
+coworker and coauthor Kai helped me formulate. 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).
 
 ### 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:
 
-{{< todo >}}This whole section, too. {{< /todo >}}
+{{< codelines "Haskell" "time-traveling/TakeMax.hs" 1 12 >}}
 
-### Leftovers
+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.
 
-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.
+Unfortunately, this doesn't work; our program never terminates.
+You may be thinking:
 
-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:
+> 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.
 
-```
->>> countMaxFactors [1,3,3,9]
+To address this, we can reformulate our `takeUntilMax`
+function as follows:
 
-fromList [(1, 1), (3, 2), (9, 1)]
-```
+{{< codelines "Haskell" "time-traveling/TakeMax.hs" 14 21 >}}
 
+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!

content/blog/typesafe_interpreter_revisited.md

@@ -1,7 +1,6 @@
 ---
 title: Meaningfully Typechecking a Language in Idris, Revisited
-date: 2020-07-19T17:19:02-07:00
-draft: true
+date: 2020-07-22T14:37:35-07:00
 tags: ["Idris"]
 ---
 
@@ -43,7 +42,7 @@ Let's start with the new `Expr` and `SafeExpr` types. Here they are:
 
 For `Expr`, the `IfElse` constructor is very straightforward. It takes
 three expressions: the condition, the 'then' branch, and the 'else' branch.
-With `SafeExpr` and `IfThneElse`, things are more rigid. The condition
+With `SafeExpr` and `IfThenElse`, things are more rigid. The condition
 of the expression has to be of a boolean type, so we make the first argument
 `SafeExpr BoolType`. Also, the two branches of the if-expression have to
 be of the same type. We encode this by making both of the input expressions
@@ -212,7 +211,7 @@ We can therefore write:
 replace'' : {x : ExprType} -> {y : ExprType} -> x = y -> SafeExpr x -> SafeExpr y
 ```
 
-This is exactly what we want! Given a proof that one `ExprType`, `x` is equal to
+This is exactly what we want! Given a proof that one `ExprType`, `x`, is equal to
 another `ExprType`, `y`, we can safely convert `SafeExpr x` to `SafeExpr y`.
 We will use this to convince the Idris typechecker to accept our program.
 
@@ -362,14 +361,15 @@ I think this is a good approach. Should we want to add more types to our languag
 lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality
 proofs, and keep the `typecheck` method the same. Had we not used this approach,
 and instead decided to pattern match on types inside of `typecheck`, we would've quickly
-found that this only works for types with finitely many values. When we add polymorphic tuples
+found that this only works for languages with finitely many types. When we add polymorphic tuples
 and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
 so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive
 solution. I think that this leads us back to `decEq`.
 
 I also hope that I've now redeemed myself as far as logical arguments go. We used dependent types
 and made our typechecking function save us from error-checking during evaluation. We did this
-without having to manually create different types of expressions like `ArithExpr` and `BoolExpr`.
+without having to manually create different types of expressions like `ArithExpr` and `BoolExpr`,
+and without having to duplicate any code.
 
 That's all I have for today, thank you for reading! As always, you can check out the
 [full source code for the typechecker and interpreter](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntrV2.idr) on my Git server.

content/blog/typesafe_interpreter_tuples.md

@@ -0,0 +1,216 @@
+---
+title: Meaningfully Typechecking a Language in Idris, With Tuples
+date: 2020-08-12T15:48:04-07:00
+tags: ["Idris"]
+---
+
+Some time ago, I wrote a post titled
+[Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}).
+I then followed it up with
+[Meaningfully Typechecking a Language in Idris, Revisited]({{< relref "typesafe_interpreter_revisited.md" >}}).
+In these posts, I described a hypothetical
+way of 'typechecking' an expression data type `Expr` into a typesafe form `SafeExpr`.
+A `SafeExpr` can be evaluated without any code to handle type errors,
+since it's by definition impossible to construct ill-typed expressions using
+it. In the first post, we implemented the method only for simple arithmetic
+expressions; in my latter post, we extended this to support `if`-expressions.
+Near the end of the post, I made the following comment:
+
+> When we add polymorphic tuples and lists, we start being able to construct an
+arbitrary number of types: `[a]`. `[[a]]`, and so on. Then, we cease to be able t
+enumerate all possible pairs of types, and require a recursive solution. I think
+that this leads us back to [our method].
+
+Recently, I thought about this some more, and decided that it's rather simple
+to add tuples into our little language. The addition of tuples mean that our
+language will have an infinite number of possible types. We would have
+`Int`, `(Int, Int)`, `((Int, Int), Int)`, and so on. This would make it
+impossible to manually test every possible case in our typechecker,
+but our approach of returning `Dec (a = b)` will work just fine.
+
+### Extending The Syntax
+First, let's extend our existing language with expressions for
+tuples. For simplicity, let's use pairs `(a,b)` instead of general
+`n`-element tuples. This would make typechecking less cumbersome while still
+having the interesting effect of making the number of types in our language
+infinite. We can always represent the 3-element tuple `(a,b,c)` as `((a,b), c)`,
+after all. To be able to extract values from our pairs, we'll add the `fst` and
+`snd` functions into our language, which accept a tuple and return its
+first or second element, respectively.
+
+Our `Expr` data type, which allows ill-typed expressions, ends up as follows:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 31 39 "hl_lines=7 8 9" >}}
+
+I've highlighted the new lines. The additions consist of the `Pair` constructor, which
+represents the tuple expression `(a, b)`, and the `Fst` and `Snd` constructors,
+which represent the `fst e` and `snd e` expressions, respectively. In
+a similar manner, we extend our `SafeExpr` GADT:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 41 49 "hl_lines=7 8 9" >}}
+
+Finally, to provide the `PairType` constructor, we extend the `ExprType` and `repr` functions:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 1 11 "hl_lines=5 11" >}}
+
+### Implementing Equality
+An important part of this change is the extension of the `decEq` function,
+which compares two types for equality. The kind folks over at `#idris` previously
+recommended the use of the `Dec` data type for this purpose. A value of
+type `Dec P`
+{{< sidenote "right" "decideable-note" "is either a proof that \(P\) is true, or a proof that \(P\) is false." >}}
+It's possible that a proposition \(P\) is not provable, and neither is \(\lnot P\).
+It is therefore not possible to construct a value of type <code>Dec P</code> for
+any proposition <code>P</code>. Having a value of type <code>Dec P</code>, then,
+provides us nontrivial information.
+{{< /sidenote >}} Our `decEq` function, given two types `a` and `b`, returns
+`Dec (a = b)`. Thus, it will return either a proof that `a = b` (which we can
+then use to convince the Idris type system that two `SafeExpr` values are,
+in fact, of the same type), or a proof of `a = b -> Void` (which tells
+us that `a` and `b` are definitely not equal). If you're not sure what the deal with `(=)`
+and `Void` is, check out
+[this section]({{< relref "typesafe_interpreter_revisited.md" >}}#curry-howard-correspondence)
+of the previous article.
+
+A lot of the work in implementing `decEq` went into constructing proofs of falsity.
+That is, we needed to explicitly list every case like `decEq IntType BoolType`, and create
+a proof that `IntType` cannot equal `BoolType`. However, here's how we use `decEq` in
+the typechecking function:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 76 78 >}}
+
+We always throw away the proof inequality! So, rather than spending the time
+constructing useless proofs like this, we can just switch `decEq` to return
+a `Maybe (a = b)`. The `Just` case will tell us that the two types are equal
+(and, as before, provide a proof); the `Nothing` case will tell us that
+the two types are _not_ equal, and provide no further information. Let's
+see the implementation of `decEq` now:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 13 23 >}}
+
+Lines 14 through 16 are pretty simple; in this case, we can tell at a glance
+that the two types are equal, and Idris can infer an equality proof in
+the form of `Refl`. We return this proof by writing it in a `Just`.
+Line 23 is the catch-all case for any combination of types we didn't handle.
+Any combination of types we don't handle is invalid, and thus, this case
+returns `Nothing`.
+
+What about lines 17 through 22? This is the case for handling the equality
+of two pair types, `(lt1, lt2)` and `(rt1, rt2)`. The equality of the two
+types depends on the equality of their constituents. That is, if we
+know that `lt1 = rt1` and `lt2 = rt2`, we know that the two pair types
+are also equal. If one of the two equalities doesn't hold, the two
+pairs obviously aren't equal, and thus, we should return `Nothing`.
+This should remind us of `Maybe`'s monadic nature: we can first compute
+`decEq lt1 rt1`, and then, if it succeeds, compute `decEq lt2 rt2`.
+If both succeed, we will have in hand the two proofs, `lt1 = rt1`
+and `lt2 = rt2`. We achieve this effect using `do`-notation,
+storing the sub-proofs into `subEq1` and `subEq2`.
+
+What now? Once again, we have to use `replace`. Recall its type:
+
+```Idris
+replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
+```
+
+Given some proposition in terms of `a`, and knowing that `a = b`, `replace`
+returns the original proposition, but now in terms of `b`. We know for sure
+that:
+
+```Idris
+PairType lt1 lt2 = PairType lt1 lt2
+```
+
+We can start from there. Let's handle one thing at a time, and try
+to replace the second `lt1` with `rt1`. Then, we can replace the second
+`lt2` with `rt2`, and we'll have our equality!
+
+Easier said than done, though. How do we tell Idris which `lt1`
+we want to substitute? After all, of the following are possible:
+
+```Idris
+PairType rt1 lt2 = PairType lt1 lt2 -- First lt1 replaced
+PairType lt1 lt2 = PairType rt1 lt2 -- Second lt1 replaced
+PairType rt1 lt2 = PairType rt1 lt2 -- Both replaced
+```
+
+The key is in the signature, specifically the expressions `P x` and `P y`.
+We can think of `P` as a function, and of `replace` as creating a value
+of `P` applied to another argument. Thus, the substitution will occur
+exactly where the argument of `P` is used. Then, to achieve each
+of the above substitution, we can write `P` as follows:
+
+```Idris {linenos=table, hl_lines=[2]}
+t1 => PairType t1 lt2 = PairType lt1 lt2
+t1 => PairType lt1 lt2 = PairType t1 lt2
+t1 => PairType t1 lt2 = PairType t1 lt2
+```
+
+The second function (highlighted) is the one we'll need to use to attain
+the desired result. Since `P` is an implicit argument to `replace`,
+we can explicitly provide it with `{P=...}`, leading to the following
+line:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 20 20>}}
+
+We now have a proof of the following proposition:
+
+```Idris
+PairType lt1 lt2 = PairType rt1 lt2
+```
+
+We want to replace the second `lt2` with `rt2`, which means that we
+write our `P` as follows:
+
+```Idris
+t2 => PairType lt1 lt2 = PairType rt1 t2
+```
+
+Finally, we perform the second replacement, and return the result:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 21 22 >}}
+
+Great! We have finished implement `decEq`.
+
+### Adjusting The Typechecker
+It's time to make our typechecker work with tuples.
+First, we need to fix the `IfElse` case to accept `Maybe (a=b)` instead
+of `Dec (a=b)`:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 71 78 "hl_lines=7 8" >}}
+
+Note that the only change is from `Dec` to `Maybe`; we didn't need to add new cases
+or even to know what sort of types are available in the language.
+
+Next, we can write the cases for the new expressions in our language. We can
+start with `Pair`, which, given expressions of types `a` and `b`, creates
+an expression of type `(a,b)`. As long as the arguments to `Pair` are well-typed,
+so is the `Pair` expression itself; thus, there are no errors to handle.
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 79 83 >}}
+
+The case for `Fst` is more complicated. If the argument to `Fst` is a tuple
+of type `(a, b)`, then `Fst` constructs from it an expression
+of type `a`. Otherwise, the expression is ill-typed, and we return an error.
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 84 89 >}}
+
+The case for `Snd` is very similar:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 90 96 >}}
+
+### Evaluation Function and Conclusion
+We conclude with our final `eval` and `resultStr` functions,
+which now look as follows.
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 97 111 "hl_lines=7-9 13-15" >}}
+
+As you can see, we require no error handling in `eval`; the expressions returned by
+`typecheck` are guaranteed to evaluate to valid Idris values. We have achieved our goal,
+with very little changes to `typecheck` other than the addition of new language
+constructs. In my opinion, this is a win!
+
+As always, you can see the code on my Git server. Here's
+[the latest Idris file,](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntrV3.idr)
+if you want to check it out (and maybe verify that it compiles). I hope you found
+this interesting!

themes/vanilla/assets/scss/code.scss

@@ -0,0 +1,78 @@
+@import "variables.scss";
+
+$code-color-lineno: grey;
+$code-color-keyword: black;
+$code-color-type: black;
+$code-color-comment: grey;
+
+code {
+  font-family: $font-code;
+  background-color: $code-color;
+  border: $code-border;
+  padding: 0 0.25rem 0 0.25rem;
+}
+
+pre code {
+    display: block;
+    box-sizing: border-box;
+    padding: 0.5rem;
+    overflow: auto;
+}
+
+.chroma {
+    .lntable {
+        border-spacing: 0;
+        padding: 0.5rem 0 0.5rem 0;
+        background-color: $code-color;
+        border-radius: 0;
+        border: $code-border;
+        display: block;
+        overflow: auto;
+
+        td {
+            padding: 0;
+        }
+
+        code {
+            border: none;
+            padding: 0;
+        }
+
+        pre {
+            margin: 0;
+        }
+
+        .lntd:last-child {
+            width: 100%;
+        }
+    }
+
+    .lntr {
+        display: table-row;
+    }
+
+    .lnt {
+        display: block;
+        padding: 0 1rem 0 1rem;
+        color: $code-color-lineno;
+    }
+
+    .hl {
+        display: block;
+        background-color: #fffd99; 
+    }
+}
+
+.kr, .k {
+    font-weight: bold;
+    color: $code-color-keyword;
+}
+
+.kt {
+    font-weight: bold;
+    color: $code-color-type;
+}
+
+.c, .c1 {
+    color: $code-color-comment;   
+}

themes/vanilla/assets/scss/style.scss

@@ -31,31 +31,6 @@ h1, h2, h3, h4, h5, h6 {
   }
 }
 
-code {
-  font-family: $font-code;
-  background-color: $code-color;
-}
-
-pre code {
-    display: block;
-    padding: 0.5rem;
-    overflow-x: auto;
-    border: $code-border;
-}
-
-div.highlight table {
-    border: $code-border !important;
-    border-radius: 0px;
-
-    pre {
-        margin: 0;
-    }
-
-    code {
-        border: none;
-    }
-}
-
 .container {
   position: relative;
   margin: auto;
@@ -241,6 +216,18 @@ figure {
     figcaption {
         text-align: center;
     }
+
+    &.tiny img {
+        max-height: 15rem;
+    }
+
+    &.small img {
+        max-height: 20rem;
+    }
+
+    &.medium img {
+        max-height: 30rem;
+    }
 }
 
 .twitter-tweet {

themes/vanilla/i18n/en.toml

@@ -0,0 +1,35 @@
+[Home]
+other = "Home"
+
+[About]
+other = "About"
+
+[Resume]
+other = "Resume"
+
+[Tags]
+other = "Tags"
+
+[RecentPosts]
+other = "Recent posts"
+
+[AllPosts]
+other = "All Posts"
+
+[PostedOn]
+other = "Posted on {{ .Date.Format \"January 2, 2006\" }}."
+
+[TableOfContents]
+other = "Table of Contents"
+
+[ReadingTime]
+other = "{{ .WordCount }} words, about {{ .ReadingTime }} minutes to read."
+
+[Note]
+other = "note"
+
+[Tagged]
+other = "Tagged \"{{ .Title }}\""
+
+[AllTags]
+other = "Below is a list of all the tags ever used on this site."

themes/vanilla/i18n/ru.toml

@@ -0,0 +1,35 @@
+[Home]
+other = "Главная"
+
+[About]
+other = "О Сайте"
+
+[Resume]
+other = "Резюме"
+
+[Tags]
+other = "Метки"
+
+[RecentPosts]
+other = "Недавние статьи"
+
+[AllPosts]
+other = "Все Статьи"
+
+[PostedOn]
+other = "Статья опубликована {{ .Date.Format \"January 2, 2006\" }}."
+
+[TableOfContents]
+other = "Оглавление"
+
+[ReadingTime]
+other = "{{ .WordCount }} слов, чтение займет примерно {{ .ReadingTime }} минут."
+
+[Note]
+other = "примечание"
+
+[Tagged]
+other = "Статьи c меткой \"{{ .Title }}\""
+
+[AllTags]
+other = "Ниже приводится список всех меток на сайте."

themes/vanilla/layouts/blog/single.html

@@ -6,14 +6,14 @@
         <a class="button" href="{{ $.Site.BaseURL }}/tags/{{ . | urlize }}">{{ . }}</a>
         {{ end }}
     </p>
-    <p>Posted on {{ .Date.Format "January 2, 2006" }}.</p>
+    <p>{{ i18n "PostedOn" . }}</p>
 </div>
 
 <div class="post-content">
     {{ if not (eq .TableOfContents "<nav id=\"TableOfContents\"></nav>") }}
     <div class="table-of-contents">
         <div class="wrapper">
-            <em>Table of Contents</em>
+            <em>{{ i18n "TableOfContents" }}</em>
             {{ .TableOfContents }}
         </div>
     </div>

themes/vanilla/layouts/index.html

@@ -1,7 +1,7 @@
 {{ define "main" }}
 {{ .Content }}
 
-Recent posts:
+{{ i18n "RecentPosts" }}:
 <ul class="post-list">
     {{ range first 10 (where (where .Site.Pages.ByDate.Reverse "Section" "blog") ".Kind" "!=" "section") }}
     {{ partial "post.html" . }}

themes/vanilla/layouts/partials/head.html

@@ -6,14 +6,16 @@
     <meta name="description" content="{{ .Description }}">
     {{ end }}
 
-    <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata&family=Raleway&family=Lora&display=block" media="screen"> 
+    <link rel="stylesheet" href="https://fonts.googleapis.com/css2?family=Inconsolata:wght@400;700&family=Raleway&family=Lora&display=block" media="screen"> 
     <link rel="stylesheet" href="//cdnjs.cloudflare.com/ajax/libs/normalize/5.0.0/normalize.min.css" media="screen">
     {{ $style := resources.Get "scss/style.scss" | resources.ToCSS | resources.Minify }}
     {{ $sidenotes := resources.Get "scss/sidenotes.scss" | resources.ToCSS | resources.Minify }}
+    {{ $code := resources.Get "scss/code.scss" | resources.ToCSS | resources.Minify }}
     {{ $icon := resources.Get "img/favicon.png" }}
     {{- partial "sidenotes.html" . -}}
     <link rel="stylesheet" href="{{ $style.Permalink }}" media="screen">
     <link rel="stylesheet" href="{{ $sidenotes.Permalink }}" media="screen">
+    <link rel="stylesheet" href="{{ $code.Permalink }}" media="screen">
     <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous" media="screen">
     <link rel="icon" type="image/png" href="{{ $icon.Permalink }}">
 

themes/vanilla/layouts/partials/header.html

@@ -3,11 +3,11 @@
 </div>
 <nav>
     <div class="container">
-        <a href="/">Home</a>
-        <a href="/about">About</a>
+        <a href="/">{{ i18n "Home" }}</a>
+        <a href="/about">{{ i18n "About" }}</a>
         <a href="https://github.com/DanilaFe">GitHub</a>
-        <a href="/Resume-Danila-Fedorin.pdf">Resume</a>
-        <a href="/tags">Tags</a>
-        <a href="/blog">All Posts</a>
+        <a href="/Resume-Danila-Fedorin.pdf">{{ i18n "Resume" }}</a>
+        <a href="/tags">{{ i18n "Tags" }}</a>
+        <a href="/blog">{{ i18n "AllPosts" }}</a>
     </div>
 </nav>

themes/vanilla/layouts/partials/post.html

@@ -1,5 +1,5 @@
 <li>
     <a href="{{ .Permalink }}" class="post-title">{{ .Title }}</a>
-    <p class="post-wordcount">{{ .WordCount }} words, about {{ .ReadingTime }} minutes to read.</p>
+    <p class="post-wordcount">{{ i18n "ReadingTime" . }}</p>
     <p class="post-preview">{{ .Summary }} . . .</p>
 </li>

themes/vanilla/layouts/shortcodes/codelines.html

@@ -6,4 +6,9 @@
 {{ .Scratch.Set "u" $t }}
 {{ end }}
 {{ $v := first (add (sub (int (.Get 3)) (int (.Get 2))) 1) (.Scratch.Get "u") }}
-{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d" (.Get 2)) }}
+{{ if (.Get 4) }}
+{{ .Scratch.Set "opts" (printf ",%s" (.Get 4)) }}
+{{ else }}
+{{ .Scratch.Set "opts" "" }}
+{{ end }}
+{{ highlight (delimit $v "\n") (.Get 0) (printf "linenos=table,linenostart=%d%s" (.Get 2) (.Scratch.Get "opts")) }}

themes/vanilla/layouts/shortcodes/numberedsidenote.html

@@ -4,7 +4,7 @@
 <label class="sidenote-label" for="numbernote-{{ $id }}">({{ $id }})</label>
 <input class="sidenote-checkbox" type="checkbox" id="numbernote-{{ $id }}"></input>
 <span class="sidenote-content sidenote-{{ .Get 0 }}">
-<span class="sidenote-delimiter">[note:</span>
+<span class="sidenote-delimiter">[{{ i18n "note" }}:</span>
 {{ .Inner }}
 <span class="sidenote-delimiter">]</span>
 </span>

themes/vanilla/layouts/shortcodes/sidenote.html

@@ -2,7 +2,7 @@
 <label class="sidenote-label" for="{{ .Get 1 }}">{{ .Get 2 }}</label>
 <input class="sidenote-checkbox" type="checkbox" id="{{ .Get 1 }}"></input>
 <span class="sidenote-content sidenote-{{ .Get 0 }}">
-<span class="sidenote-delimiter">[note:</span>
+<span class="sidenote-delimiter">[{{ i18n "Note" }}:</span>
 {{ .Inner }}
 <span class="sidenote-delimiter">]</span>
 </span>

themes/vanilla/layouts/tags/list.html

@@ -1,5 +1,5 @@
 {{ define "main" }}
-<h2>Tagged "{{ .Title }}"</h2>
+<h2>{{ i18n "Tagged" . }}</h2>
 
 <ul class="post-list">
     {{ range .Pages.ByDate.Reverse }}

themes/vanilla/layouts/tags/terms.html

@@ -1,6 +1,6 @@
 {{ define "main" }}
-<h2>{{ .Title }}</h2>
-Below is a list of all the tags ever used on this site.
+<h2>{{ i18n "Tags" }}</h2>
+{{ i18n "AllTags" }}
 
 <ul>
     {{ range sort .Pages "Title" }}