From 7d2f78d25c3d0670c3ebcf62e58856e772c05fdb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 20 Jul 2020 13:56:07 -0700 Subject: [PATCH] Add links and make small clarifications. --- content/blog/typesafe_interpreter_revisited.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/content/blog/typesafe_interpreter_revisited.md b/content/blog/typesafe_interpreter_revisited.md index fe38bc7..4a75a99 100644 --- a/content/blog/typesafe_interpreter_revisited.md +++ b/content/blog/typesafe_interpreter_revisited.md @@ -8,9 +8,10 @@ tags: ["Idris"] Some time ago, I wrote a post titled [Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}). The gist of the post was as follows: * _Programming Language Fundamentals_ students were surprised that, despite -having run their expression through typechecking, they still had to +having run their expression through (object language) typechecking, they still had to have a `Maybe` type in their evaluation functions. This was due to -the fact that the type system was not certain that typechecking worked. +the fact that the (meta language) type system was not certain that +(object language) typechecking worked. * A potential solution was to write separate expression types such as `ArithExpr` and `BoolExpr`, which are known to produce booleans or integers. However, this required the re-implementation of most @@ -370,4 +371,5 @@ I also hope that I've now redeemed myself as far as logical arguments go. We use 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`. -That's all I have for today, thank you for reading! +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.