code/typesafe-interpreter/TypesafeIntrV2.idr

@@ -1,99 +0,0 @@
-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 {a = IntType} {b = IntType} = Yes Refl
-decEq {a = BoolType} {b = BoolType} = Yes Refl
-decEq {a = StringType} {b = StringType} = Yes Refl
-decEq {a = IntType} {b = BoolType} = No intBoolImpossible
-decEq {a = BoolType} {b = IntType} = No $ intBoolImpossible . sym
-decEq {a = IntType} {b = StringType} = No intStringImpossible
-decEq {a = StringType} {b = IntType} = No $ intStringImpossible . sym
-decEq {a = BoolType} {b = StringType} = No boolStringImpossible 
-decEq {a = StringType} {b = BoolType} = No $ boolStringImpossible . sym
-
-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 : { t : ExprType } -> 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))

content/blog/backend_math_rendering.md

@@ -42,9 +42,9 @@ 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.
+* As before I would generate my pages using Hugo.
+* I would use the KaTeX NPM package to rendering math.
+* To build the website no matter what computer 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.
@@ -119,12 +119,9 @@ 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. 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.
+math. There are no such easy answers for back-end rendering.
 
-There are two types of math on my website: inline math and display math.
+So what _do_ I do? Well, there are two types 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,
@@ -170,7 +167,7 @@ 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! Thus, we can't just
+it wouldn't be able to talk about LaTeX code! Thus, we can't just
 search-and-replace over the entire HTML document; we need to be context
 aware. This is where `nokigiri` comes in. We parse the HTML, and iterate
 over all of the 'text' nodes, calling `perform_katex_sub` on all
@@ -201,7 +198,7 @@ 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.
+* `[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.