diff --git a/content/blog/typesafe_imperative_lang.md b/content/blog/typesafe_imperative_lang.md index 88a5e68..050c115 100644 --- a/content/blog/typesafe_imperative_lang.md +++ b/content/blog/typesafe_imperative_lang.md @@ -1,8 +1,7 @@ --- title: "A Typesafe Representation of an Imperative Language" -date: 2020-10-30T17:19:59-07:00 +date: 2020-11-02T01:07:21-08:00 tags: ["Idris"] -draft: true --- A recent homework assignment for my university's programming languages @@ -85,7 +84,7 @@ can evaluate to either a boolean or an integer value (because a register can contain either of those types of values). Perhaps we can specify the type that an expression evaluates to in the expression's own type: `Expr IntTy` would evaluate to integers, and `Expr BoolTy` would evaluate -to booleans. Then, we could constructors as follows: +to booleans. Then, we could have constructors as follows: ```Idris Lit : Int -> Expr IntTy @@ -360,7 +359,7 @@ pattern matching: The `getReg` function will take out the value of the corresponding register, returning `Int` or `Bool` depending on the `TypeState`. What's important is that if the `TypeState` is known, then so -is the type of `getReg`: no `Either` is involved her, and we +is the type of `getReg`: no `Either` is involved here, and we can directly use the integer or boolean stored in the register. This is exactly what we do: @@ -453,7 +452,7 @@ We then have: MkState (0, 9, 63) : State (IntTy, IntTy, IntTy) ``` -Which seems correct! The program multiplies seven by nine, +This seems correct! The program multiplies seven by nine, and stops when register `A` reaches zero. Our test program runs, too: @@ -473,7 +472,5 @@ aren't possible: our programs are guaranteed to be {{< sidenote "right" "termination-note" "type correct." >}} Our programs aren't guaranteed to terminate: we're lucky that Idris' totality checker is turned off by default. -{{< /sidenote >}} - -This was a fun exercise, and I hope you enjoyed reading along! +{{< /sidenote >}} This was a fun exercise, and I hope you enjoyed reading along! I hope to see you in my future posts.