Start working on the improved type-safe interpreter.

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 {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 rendering math.
-* To build the website no matter what computer I was on, I would use Nix.
+* 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.
@@ -119,9 +119,12 @@ 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.
+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.
 
-So what _do_ I do? Well, there are two types on my website: inline math and display math.
+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,
@@ -167,7 +170,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 able to talk about LaTeX code! Thus, we can't just
+it wouldn't be possible 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
@@ -198,7 +201,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.