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

Add links and make small clarifications.

Browse Source
This commit is contained in:
Danila Fedorin 2020-07-20 13:56:07 -07:00
parent 1f734a613c
commit 7d2f78d25c
1 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
content/blog/typesafe_interpreter_revisited.md
View File

@ -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.