Web-Projects
/
blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Edit and publish typesafe interpreter.

This commit is contained in:
Danila Fedorin 2020-07-22 14:35:19 -07:00
parent b078ef9a22
commit e59b8cf403
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
content/blog/typesafe_interpreter_revisited.md
View File

@ -1,7 +1,6 @@
--- ---
title: Meaningfully Typechecking a Language in Idris, Revisited title: Meaningfully Typechecking a Language in Idris, Revisited
date: 2020-07-19T17:19:02-07:00 date: 2020-07-19T17:19:02-07:00
draft: true
tags: ["Idris"] 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 For `Expr`, the `IfElse` constructor is very straightforward. It takes
three expressions: the condition, the 'then' branch, and the 'else' branch. 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 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 `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 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 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`. 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. 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 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 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 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. [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.