code/typesafe-interpreter/TypesafeIntrV2.idr

@@ -18,15 +18,15 @@ boolStringImpossible : BoolType = StringType -> Void
 boolStringImpossible Refl impossible
 
 decEq : (a : ExprType) -> (b : ExprType) -> Dec (a = b)
-decEq 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
+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

content/blog/typesafe_interpreter_revisited.md

@@ -1,6 +1,7 @@
 ---
 title: Meaningfully Typechecking a Language in Idris, Revisited
 date: 2020-07-19T17:19:02-07:00
+draft: true
 tags: ["Idris"]
 ---
 
@@ -42,7 +43,7 @@ Let's start with the new `Expr` and `SafeExpr` types. Here they are:
 
 For `Expr`, the `IfElse` constructor is very straightforward. It takes
 three expressions: the condition, the 'then' branch, and the 'else' branch.
-With `SafeExpr` and `IfThenElse`, things are more rigid. The condition
+With `SafeExpr` and `IfThneElse`, 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
@@ -211,7 +212,7 @@ We can therefore write:
 replace'' : {x : ExprType} -> {y : ExprType} -> x = y -> SafeExpr x -> SafeExpr y
 ```
 
-This is exactly what we want! Given a proof that one `ExprType`, `x`, is equal to
+This is exactly what we want! Given a proof that one `ExprType`, `x` is equal to
 another `ExprType`, `y`, we can safely convert `SafeExpr x` to `SafeExpr y`.
 We will use this to convince the Idris typechecker to accept our program.
 
@@ -368,8 +369,7 @@ 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.
+without having to manually create different types of expressions like `ArithExpr` and `BoolExpr`.
 
 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.