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

@@ -0,0 +1,99 @@
+data ExprType
+  = IntType
+  | BoolType
+  | StringType
+
+repr : ExprType -> Type
+repr IntType = Int
+repr BoolType = Bool
+repr StringType = String
+
+intBoolImpossible : IntType = BoolType -> Void
+intBoolImpossible Refl impossible
+
+intStringImpossible : IntType = StringType -> Void
+intStringImpossible Refl impossible
+
+boolStringImpossible : BoolType = StringType -> Void
+boolStringImpossible Refl impossible
+
+decEq : (a : ExprType) -> (b : ExprType) -> Dec (a = b)
+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
+  | Subtract
+  | Multiply
+  | Divide
+
+data Expr
+  = IntLit Int
+  | BoolLit Bool
+  | StringLit String
+  | BinOp Op Expr Expr
+  | IfElse Expr Expr 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
+
+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
+      Yes p => pure (_ ** IfThenElse ce (replace p te) ee)
+      No _ => Left "Incompatible branch types."
+
+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)
+
+resultStr : {t : ExprType} -> repr t -> String
+resultStr {t=IntType} i = show i
+resultStr {t=BoolType} b = show b
+resultStr {t=StringType} s = show s
+
+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 (IfElse (BoolLit True) (IntLit 6) (IntLit 7)) (BinOp Multiply (IntLit 160) (IntLit 2))

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/about.md

@@ -1,8 +1,8 @@
 ---
 title: About
 ---
-I'm Daniel, a Computer Science student currently in my third (and final) undergraduate year at Oregon State University.
-Due my initial interest in calculators and compilers, I got involved in the Programming Language Theory research
+I'm Daniel, a Computer Science student currently working towards my Master's Degree at Oregon State University.
+Due to my initial interest in calculators and compilers, I got involved in the Programming Language Theory research
 group, gaining same experience in formal verification, domain specific language, and explainable computing.
 
 For work, school, and hobby projects, I use a variety of programming languages, most commonly C/C++,

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/backend_math_rendering.md

@@ -0,0 +1,304 @@
+---
+title: Rendering Mathematics On The Back End
+date: 2020-07-21T14:54:26-07:00
+tags: ["Website", "Nix", "Ruby", "KaTeX"]
+---
+
+Due to something of a streak of bad luck when it came to computers, I spent a
+significant amount of time using a Linux-based Chromebook, and then a
+Pinebook Pro. It was, in some way, enlightening. The things that I used to take
+for granted with a 'powerful' machine now became a rare luxury: StackOverflow,
+and other relatively static websites, took upwards of ten seconds to finish
+loading. On Slack, each of my keypresses could take longer than 500ms to
+appear on the screen, and sometimes, it would take several seconds. Some
+websites would present me with a white screen, and remain that way for much
+longer than I had time to wait. It was awful.
+
+At one point, I installed uMatrix, and made it the default policy to block
+all JavaScript. For the most part, this worked well. Of course, I had to
+enable JavaScript for applications that needed to be interactive, like
+Slack, and Discord. But for the most part, I was able to browse the majority
+of the websites I normally browse. This went on until I started working
+on the [compiler series]({{< relref "00_compiler_intro.md" >}}) again,
+and discovered that the LaTeX math on my page, which was required
+for displaying things like inference rules, didn't work without
+JavaScript. I was left with two options:
+
+* Allow JavaScript, and continue using MathJax to render my math.
+* Make it so that the mathematics are rendered on the back end.
+
+I've [previously written about math rendering]({{< relref "math_rendering_is_wrong.md" >}}),
+and made the observation that MathJax's output for LaTeX is __identical__
+on every computer. From the MathJax 2.6 change log:
+
+> _Improved CommonHTML output_. The CommonHTML output now provides the same layout quality and MathML support as the HTML-CSS and SVG output. It is on average 40% faster than the other outputs and the markup it produces are identical on all browsers and thus can also be pre-generated on the server via MathJax-node.
+
+It seems absurd, then, to offload this kind of work into the users, to
+be done over and over again. As should be clear from the title of
+this post, this made me settle for the second option: it was
+__obviously within reach__, especially for a statically-generated website
+like mine, to render math on the backend.
+
+I settled on the following architecture:
+
+* As before, I would generate my pages using Hugo.
+* I would use the KaTeX NPM package to render math.
+* To build the website no matter what system I was on, I would use Nix.
+
+It so happens that Nix isn't really required for using my approach in general.
+I will give my setup here, but feel free to skip ahead.
+
+### Setting Up A Nix Build
+My `default.nix` file looks like this:
+
+```Nix {linenos=table}
+    { stdenv, hugo, fetchgit, pkgs, nodejs, ruby }:
+
+    let
+        url = "https://dev.danilafe.com/Web-Projects/blog-static.git";
+        rev = "<commit>";
+        sha256 = "<hash>";
+        requiredPackages = import ./required-packages.nix {
+            inherit pkgs nodejs;
+        };
+    in
+        stdenv.mkDerivation {
+            name = "blog-static";
+            version = rev;
+            src = fetchgit {
+                inherit url rev sha256;
+            };
+            builder = ./builder.sh;
+            converter = ./convert.rb;
+            buildInputs = [
+                hugo
+                requiredPackages.katex
+                (ruby.withPackages (ps: [ ps.nokogiri ]))
+            ];
+        }
+```
+
+I'm using `node2nix` to generate the `required-packages.nix` file, which allows me,
+even from a sandboxed Nix build, to download and install `npm` packages. This is needed
+so that I have access to the `katex` binary at build time. I fed the following JSON file
+to `node2nix`:
+
+```JSON {linenos=table}
+[
+    "katex"
+]
+```
+
+The Ruby script I wrote for this (more on that soon) required the `nokogiri` gem, which
+I used for traversing the HTML generated for my site. Hugo was obviously required to
+generate the HTML.
+
+### Converting LaTeX To HTML
+After my first post complaining about the state of mathematics on the web, I received
+the following email (which the author allowed me to share):
+
+> Sorry for having a random stranger email you, but in your blog post
+[(link)](https://danilafe.com/blog/math_rendering_is_wrong) you seem to focus on MathJax's
+difficulty in rendering things server-side, while quietly ignoring that KaTeX's front
+page advertises server-side rendering. Their documentation [(link)](https://katex.org/docs/options.html)
+even shows (at least as of the time this email was sent) that it renders both HTML
+(to be arranged nicely with their CSS) for visuals and MathML for accessibility.
+
+The author of the email then kindly provided a link to a page they generated using KaTeX and
+some Bash scripts. The math on this page was rendered at the time it was generated.
+
+This is a great point, and KaTeX is indeed usable for server-side rendering. But I've
+seen few people who do actually use it. Unfortunately, as I pointed out in my previous post on the subject,
+few tools actually take your HTML page and replace LaTeX with rendered math.
+Here's what I wrote about this last time:
+
+> [In MathJax,] The bigger issue, though, was that the `page2html`
+program, which rendered all the mathematics in a single HTML page,
+was gone. I found `tex2html` and `text2htmlcss`, which could only
+render equations without the surrounding HTML. I also found `mjpage`,
+which replaced mathematical expressions in a page with their SVG forms.
+
+This is still the case, in both MathJax and KaTeX. The ability
+to render math in one step is the main selling point of front-end LaTeX renderers:
+all you have to do is drop in a file from a CDN, and voila, you have your
+math. There are no such easy answers for back-end rendering. In fact,
+as we will soon see, it's not possible to just search-and-replace occurences
+of mathematics on your page, either. To actually get KaTeX working
+on the backend, you need access to tools that handle the potential variety
+of edge cases associated with HTML. Such tools, to my knowledge, do not
+currently exist.
+
+I decided to write my own Ruby script to get the job done. From this script, I
+would call the `katex` command-line program, which would perform
+the heavy lifting of rendering the mathematics.
+
+There are two types of math on my website: inline math and display math.
+On the command line ([here are the docs](https://katex.org/docs/cli.html)),
+the distinction is made using the `--display-mode` argument. So, the general algorithm
+is to replace the code inside the `$$...$$` with their display-rendered version,
+and the code inside the `\(...\)` with the inline-rendered version. I came up with
+the following Ruby function:
+
+```Ruby {linenos=table}
+def render_cached(cache, command, string, render_comment = nil)
+  cache.fetch(string) do |new|
+    puts "  Rendering #{render_comment || new}"
+    cache[string] = Open3.popen3(command) do |i, o, e, t|
+      i.write new
+      i.close
+      o.read.force_encoding(Encoding::UTF_8).strip
+    end
+  end
+end
+```
+
+Here, the `cache` argument is used to prevent re-running the `katex` command
+on an equation that was already rendered before (the output is the same, after all).
+The `command` is the specific shell command that we want to invoke; this would
+be either `katex` or `katex -d`. The `string` is the math equation to render,
+and the `render_comment` is the string to print to the console instead of the equation
+(so that long, display math equations are not printed out to standard out).
+
+Then, given a substring of the HTML file, we use regular expressions
+to find the `\(...\)` and `$$...$$`s, and use the `render_cached` method
+on the LaTeX code inside.
+
+```Ruby {linenos=table}
+def perform_katex_sub(inline_cache, display_cache, content)
+  rendered = content.gsub /\\\(((?:[^\\]|\\[^\)])*)\\\)/ do |match|
+    render_cached(inline_cache, "katex", $~[1])
+  end
+  rendered = rendered.gsub /\$\$((?:[^\$]|$[^\$])*)\$\$/ do |match|
+    render_cached(display_cache, "katex -d", $~[1], "display")
+  end
+  return rendered
+end
+```
+
+There's a bit of a trick to the final layer of this script. We want to be
+really careful about where we replace LaTeX, and where we don't. In
+particular, we _don't_ want to go into the `code` tags. Otherwise,
+it wouldn't be possible to talk about LaTeX code! I also suspect that
+some captions, alt texts, and similar elements should also be left alone.
+However, I don't have those on my website (yet), and I won't worry about
+them now. Either way, because of the code tags,
+we can't just search-and-replace over the entire page; we need to be context
+aware. This is where `nokogiri` comes in. We parse the HTML, and iterate
+over all of the 'text' nodes, calling `perform_katex_sub` on all
+of those that _aren't_ inside code tags.
+
+Fortunately, this kind of iteration is pretty easy to specify thanks to something called XPath.
+This was my first time encountering it, but it seems extremely useful: it's
+a sort of language for selecting XML nodes. First, you provide an 'axis',
+which is used to specify the positions of the nodes you want to look at
+relative to the root node. The axis `/` looks at the immediate children
+(this would be the `html` tag in a properly formatted document, I would imagine).
+The axis `//` looks at all the transitive children. That is, it will look at the
+children of the root, then its children, and so on. There's also the `self` axis,
+which looks at the node itself.
+
+After you provide an axis, you need to specify the type of node that you want to
+select. We can write `code`, for instance, to pick only the `<code>....</code>` tags
+from the axis we've chosen. We can also use `*` to select any node, and we can
+use `text()` to select text nodes, such as the `Hello` inside of `<b>Hello</b>`.
+
+We can also apply some more conditions to the nodes we pick using `[]`.
+For us, the relevant feature here is `not(...)`, which allows us to
+select nodes that do __not__ match a particular condition. This is all
+we need to know.
+
+We write:
+
+* `//`, starting to search for nodes everywhere, not just the root of the document.
+* `*`, to match _any_ node. We want to replace math inside of `div`s, `span`s, `nav`s,
+all of the `h`s, and so on.
+* `[not(self::code)]`, cutting out all the `code` tags.
+* `/`, now selecting the nodes that are immediate descendants of the nodes we've selected.
+* `text()`, giving us the text contents of all the nodes we've selected.
+
+All in all:
+
+```
+//*[not(self::code)]/text()
+```
+
+Finally, we use this XPath from `nokogiri`:
+
+```Ruby {linenos=table}
+files = ARGV[0..-1]
+inline_cache, display_cache = {}, {}
+
+files.each do |file|
+  puts "Rendering file: #{file}"
+  document = Nokogiri::HTML.parse(File.open(file))
+  document.search('//*[not(self::code)]/text()').each do |t|
+    t.replace(perform_katex_sub(inline_cache, display_cache, t.content))
+  end
+  File.write(file, document.to_html)
+end
+```
+
+I named this script `convert.rb`; it's used from inside of the Nix expression
+and its builder, which we will cover below.
+
+### Tying it All Together
+Finally, I wanted an end-to-end script to generate HTML pages and render the LaTeX in them.
+I used Nix for this, but the below script will largely be compatible with a non-Nix system.
+I came up with the following, commenting on Nix-specific commands:
+
+```Bash {linenos=table}
+# Nix-specific; set up paths.
+source $stdenv/setup
+
+# Build site with Hugo
+# The cp is Nix-specific; it copies the blog source into the current directory.
+cp -r $src/* .
+hugo --baseUrl="https://danilafe.com"
+
+# Render math in HTML and XML files.
+# $converter is Nix-specific; you can just use convert.rb.
+find public/ -regex "public/.*\.html" | xargs ruby $converter
+
+# Output result
+# $out is Nix-specific; you can replace it with your destination folder.
+mkdir $out
+cp -r public/* $out/
+```
+
+This is it! Using the two scripts, `convert.rb` and `builder.sh`, I
+was able to generate my blog with the math rendered on the back-end.
+Please note, though, that I had to add the KaTeX CSS to my website's
+`<head>`.
+
+### Caveats
+The main caveat of my approach is performance. For every piece of
+mathematics that I render, I invoke the `katex` command. This incurs
+the penalty of Node's startup time, every time, and makes my approach
+take a few dozen seconds to run on my relatively small site. The
+better approach would be to use a NodeJS script, rather than a Ruby one,
+to perform the conversion. KaTeX also provides an API, so such a NodeJS
+script can find the files, parse the HTML, and perform the substitutions.
+I did quite like using `nokogiri` here, though, and I hope that an equivalently
+pleasant solution exists in JavaScript.
+
+Re-rendering the whole website is also pretty wasteful. I rarely change the
+mathematics on more than one page at a time, but every time I do so, I have
+to re-run the script, and therefore re-render every page. This makes sense
+for me, since I use Nix, and my builds are pretty much always performed
+from scratch. On the other hand, for others, this may not be the best solution.
+
+### Alternatives
+The same person who sent me the original email above also pointed out
+[this `pandoc` filter for KaTeX](https://github.com/Zaharid/pandoc_static_katex).
+I do not use Pandoc, but from what I can see, this fitler relies on
+Pandoc's `Math` AST nodes, and applies KaTeX to each of those. This
+should work, but wasn't applicable in my case, since Hugo's shrotcodes
+don't mix well with Pandoc. However, it certainly seems like a workable
+solution.
+
+### Conclusion
+With the removal of MathJax from my site, it is now completely JavaScript free,
+and contains virtually the same HTML that it did beforehand. This, I hope,
+makes it work better on devices where computational power is more limited.
+I also hope that it illustrates a general principle - it's very possible,
+and plausible, to render LaTeX on the back-end for a static site.

content/blog/dell_is_horrible/index.md

@@ -0,0 +1,381 @@
+---
+title: DELL Is A Horrible Company And You Should Avoid Them At All Costs
+date: 2020-07-23T13:40:05-07:00
+tags: ["Electronics"]
+---
+
+I really do not want this to be a consumer electronics blog. Such things
+aren't interesting to me, and nor do I have much knowledge
+about them. However, sometimes, ripples from these areas make their way
+into my life, and this is one such instance. Let me tell you
+{{< sidenote "right" "source-note" "a story" >}}
+I originally wrote about this in
+<a href="https://www.dell.com/community/XPS/Ridiculously-Bad-Support-Experience/td-p/7554383">a thread on DELL's support website</a>. Some of this post is
+going to be adapted from the support website, but some things have happened
+since. You will probably notice the change between the terse language I used
+in the original post and the fresh text that I'm writing now.
+{{< /sidenote >}} of
+my experience with DELL and their XPS 2-in-1 laptop, which has gone on since
+around January of 2020, and is still going at the time of writing, in July
+2020, half a year later.
+
+I was, until recently, an undergraduate student in Computer Science. I will
+soon be starting my Masters in Computer Science, too. I say this to make one
+thing clear: I need a computer. Not only is it a necessity for my major,
+but the majority of my hobbies -- including this blog -- are digital, too.
+Since my university is a couple of hours from my home, I travel back and forth
+a lot. I also have a cozy little spot in the
+{{< sidenote "right" "offices-note" "graduate student offices" >}}
+They're a bunch of cubicles in a keycard-protected room, really. Nothing fancy.
+{{< /sidenote >}}at my university, but travel by bus, so I find myself spending
+roughly equal portions of my work time at home and 'elsewhere'. A laptop
+as my primary machine, I thought, made sense. But it had to be a decent one.
+Persuaded by one of my instructors, who stressed the importance of vision and
+a decent screen, I settled on a DELL XPS, which at the time came with a 4k
+display.
+
+As is commonplace, things went great at first. The screen _was_ really nice,
+all of my code compiled swiftly, and even the games I occasionally played ran
+at a solid 60fps. I was happy with my purchase.
+
+There was one hiccup before things went really downhill, a sort of
+foreshadowing of things to come. My trackpad didn't work at peculiar times.
+
+### Prologue: Trackpad Hiccups
+While working, booted into Linux, I noticed that my trackpad was having some
+trouble. It was stuttering, and occasionally wouldn't work at all for seconds
+at a time. I assumed that this was a problem with the trackpad drivers on
+Linux, or perhaps the whole system was freezing up. I rebooted, and the
+problem went away.
+
+Until it came back.
+
+A few days later, my trackpad was freezing virtually every minute.
+It was strange, but fortunately, I'm used to a keyboard-based workflow, and
+the malfunctions did not affect me too much. It was just a little troubling.
+What soon made it more troubling, was that I noticed this exact same issue
+occurring on Windows. To me, this meant one dreadful thing: it was a hardware
+issue.
+
+I poked and prodded for a little bit, and finally discovered the cause:
+whenever I put my hand on the left palmrest, the trackpad would reliably stop
+working. Knowing what the issue was, I called DELL. I spoke to a guy on the
+other end, who had me run through diagnostics, driver updates, and BIOS
+settings (I imagined this was procedure, so I didn't mind doing the extra
+work to make the other guy's job easier). Finally, he scheduled a repair
+appointment. A technician came into my house, took off the laptop cover,
+and said something along the lines of:
+
+> Now look. They gave me a whole new motherboard and case to replace yours,
+but in my personal opinion, this is a bad idea. Things are bound to break
+when you do this. See how the replacement case has an insulating piece
+of fabric under the left palmrest, and yours doesn't? Why don't we rip
+the fabric off the replacement case, and tape it in place on your machine,
+without any reassembly?
+
+This man was wiser than any of the other DELL technicians, I now understand.
+The repair went without a hitch. He grilled me for going to college instead of
+just picking up a trade, which was cheaper and offered more job security.
+In the end, I felt a little weird about having a piece of fabric duct taped
+inside my computer, but the trackpad had no more issues ever since. All was
+well.
+
+### Service Request 1: Broken D Key
+All was well, that is, until the middle of winter term. I was typing up an
+assignment for a university class. I was working as usual, when I suddenly
+noticed that the "d" key stopped working - it had to be pressed rather weird
+to register on the computer. I looked down, and discovered that the key had
+snapped in half. The top part of the key fell off shortly thereafter.
+
+{{< figure src="brokenkey.jpg" caption="The broken D key shortly after the above events." >}}
+
+At that point, I was more surprised than anything. I hadn't heard of something
+like this ever happening, especially under circumstances as normal as typing.
+Regardless, I contacted support, and set up a repair appointment. Things only
+went downhill from there.
+
+Again, the appointment was scheduled, and only a few days later, another
+technician arrived at my house. The only way to repair the key, he said,
+was to replace the whole keyboard. They keyboard happens to be located
+underneath all the other hardware, and so, the entire laptop had to be
+disassembled and reassembled from scratch. He worked for about an hour, and
+eventually, he put the machine together. The words of the previous
+technician, who wanted to avoid doing exactly what had just been done, echoed
+in my head:
+
+> Things are bound to break when you do this.
+
+I asked him to test it, just to make sure everything works. Sure enough,
+not everything did work: the machine no longer had sound!
+
+### Service Request 2: No sound
+During diagnostics, the laptop did not emit the "beep" it usually does. This
+was the first sign. Booting into Windows, the sound icon was crossed out in
+red, and no sound was present. Booting into Linux led to similar results.
+The microphone on the machine did not seem to work either. The service
+technician said that he didn't have the parts to repair it, told me he'd call
+it in, and left. Soon after, I got an email asking for times I'm available to
+call: I said "any time except for 1-4 pacific time". DELL support proceeded
+to call me at 3pm pacific time, when I had no service. Unable to reach me,
+they promptly notified me that they are archiving my service request.
+
+This all occurred near finals week at my university, so I had to put the issue
+on hold. I had to maintain my grades, and I had to grade heaps of assignments
+from other students. Though the lack of sound was annoying, it wasn't as
+pressing as preparing for exams, so it was during spring break that I finally
+called again, and scheduled the service appointment. By then,
+{{< sidenote "right" "pandemic-note" "the pandemic was in full swing," >}}
+Just for posterity, in 2020, there had been an outbreak of COVID-19,
+a Coronavirus. Many states in the U.S., including my own, issued
+the orders for lockdown and social distancing, which meant the closing
+of schools, restaurants, and, apparently, the cessation of in-person
+repairs.
+{{< /sidenote >}}and DELL told me they'd mail me a box to put my laptop in, and
+I'd have to mail it off to their service center. Sure, I thought, that's
+fine. If it's at the service center, they won't ever "not have the required
+parts". I told the tech support person my address, he read it back to me, and
+so it was settled.
+
+Until, that is, the box arrived at the wrong address.
+
+I had received the machine as a gift from my family, who purchased the
+computer to arrive at their address. The box arrived at that address too,
+despite my explicit instructions to have it deliver to my current residence.
+Since my family and I live 2 hours apart, it took 4 total hours to get the box
+to me (a drive that couldn't be made right away!), and by the time I had it,
+DELL was already threatening me again with closing the service request.
+Eventually, I was able to mail the machine off, and about 5 business days
+later (business days during which I did not have a working machine, which is
+very necessary for my school and job) I received it back. I was excited to
+have the machine back, but that didn't last very long. As I was using the
+computer with Wolfram Mathematica (a rather heavy piece of software running
+under Linux), I noticed that it was discharging even while plugged in. I
+booted into Windows, and was greeted with a warning, something along the
+lines of: "you are using a slow charger. Please use the official adapter".
+But I was using the official adapter! I also tried to plug my mouse into the
+relevant USB-C port, only to discover that it did not work. I had to make
+another service requests.
+
+### Service Request 3: Broken Charging Port
+This time, I made sure to tell the person on the other end of the support
+call to please send it to my address. I asked if there was anything I can do,
+or anyone I can contact, and was told "no, just mail the computer in again."
+I obliged. The box arrived at the right address this time, so I was able to
+ship it off.
+
+In the "describe your issue" field on the provided form, I begged the
+technicians to send me a working machine. "Please", I wrote "Last time I got
+a machine back from support, it was still broken. I really need it for school
+and work!". 5 business days later, I received the machine back. I plugged it
+in to make sure it worked, only to find out . . . that the very same charging
+port that I requested be repaired, is still broken! It would've been funny,
+if it wasn't infuriating. How is it possible for me to receive a machine from
+repairs, without the thing I asked to repair being as much as improved?!
+
+Worse, a day after I received the machine back (I was able to keep using it
+thanks to it having two USB-C ports capable of charging), the LCD suddenly
+flashed, and started flickering. Thinking it was a software glitch, I
+restarted the machine, only to discover the same flickering during the boot
+animation and menu. Not only was the charging port not repaired, but now my
+LCD was broken! (in the below picture, the screen is meant to be blue, but
+the bottom part of the display is purple and flickering).
+
+{{< figure src="brokenlcd.jpg" caption="The broken LCD." >}}
+
+### Service Request 4: Broken LCD
+I called in to support again, and they once again told me to ship the machine 
+off. What's worse, they accused me of breaking the port myself, and told me
+this was no longer covered under basic warranty. I had to explain all over
+again that the port worked fine before the fateful day the D-key snapped. They
+told me they'd "look into it". Eventually, I received a box in the mail. I
+wasn't told I would be receiving a box, but that wasn't a big deal. I mailed
+off the machine.
+
+The UPS shipping was always the most streamlined part of the process. A day
+later, I was told my machine was received intact. Another day, and I was
+informed that the technicians are starting to work on it. And then,
+a few hours later:
+
+> __Current Status:__
+> The part(s) needed to repair your system are not currently in stock.
+> __What's Next:__
+> In most cases the parts are available is less than five days.
+
+A few days is no big deal, and it made sense that DELL wouldn't just
+have screens lying around. So I waited. And waited. And waited. Two weeks
+later, I got a little tired of waiting, and called the repair center.
+An automated message told me:
+
+> We're currently experiencing heavy call volumes. Please try again later. Goodbye.
+
+And the call was dropped. This happened every time I tried to call, no matter
+the hour. The original status update -- the one that notified me about the
+part shortage -- came on May 8th, but the machine finally arrived to me
+(without prior warning) on June 2nd, almost a month later.
+
+The charging port worked. Sound
+worked. The screen wasn't flickering. I was happy for the brief moments that
+my computer was loading. As soon as I started vim, though, I noticed something
+was off: the fonts looked more pixelated. The DPI settings I'd painstakingly
+tweaked were wrong. Now that I thought about it, even the GRUB menu was
+larger. My suspicion growing, I booted into Windows, and looked at the display
+settings. Noticeably fewer resolutions were listed in the drop-down menu;
+worse, the highest resolution was 1080p. After almost a month of waiting,
+DELL replaced my 4k laptop display with a 1080p one.
+
+### System Replacement: Worse LCD Screen
+
+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](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." >}}
+
+Of course we can proceed further. I wanted to know what kind of machine I was getting,
+though. As long as it was the same model that I originally bought,
+{{< sidenote "right" "replacement-note" "it would be better than what I have." >}}
+At least in principle, it would be. Perhaps the wear and tear on the replacement
+parts would be greater, but at least I would have, presumably, a machine
+in good condition that had the 4k screen that made me buy it in the first place.
+{{< /sidenote >}}
+Despite this, I knew that the machine I was getting was likely refurbished.
+This _had_ to mean that some of the parts would come from other, used, machines.
+This irked me, because, well, I payed for a new machine.
+
+{{< figure src="dm_2.png" caption="Ah, the classic use of canned responses." >}}
+
+Their use of the canned response, and their unwillingness to answer this simple
+question, was transparent. Indeed, the machine would be made of used
+parts. I still wanted to proceed. DELL requested that I sent an image of
+my machine which included its service tag, together with a piece of
+paper which included my name and email address. I obliged, and quickly got a response:
+
+{{< 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. 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?" >}}
+
+My initial request was cancelled? Why wasn't I told? What was the reason?
+What the heck was going on at DELL Support? Should I be worried?
+My question of "Why" was answered with the apt response of "Yes",
+and a message meant to pacify me. While this was going on, I ordered
+a
+{{< sidenote "right" "pinebook-note" "Pinebook Pro." >}}
+The Pinebook – a $200 machine – has, thus far, worked more reliably than any DELL product
+I've had the misfortune of owning.
+{{< /sidenote >}} It was not a replacement for the DELL machine, but rather
+the first step towards migrating my setup to a stationary computer,
+and a small, lightweight SSH device. At this point,
+there was no more faith in DELL left in my mind.
+
+Soon, DELL required my attention, only to tell me that they put in
+a request to see that status of my request. How bureaucratic. Two
+more names -- Kareem and JKC -- flickered through the chats,
+also never to be seen again.
+
+{{< figure src="dm_5.png" caption="Not much of a conversation, really." >}}
+
+Finally, on July 9th (a month and six days after my first real message to DELL
+support), I was notified by my roommates that FedEx tried to deliver a package
+to our house, but gave up when no one came to sign for it. On one hand, this
+is great: FedEx didn't just leave my laptop on the porch. On the other hand,
+though, this was the first time I heard about receiving the machine. I got
+to the house the next day, unpacked the new computer, and tested all the things
+that had, at one point, failed. Everything seemed to work. I transfered all my
+files, wiped the old computer clean, and mailed it off. I also spent some
+time dealing with the fallout of DELL PremierColor starting on its own,
+and permanently altering the color profile of my display. I don't have the
+special, physical calibration device, and therefore still suspect that my
+screen is somewhat green.
+
+Today, I discovered that the microphone of the replacement machine didn't work.
+
+### Am I The Problem?
+When the mysterious FedEx package arrived at my door on July 9th, I did some
+digging to verify my suspicion that it was from DELL. I discovered their
+HQ in Lebanon, TN. This gave me an opportunity to
+{{< sidenote "right" "reviews-note" "see" >}}
+See, of course, modulo whatever bias arises when only those who feel strongly leave reviews.
+{{< /sidenote >}} whether or not I was alone in this situation. I was genuinely
+worried that I was suffering from the technical variant of
+[Munchausen Syndrome](https://www.webmd.com/mental-health/munchausen-syndrome#1),
+and that I was compulsively breaking my electronics. These worries were
+dispelled by the reviews on Google:
+
+{{< figure src="reviews_1.png" caption="Most of the reviews are pretty terse, but the ratings convey the general idea." >}}
+
+There were even some that were shockingly similar in terms of the apparent
+incompetence of the DELL technicians:
+
+{{< figure src="reviews_2.png" caption="Now, now, Maggie, I wouldn't go as far as recommending Apple." >}}
+
+So, this is not uncommon. This is how DELL deals with customers now. It's
+awfully tiring, really; I've been in and out of repairs continuously for
+almost half a year, now. That's 2.5% of my life at the time of writing,
+all non-stop since the D-key. And these people probably have spent considerable
+amounts of time, too.
+
+### It's About the Principle
+The microphone on my machine is rather inconsequential to me. I can, and regularly do,
+teleconference from my phone (a habit that I developed thanks to DELL, since
+my computer was so often unavailable). I don't need to dictate anything. Most
+of my communication is via chat.
+
+Really, compared to the other issues (keyboard, sound, charging, USB ports, the broken or low-resolution screen)
+the microphone is a benign problem. As I have now learned, things could be worse.
+
+But why should the thought, _"It could be worse"_, even cross my mind
+when dealing with such a matter? Virtually every issue that has
+occurred with my computer thus far could -- should! -- have been diagnosed
+at the repair center. The 'slow charger' warning shows up in BIOS,
+so just turning the computer on while plugged in should make it obvious something
+is wrong; doubly so when the very reason that the laptop was in repairs
+in the first place was because of the faulty charger. I refuse to believe
+that screens with different resolutions have the same part identifier,
+either. How have the standards of service from DELL fallen so low?
+How come this absurd scenario plays out not just for me, but
+for others as well? It would be comforting, in a way, to think
+that I was just the 'exceptional case'. But apparently, I'm not.
+This is standard practice.
+
+### Tl;DR
+Here are he problems I've had with DELL:
+
+* The machine shipped, apparently, with a missing piece of insulation.
+* The "D" key on the keyboard snapped after only a few months of use.
+* While repairing the "D" key, the DELL technician broke the computer's sound and microphone.
+* While repairing the sound and microphone, the DELL technicians broke a charging port.
+* The DELL technicians failed to repair the charging port, mailing me back a machine
+exhibiting the same issues, in addition to a broken LCD screen.
+* The repair of the LCD screen took almost a month, and concluded
+with me receiving a worse quality screen than I originally had.
+* The system replacement that followed the botched LCD repair took
+over a month to go through.
+* The replaced system was made partially of used parts, which
+DELL refused to admit.
+* The microphone on the replacement system was broken.
+
+### Closing Thoughts
+I will not be sending my system in again. It doesn't make sense to do so -
+after mailing my system in for repairs three times, I've measured empirically that
+the chance of failure is 100%. Every service request is a lottery, dutifully
+giving out a random prize of another broken part. I no longer wish to play;
+as any person who gambles should, I will quit while I'm ahead, and cut my losses.
+However, I hope for this story, which may be unusual in its level of detail,
+but not its content, to be seen by seen by someone. I hope to prevent
+someone out there from feeling the frustration, and anger, and peculiar amusement
+that I felt during this process. I hope for someone else to purchase a computer
+with money, and not with their sanity. A guy can hope.
+
+If you're reading this, please take this as a warning. __DELL is a horrible
+company. They have the lowest standards of customer support of any
+U.S. company that I've encountered. Their technicians are largely incompetent.
+Their quality assurance is non-existent. Stay away from them.__

content/blog/haskell_lazy_evaluation.md

@@ -1,95 +0,0 @@
----
-title: "Clairvoyance for Good: Using Lazy Evaluation in Haskell"
-date: 2020-05-03T20:05:29-07:00
-tags: ["Haskell"]
-draft: true
----
-
-While tackling a project for work, I ran across a rather unpleasant problem.
-I don't think it's valuable to go into the specifics here (it's rather
-large and convoluted); however, the outcome of this experience led me to
-discover a very interesting technique for lazy functional languages,
-and I want to share what I learned.
-
-### Time Traveling
-Some time ago, I read [this post](https://kcsongor.github.io/time-travel-in-haskell-for-dummies/) by Csongor Kiss about time traveling in Haskell. It's
-really cool, and makes a lot of sense if you have wrapped your head around
-lazy evaluation. I'm going to present my take on it here, but please check out
-Csongor's original post if you are interested.
-
-Say that you have a list of integers, like `[3,2,6]`. Next, suppose that
-you want to find the maximum value in the list. You can implement such
-behavior quite simply with pattern matching:
-
-```Haskell
-myMax :: [Int] -> Int
-myMax [] = error "Being total sucks"
-myMax (x:xs) = max x $ myMax xs
-```
-
-You could even get fancy with a `fold`:
-
-```Haskell
-myMax :: [Int] -> Int
-myMax = foldr1 max
-```
-
-All is well, and this is rather elementary Haskell. But now let's look at
-something that Csongor calls the `repMax` problem:
-
-> Imagine you had a list, and you wanted to replace all the elements of the
-> list with the largest element, by only passing the list once.
-
-How can we possibly do this in one pass? First, we need to find the maximum
-element, and only then can we have something to replace the other numbers
-with! It turns out, though, that we can just expect to have the future
-value, and all will be well. Csongor provides the following example:
-
-```Haskell {linenos=table}
-repMax :: [Int] -> Int -> (Int, [Int])
-repMax [] rep = (rep, [])
-repMax [x] rep = (x, [rep])
-repMax (l : ls) rep = (m', rep : ls')
-  where (m, ls') = repMax ls rep
-        m' = max m l
-
-doRepMax :: [Int] -> [Int]
-doRepMax xs = xs'
-  where (largest, xs') = repMax xs largest
-```
-
-In the above snippet, `repMax` expects to receive the maximum value of
-its input list. At the same time, it also computes that maximum value,
-returning it and the newly created list. `doRepMax` is where the magic happens:
-the `where` clauses receives the maximum number from `repMax`, while at the
-same time using that maximum number to call `repMax`!
-
-This works because Haskell's evaluation model is, effectively,
-[lazy graph reduction](https://en.wikipedia.org/wiki/Graph_reduction). That is,
-you can think of Haskell as manipulating your code as
-{{< sidenote "right" "tree-note" "a syntax tree," >}}
-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.
-{{< /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
-needed to compute the final answer can exist, unsimplied, in the tree. 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.
-
-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:
-
-```
->>> countMaxFactors [1,3,3,9]
-
-fromList [(1, 1), (3, 2), (9, 1)]
-```

content/blog/haskell_lazy_evaluation/index.md

@@ -0,0 +1,564 @@
+---
+title: "Time Traveling In Haskell: How It Works And How To Use It"
+date: 2020-07-30T00:58:10-07:00
+tags: ["Haskell"]
+---
+
+I recently got to use a very curious Haskell technique
+{{< sidenote "right" "production-note" "in production:" >}}
+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
+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
+never terminate.
+
+### Time Traveling
+Some time ago, I read [this post](https://kcsongor.github.io/time-travel-in-haskell-for-dummies/) by Csongor Kiss about time traveling in Haskell. It's
+really cool, and makes a lot of sense if you have wrapped your head around
+lazy evaluation. I'm going to present my take on it here, but please check out
+Csongor's original post if you are interested.
+
+Say that you have a list of integers, like `[3,2,6]`. Next, suppose that
+you want to find the maximum value in the list. You can implement such
+behavior quite simply with pattern matching:
+
+```Haskell
+myMax :: [Int] -> Int
+myMax [] = error "Being total sucks"
+myMax (x:xs) = max x $ myMax xs
+```
+
+You could even get fancy with a `fold`:
+
+```Haskell
+myMax :: [Int] -> Int
+myMax = foldr1 max
+```
+
+All is well, and this is rather elementary Haskell. But now let's look at
+something that Csongor calls the `repMax` problem:
+
+> Imagine you had a list, and you wanted to replace all the elements of the
+> list with the largest element, by only passing the list once.
+
+How can we possibly do this in one pass? First, we need to find the maximum
+element, and only then can we have something to replace the other numbers
+with! It turns out, though, that we can just expect to have the future
+value, and all will be well. Csongor provides the following example:
+
+```Haskell
+repMax :: [Int] -> Int -> (Int, [Int])
+repMax [] rep = (rep, [])
+repMax [x] rep = (x, [rep])
+repMax (l : ls) rep = (m', rep : ls')
+  where (m, ls') = repMax ls rep
+        m' = max m l
+```
+In this example, `repMax` takes the list of integers,
+each of which it must replace with their maximum element.
+It also takes __as an argument__ the maximum element,
+as if it had already been computed. It does, however,
+still compute the intermediate maximum element,
+in the form of `m'`. Otherwise, where would the future
+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
+thinking. The real magic happens in Csongor's `doRepMax`
+function:
+
+```Haskell
+doRepMax :: [Int] -> [Int]
+doRepMax xs = xs'
+  where (largest, xs') = repMax xs largest
+```
+
+Look, in particular, on the line with the `where` clause.
+We see that `repMax` returns the maximum element of the
+list, `largest`, and the resulting list `xs'` consisting
+only of `largest` repeated as many times as `xs` had elements.
+But what's curious is the call to `repMax` itself. It takes
+as input `xs`, the list we're supposed to process... and
+`largest`, the value that _it itself returns_.
+
+This works because Haskell's evaluation model is, effectively,
+[lazy graph reduction](https://en.wikipedia.org/wiki/Graph_reduction). That is,
+you can think of Haskell as manipulating your code as
+{{< sidenote "right" "tree-note" "a syntax tree," >}}
+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.
+{{< /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
+needed to compute the final answer can exist, unsimplified, in the tree.
+Why don't we draw a few graphs to get familiar with the idea?
+
+### Visualizing Graphs and Their Reduction
+Let's start with something that doesn't have anything fancy. We can
+take a look at the graph of the expression:
+
+```Haskell
+length [1]
+```
+
+Stripping away Haskell's syntax sugar for lists, we can write this expression as:
+
+```Haskell
+length (1:[])
+```
+
+Then, recalling that `(:)`, or 'cons', is just a binary function, we rewrite:
+
+```Haskell
+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" >}}
+
+In this image, the `@` nodes represent function application. The
+root node is an application of the function `length` to the graph that
+represents the list `[1]`. The list itself is represented using two
+application nodes: `(:)` takes two arguments, the head and tail of the
+list, and function applications in Haskell are
+[curried](https://en.wikipedia.org/wiki/Currying). Eventually,
+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" >}}
+
+Conceptually, we only took one reduction step, and thus, we haven't yet gotten
+to evaluating the recursive call to `length`. Since `(+)`
+is also a binary function, `1+length xs` is represented in this
+new graph as two applications of `(+)`, first to `1`, and then
+to `length []`.
+
+But what is that box at the root? This box _used to be_ the root of the
+first graph, which was an application node. However, it is now a
+an _indirection_. Conceptually, reducing
+this indirection amounts to reducing the graph
+it points to. But why have we {{< sidenote "right" "altered-note" "altered the graph" >}}
+This is a key aspect of implementing functional languages.
+The language itself may be pure, while the runtime
+can be, and usually is, impure and stateful. After all,
+computers are impure and stateful, too!
+{{< /sidenote >}} in this manner? Because Haskell is a pure language,
+of course! If we know that a particular graph reduces to some value,
+there's no reason to reduce it again. However, as we will
+soon see, it may be _used_ again, so we want to preserve its value.
+Thus, when we're done reducing a graph, we replace its root node with
+an indirection that points to its result. 
+
+When can a graph be used more than once? Well, how about this:
+
+```Haskell
+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" >}}
+
+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:
+
+{{< 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 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).
+
+Our graphs can also include cycles.
+A simple, perhaps _the most_ simple example of this in practice is Haskell's
+`fix` function. It computes a function's fixed point,
+{{< sidenote "right" "fixpoint-note" "and can be used to write recursive functions." >}}
+In fact, in the lambda calculus, <code>fix</code> is pretty much <em>the only</em>
+way to write recursive functions. In the untyped lambda calculus, it can
+be written as: $$\lambda f . (\lambda x . f (x \ x)) \  (\lambda x . f (x \ x))$$
+In the simply typed lambda calculus, it cannot be written in any way, and
+needs to be added as an extension, typically written as \(\textbf{fix}\).
+{{< /sidenote >}}
+It's implemented as follows:
+
+```Haskell
+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" >}}
+
+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" >}}
+
+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.
+
+Almost there! A node can refer to itself, and, when evaluated, it
+is replaced with its own value. Thus, a node can effectively reference
+its own value! The last piece of the puzzle is how a node can access
+_parts_ of its own value: recall that `doRepMax` calls `repMax`
+with only `largest`, while `repMax` returns `(largest, xs')`.
+I have to admit, I don't know the internals of GHC, but I suspect
+this is done by translating the code into something like:
+
+```Haskell
+doRepMax :: [Int] -> [Int]
+doRepMax xs = snd t
+  where t = repMax xs (fst t)
+```
+
+#### 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.
+This is a rather long and detailed example, so feel free to skip
+this section to read more about actually using time traveling.
+
+If you're sticking around, why don't we watch how the graph of `doRepMax [1, 2]` unfolds.
+This example will be more complex than the ones we've seen
+so far; to avoid overwhelming ourselves with notation,
+let's adopt a different convention of writing functions. Instead
+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" >}}
+
+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" >}}
+
+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
+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
+consists of two uses of the `(:)` function.
+
+{{< figure src="repmax_2.png" caption="The first step of reducing `doRepMax [1,2]`." class="small" >}}
+
+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
+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" >}}
+
+Since `(,)` is a constructor, let's say that it doesn't
+need to be evaluated, and that its
+{{< sidenote "right" "normal-note" "graph cannot be reduced further" >}}
+A graph that can't be reduced further is said to be in <em>normal form</em>,
+by the way.
+{{< /sidenote >}} (in practice, other things like
+packing may occur here, but they are irrelevant to us).
+If `(,)` can't be reduced, we can move on to evaluating `snd`. Given a pair, `snd`
+simply returns the second element, which in our
+case is the subgraph starting at `(:)`. We
+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" >}}
+
+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.
+However, stopping at `(:)` wouldn't be very interesting,
+and we wouldn't learn much from doing so. So instead, let's assume
+that _something_ is trying to read the elements of our list;
+perhaps we are trying to print this list to the screen in GHCi.
+
+In this case, our mysterious external force starts unpacking and
+inspecting the arguments to `(:)`. The first argument to `(:)` is
+the list's head, which is the subgraph starting with the starred application
+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" >}}
+
+Phew! Next, we need to evaluate the body of `max`. Let's make one more
+simplification here: rather than substitututing `max` for its body
+here, let's just reason about what evaluating `max` would entail.
+We would need to evaluate its two arguments, compare them,
+and return the larger one. The argument `1` can't be reduced
+any more (it's just a number!), but the second argument,
+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" >}}
+
+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.
+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" >}}
+
+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" >}}
+
+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
+another indirection (formerly the call to `max`), which
+points to `2`. Thus, any edge pointing to a star now
+points to the value 2. 
+
+By finding the value of the starred node, we have found the first
+argument of `(:)`, and returned it to our mysterious external force.
+If we were printing to GHCi, the number `2` would appear on the screen
+right about now. The force then moves on to the second argument of `(:)`,
+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" >}}
+
+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
+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:
+
+{{< figure src="repmax_10.png" caption="The result of reducing `doRepMax [1,2]`." class="small" >}}
+
+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.
+
+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:
+
+{{< codelines "Haskell" "time-traveling/TakeMax.hs" 1 12 >}}
+
+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.
+
+Unfortunately, this doesn't work; our program never terminates.
+You may be thinking:
+
+> 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.
+
+To address this, we can reformulate our `takeUntilMax`
+function as follows:
+
+{{< 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

@@ -0,0 +1,375 @@
+---
+title: Meaningfully Typechecking a Language in Idris, Revisited
+date: 2020-07-22T14:37:35-07:00
+tags: ["Idris"]
+---
+
+Some time ago, I wrote a post titled [Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}). The gist of the post was as follows:
+
+* _Programming Language Fundamentals_ students were surprised that, despite
+having run their expression through (object language) typechecking, they still had to
+have a `Maybe` type in their evaluation functions. This was due to
+the fact that the (meta language) type system was not certain that
+(object language) typechecking worked.
+* A potential solution was to write separate expression types such
+as `ArithExpr` and `BoolExpr`, which are known to produce booleans
+or integers. However, this required the re-implementation of most
+of the logic for `IfElse`, for which the branches could have integers,
+booleans, or strings.
+* An alternative solution was to use dependent types, and index
+the `Expr` type with the type it evaluates to. We defined a data type
+`data ExprType = IntType | StringType | BoolType`, and then were able
+to write types like `SafeExpr IntType` that we _knew_ would evaluate
+to an integer, or `SafeExpr BoolType`, which we also _knew_ would
+evaluate to a boolean. We then made our `typecheck` function
+return a pair of `(type, SafeExpr of that type)`.
+
+Unfortunately, I think that post is rather incomplete. I noted
+at the end of it that I was not certain on how to implement
+if-expressions, which were my primary motivation for not just
+sticking with `ArithExpr` and `BoolExpr`. It didn't seem too severe
+then, but now I just feel like a charlatan. Today, I decided to try
+again, and managed to figure it out with the excellent help from
+people in the `#idris` channel on Freenode. It required a more
+advanced use of dependent types: in particular, I ended up using
+Idris' theorem proving facilities to get my code to pass typechecking.
+In this post, I will continue from where we left off in the previous
+post, adding support for if-expressions.
+
+Let's start with the new `Expr` and `SafeExpr` types. Here they are:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 37 49 >}}
+
+For `Expr`, the `IfElse` constructor is very straightforward. It takes
+three expressions: the condition, the 'then' branch, and the 'else' branch.
+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
+be of type `SafeExpr t`. Since the result of the if-expression will be
+the output of one of the branches, the whole if-expression is also
+of type `SafeExpr t`.
+
+### What Stumped Me: Equality
+Typechecking if-expressions is where things get interesting. First,
+we want to require that the condition of the expression evaluates
+to a boolean. For this, we can write a function `requireBool`,
+that takes a dependent pair produced by `typecheck`. This
+function does one of two things:
+
+* If the dependent pair contains a `BoolType`, and therefore also an expression
+of type `SafeExpr BoolType`, `requireBool` succeeds, and returns the expression.
+* If the dependent pair contains any type other than `BoolType`, `requireBool`
+fails with an error message. Since we're using `Either` for error handling,
+this amounts to using the `Left` constructor.
+
+Such a function is quite easy to write:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 58 60 >}}
+
+We can then write all of the recursive calls to `typecheck` as follows:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 71 75 >}}
+
+Alright, so we have the types of the `t` and `e` branches. All we have to
+do now is use `(==)`. We could implement `(==)` as follows:
+
+```Idris
+implementation Eq ExprType where
+  IntType == IntType = True
+  BoolType == BoolType = True
+  StringType == StringType = True
+  _ == _ = False
+```
+
+Now we're golden, right? We can just write the following:
+
+```Idris {linenos=table, linenostart=76}
+    if tt == et
+       then pure (_ ** IfThenElse ce te ee)
+       else Left "Incompatible branch types."
+```
+
+No, this is not quire right. Idris complains:
+
+```
+Type mismatch between et and tt
+```
+
+Huh? But we just saw that `et == tt`! What's the problem?
+The problem is, in fact, that `(==)` is meaningless as far
+as the Idris typechecker is concerned. We could have just
+as well written,
+
+```Idris
+implementation Eq ExprType where
+  _ == _ = True
+```
+
+This would tell us that `IntType == BoolType`. But of course,
+`SafeExpr IntType` is not the same as `SafeExpr BoolType`; I
+would be very worried if the typechecker allowed me to assert
+otherwise. There is, however, a kind of equality that we can
+use to convince the Idris typechecker that two types are the
+same. This equality, too, is a type.
+
+### Curry-Howard Correspondence
+Spend enough time learning about Programming Language Theory, and
+you will hear the term _Curry Howard Correspondence_. If you're
+the paper kind of person, I suggest reading Philip Wadler's
+_Propositions as Types_ paper. Alternatively, you can take a look
+at _Logical Foundations_' [Proof Objects](https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html)
+chapter. I will give a very brief
+explanation here, too, for the sake of completeness. The general
+gist is as follows: __propositions (the logical kind) correspond
+to program types__, and proofs of the propositions correspond
+to values of the types.
+
+To get settled into this idea, let's look at a few 'well-known' examples:
+
+* `(A,B)`, the tuple of two types `A` and `B` is equivalent to the
+proposition \\(A \land B\\), which means \\(A\\) and \\(B\\). Intuitively,
+to provide a proof of \\(A \land B\\), we have to provide the proofs of
+\\(A\\) and \\(B\\).
+* `Either A B`, which contains one of `A` or `B`, is equivalent
+to the proposition \\(A \lor B\\), which means \\(A\\) or \\(B\\).
+Intuitively, to provide a proof that either \\(A\\) or \\(B\\)
+is true, we need to provide one of them.
+* `A -> B`, the type of a function from `A` to `B`, is equivalent
+to the proposition \\(A \rightarrow B\\), which reads \\(A\\)
+implies \\(B\\). We can think of a function `A -> B` as creating
+a proof of `B` given a proof of `A`. 
+
+Now, consider Idris' unit type `()`:
+
+```Idris
+data () = ()
+```
+
+This type takes no arguments, and there's only one way to construct
+it. We can create a value of type `()` at any time, by just writing `()`.
+This type is equivalent to \\(\\text{true}\\): only one proof of it exists,
+and it requires no premises. It just is.
+
+Consider also the type `Void`, which too is present in Idris:
+
+```Idris
+-- Note: this is probably not valid code.
+data Void = -- Nothing
+```
+
+The type `Void` has no constructors: it's impossible
+to create a value of this type, and therefore, it's 
+impossible to create a proof of `Void`. Thus, as you may have guessed, `Void`
+is equivalent to \\(\\text{false}\\).
+
+Finally, we get to a more complicated example:
+
+```Idris
+data (=) : a -> b -> Type where
+   Refl : x = x
+```
+
+This defines `a = b` as a type, equivalent to the proposition
+that `a` is equal to `b`. The only way to construct such a type
+is to give it a single value `x`, creating the proof that `x = x`.
+This makes sense: equality is reflexive. 
+
+This definition isn't some loosey-goosey boolean-based equality! If we can construct a value of 
+type `a = b`, we can prove to Idris' typechecker that `a` and `b` are equivalent. In
+fact, Idris' standard library gives us the following function:
+
+```Idris
+replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
+```
+
+This reads, given a type `a`, and values `x` and `y` of type `a`, if we know
+that `x = y`, then we can rewrite any proposition in terms of `x` into
+another, also valid proposition in terms of `y`. Let's make this concrete.
+Suppose `a` is `Int`, and `P` (the type of which is now `Int -> Type`),
+is `Even`, a proposition that claims that its argument is even.
+{{< sidenote "right" "specialize-note" "Then, we have:" >}}
+I'm only writing type signatures for <code>replace'</code>
+to avoid overloading. There's no need to define a new function;
+<code>replace'</code> is just a specialization of <code>replace</code>,
+so we can use the former anywhere we can use the latter.
+{{< /sidenote >}}
+
+```Idris
+replace' : {x : Int} -> {y : Int} -> x = y -> Even x -> Even y
+```
+
+That is, if we know that `x` is equal to `y`, and we know that `x` is even,
+it follows that `y` is even too. After all, they're one and the same!
+We can take this further. Recall:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 44 44 >}}
+
+We can therefore write:
+
+```Idris
+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
+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.
+
+### First Attempt: `Eq` implies Equality
+It's pretty trivial to see that we _did_ define `(==)` correctly (`IntType` is equal
+to `IntType`, `StringType` is equal to `StringType`, and so on). Thus,
+if we know that `x == y` is `True`, it should follow that `x = y`. We can thus
+define the following proposition:
+
+```Idris
+eqCorrect : {a : ExprType} -> {b : ExprType} -> (a == b = True) -> a = b
+```
+
+We will see shortly why this is _not_ the best solution, and thus, I won't bother
+creating a proof / implementation for this proposition / function.
+It reads:
+
+> If we have a proof that `(==)` returned true for some `ExprType`s `a` and `b`,
+it must be that `a` is the same as `b`.
+
+We can then define a function to cast
+a `SafeExpr a` to `SafeExpr b`, given that `(==)` returned `True` for some `a` and `b`:
+
+```Idris
+safeCast : {a : ExprType} -> {b : ExprType} -> (a == b = True) -> SafeExpr a -> SafeExpr b
+safeCast h e = replace (eqCorrect h) e
+```
+
+Awesome! All that's left now is to call `safeCast` from our `typecheck` function:
+
+```Idris {linenos=table, linenostart=76}
+    if tt == et
+       then pure (_ ** IfThenElse ce te (safeCast ?uhOh ee))
+       else Left "Incompatible branch types."
+```
+
+No, this doesn't work after all. What do we put for `?uhOh`? We need to have
+a value of type `tt == et = True`, but we don't have one. Idris' own if-then-else
+expressions do not provide us with such proofs about their conditions. The awesome
+people at `#idris` pointed out that the `with` clause can provide such a proof.
+We could therefore write:
+
+```Idris
+createIfThenElse ce (tt ** et) (et ** ee) with (et == tt) proof p
+  | True = pure (tt ** IfThenElse ce te (safeCast p ee))
+  | False = Left "Incompatible branch types."
+```
+
+Here, the `with` clause effectively adds another argument equal to `(et == tt)` to `createIfThenElse`,
+and tries to pattern match on its value. When we combine this with the `proof` keyword,
+Idris will give us a handle to a proof, named `p`, that asserts the new argument
+evaluates to the value in the pattern match. In our case, this is exactly
+the proof we need to give to `safeCast`.
+
+However, this is ugly. Idris' `with` clause only works at the top level of a function,
+so we have to define a function just to use it. It also shows that we're losing
+information when we call `(==)`, and we have to reconstruct or recapture it using
+some other means.
+
+
+### Second Attempt: Decidable Propositions
+More awesome folks over at `#idris` pointed out that the whole deal with `(==)`
+is inelegant; they suggested I use __decidable propositions__, using the `Dec` type.
+The type is defined as follows:
+
+```Idris
+data Dec : Type -> Type where
+  Yes : (prf : prop) -> Dec prop
+  No : (contra : prop -> Void) -> Dec prop
+```
+
+There are two ways to construct a value of type `Dec prop`:
+
+* We use the `Yes` constructor, which means that the proposition `prop`
+is true. To use this constructor, we have to give it a proof of `prop`,
+called `prf` in the constructor.
+* We use the `No` constructor, which means that the proposition `prop`
+is false. We need a proof of type `prop -> Void` to represent this:
+if we have a proof of `prop`, we arrive at a contradiction.
+
+This combines the nice `True` and `False` of `Bool`, with the
+'real' proofs of the truthfulness or falsity. At the moment
+that we would have been creating a boolean, we also create
+a proof of that boolean's value. Thus, we don't lose information.
+Here's how we can go about this:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 20 29 >}}
+
+We pattern match on the input expression types. If the types are the same, we return
+`Yes`, and couple it with `Refl` (since we've pattern matched on the types
+in the left-hand side of the function definition, the typechecker has enough
+information to create that `Refl`). On the other hand, if the expression types
+do not match, we have to provide a proof that their equality would be absurd.
+For this we use helper functions / theorems like `intBoolImpossible`:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 11 12 >}}
+
+I'm not sure if there's a better way of doing this than using `impossible`.
+This does the job, though: Idris understands that there's no way we can get
+an input of type `IntType = BoolType`, and allows us to skip writing a right-hand side.
+
+We can finally use this new `decEq` function in our type checker:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 76 78 >}}
+
+Idris is happy with this! We should also add `IfThenElse` to our `eval` function.
+This part is very easy:
+
+{{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV2.idr" 80 85 >}}
+
+Since the `c` part of the `IfThenElse` is indexed with `BoolType`, we know
+that evaluating it will give us a boolean. Thus, we can use that
+directly in the Idris if-then-else expression. Let's try this with a few
+expressions:
+
+```Idris
+BinOp Add (IfElse (BoolLit True) (IntLit 6) (IntLit 7)) (BinOp Multiply (IntLit 160) (IntLit 2))
+```
+
+This evaluates `326`, as it should. What if we make the condition non-boolean?
+
+```Idris
+BinOp Add (IfElse (IntLit 1) (IntLit 6) (IntLit 7)) (BinOp Multiply (IntLit 160) (IntLit 2))
+```
+
+Our typechecker catches this, and we end up with the following output:
+
+```
+Type error: Not a boolean.
+```
+
+Alright, let's make one of the branches of the if-expression be a boolean, while the
+other remains an integer.
+
+```Idris
+BinOp Add (IfElse (BoolLit True) (BoolLit True) (IntLit 7)) (BinOp Multiply (IntLit 160) (IntLit 2))
+```
+
+Our typechecker catches this, too:
+
+```
+Type error: Incompatible branch types.
+```
+
+### Conclusion
+I think this is a good approach. Should we want to add more types to our language, such as tuples,
+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 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`,
+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,4 +216,20 @@ figure {
     figcaption {
         text-align: center;
     }
+
+    &.tiny img {
+        max-height: 15rem;
+    }
+
+    &.small img {
+        max-height: 20rem;
+    }
+
+    &.medium img {
+        max-height: 30rem;
+    }
+}
+
+.twitter-tweet {
+    margin: auto;
 }

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,10 +3,11 @@
 </div>
 <nav>
     <div class="container">
-        <a href="/">Home</a>
+        <a href="/">{{ i18n "Home" }}</a>
+        <a href="/about">{{ i18n "About" }}</a>
         <a href="https://github.com/DanilaFe">GitHub</a>
-        <a href="/about">About</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" }}