From e59b8cf4033eaa78bde8c7426566d15fbc89ed7e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 22 Jul 2020 14:35:19 -0700 Subject: [PATCH] Edit and publish typesafe interpreter. --- content/blog/typesafe_interpreter_revisited.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/content/blog/typesafe_interpreter_revisited.md b/content/blog/typesafe_interpreter_revisited.md index 4a75a99..1b16d92 100644 --- a/content/blog/typesafe_interpreter_revisited.md +++ b/content/blog/typesafe_interpreter_revisited.md @@ -1,7 +1,6 @@ --- title: Meaningfully Typechecking a Language in Idris, Revisited date: 2020-07-19T17:19:02-07:00 -draft: true tags: ["Idris"] --- @@ -43,7 +42,7 @@ Let's start with the new `Expr` and `SafeExpr` types. Here they are: For `Expr`, the `IfElse` constructor is very straightforward. It takes three expressions: the condition, the 'then' branch, and the 'else' branch. -With `SafeExpr` and `IfThneElse`, things are more rigid. The condition +With `SafeExpr` and `IfThenElse`, things are more rigid. The condition of the expression has to be of a boolean type, so we make the first argument `SafeExpr BoolType`. Also, the two branches of the if-expression have to be of the same type. We encode this by making both of the input expressions @@ -212,7 +211,7 @@ We can therefore write: replace'' : {x : ExprType} -> {y : ExprType} -> x = y -> SafeExpr x -> SafeExpr y ``` -This is exactly what we want! Given a proof that one `ExprType`, `x` is equal to +This is exactly what we want! Given a proof that one `ExprType`, `x`, is equal to another `ExprType`, `y`, we can safely convert `SafeExpr x` to `SafeExpr y`. We will use this to convince the Idris typechecker to accept our program. @@ -369,7 +368,8 @@ solution. I think that this leads us back to `decEq`. I also hope that I've now redeemed myself as far as logical arguments go. We used dependent types and made our typechecking function save us from error-checking during evaluation. We did this -without having to manually create different types of expressions like `ArithExpr` and `BoolExpr`. +without having to manually create different types of expressions like `ArithExpr` and `BoolExpr`, +and without having to duplicate any code. That's all I have for today, thank you for reading! As always, you can check out the [full source code for the typechecker and interpreter](https://dev.danilafe.com/Web-Projects/blog-static/src/branch/master/code/typesafe-interpreter/TypesafeIntrV2.idr) on my Git server.