From 49469bdf12c66970fa7620e15cc6d87ed934f973 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 12 Aug 2020 15:43:22 -0700 Subject: [PATCH] Fix issues in typesafe interpreter article. --- content/blog/typesafe_interpreter_tuples.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/content/blog/typesafe_interpreter_tuples.md b/content/blog/typesafe_interpreter_tuples.md index 9e9e6ea..d2f2302 100644 --- a/content/blog/typesafe_interpreter_tuples.md +++ b/content/blog/typesafe_interpreter_tuples.md @@ -30,7 +30,7 @@ impossible to manually test every possible case in our typechecker, but our approach of returning `Dec (a = b)` will work just fine. ### Extending The Syntax -First, let's extend our existing language with expressions fpr +First, let's extend our existing language with expressions for tuples. For simplicity, let's use pairs `(a,b)` instead of general `n`-element tuples. This would make typechecking less cumbersome while still having the interesting effect of making the number of types in our language @@ -46,7 +46,7 @@ Our `Expr` data type, which allows ill-typed expressions, ends up as follows: I've highlighted the new lines. The additions consist of the `Pair` constructor, which represents the tuple expression `(a, b)`, and the `Fst` and `Snd` constructors, which represent the `fst e` and `snd e` expressions, respectively. In -a similar vein, we extend our `SafeExpr` GADT: +a similar manner, we extend our `SafeExpr` GADT: {{< codelines "Idris" "typesafe-interpreter/TypesafeIntrV3.idr" 41 49 "hl_lines=7 8 9" >}} @@ -93,7 +93,7 @@ Lines 14 through 16 are pretty simple; in this case, we can tell at a glance that the two types are equal, and Idris can infer an equality proof in the form of `Refl`. We return this proof by writing it in a `Just`. Line 23 is the catch-all case for any combination of types we didn't handle. -Any combination of types we don't handle is false, and thus, this case +Any combination of types we don't handle is invalid, and thus, this case returns `Nothing`. What about lines 17 through 22? This is the case for handling the equality @@ -131,7 +131,7 @@ we want to substitute? After all, of the following are possible: ```Idris PairType rt1 lt2 = PairType lt1 lt2 -- First lt1 replaced -PairType lt1 lt2 = PairType rt1 lt2 -- Second lt2 replaced +PairType lt1 lt2 = PairType rt1 lt2 -- Second lt1 replaced PairType rt1 lt2 = PairType rt1 lt2 -- Both replaced ``` @@ -147,7 +147,7 @@ t1 => PairType lt1 lt2 = PairType t1 lt2 t1 => PairType t1 lt2 = PairType t1 lt2 ``` -The highlighted function is the one we'll need to use to attain +The second function (highlighted) is the one we'll need to use to attain the desired result. Since `P` is an implicit argument to `replace`, we can explicitly provide it with `{P=...}`, leading to the following line: