Finish discussion post for homework 4.

HW4.md

@@ -182,7 +182,7 @@ I have made a case that you _shouldn't_ be using strings for this homework. Howe
 
 Other than those two things, it looks like this should work!
 
-# My Solution
+## My Solution
 My solution to Part 1 is pretty much identical to everyone else's; I opted to use `Prog = [Stmt]` instead of defining a data type, but other than that, not much is different.
 
 I had some fun in Part 2, though. In particular, instead of creating two separate data types, `BExpr` and `IExpr`, I used a Generalized Algebraic Data Type (GADT). Thus, my code was as follows:
@@ -227,4 +227,39 @@ data Expr a where
 
 Which covers both `x ? 1 : 2` and `x ? true : false`, but doesn't allow `x ? true : 3` (which would be a type error). Using a GADT, the "bexpr" part of the abstract syntax maps to `Expr Bool`, and the "iexpr" part maps to `Expr Int`.
 
-I also wrote a quick interpreter using the Monad Transformer Library. Monads are one of the classic "what the heck is this" things in Haskell; someone once said there are more monad tutorials than Haskell programmers out there. I don't think I'm qualified to give a good explanation, but in short: I used a _state monad_ (which is basically a Haskell type that helps you keep track of changing variables) and an _exception monad_ (which implements exception handling similar to Java's `throw`) to implement the language. Every `Loop` was implicitly a `catch` clause, and `Break` was a `throw`. Thus, when you reached a break, you would immediately return to the innermost loop, and continue from there. Combined with a GADT for expressions, the evaluator turned out _really_ compact: less than 25 lines of actual code!
+I also wrote a quick interpreter using the Monad Transformer Library. Monads are one of the classic "what the heck is this" things in Haskell; someone once said there are more monad tutorials than Haskell programmers out there. I don't think I'm qualified to give a good explanation, but in short: I used a _state monad_ (which is basically a Haskell type that helps you keep track of changing variables) and an _exception monad_ (which implements exception handling similar to Java's `throw`) to implement the language. Every `Loop` was implicitly a `catch` clause, and `Break` was a `throw`. Thus, when you reached a break, you would immediately return to the innermost loop, and continue from there. Combined with a GADT for expressions, the evaluator turned out _really_ compact: less than 25 lines of actual code!
+
+# Part 2: Questions
+__Q__: What happens if you encode those programs using the data types you defined in Part 1?
+
+__A__: Well, not much. The program is accepted, even though it's not type-correct. Haskell doesn't have any issues with it; however, were we to write an interpreter, we would quickly notice that although Haskell accepts the program, it's aware of the possibility of invalid cases; our interpreter would need to account for the possibility of expressions evaluating both to integers and to booleans.
+
+__Q__: What happens if you encode them using (a correct version of) the data types you defined in Part 2?
+
+__A__: Haskell rejects the program. We've "made illegal states unrepresentable" by one way or another teaching the Haskell type systems that integer and boolean expressions can't arbitrarily mix. An interpreter would not require error handling, since type errors were eliminated using the metalanguage's type system.
+
+__Q__: What does this tell you about the relationship between errors in your object language and errors in the metalanguage of Haskell?
+
+__A__: The way I see it, a metalanguage is merely a toolbox for working with our object language. By specifying our data types in a different way, we are effectively configuring the toolbox to work differently. In this specific case, we've given this "toolbox" a primitive understanding of our language's semantics, and it is able to automatically reason about basic "correctness" properties of programs. In terms of the two types of errors, we've shifted the errors from the object language into the meta language.
+
+__Q__: Can type errors always be eliminated from a language by refactoring the syntax in this way? Provide a brief rationale for your answer.
+
+__A__: Not in general, no. Suppose we allowed registers to include booleans, too. Type errors could still occur at runtime. Perhaps something like the following:
+
+```
+try {
+    someFunction();
+    A = true;
+} catch(error) {
+    A = 1
+}
+if A then B = 1 else B = 2 end
+```
+
+Determining whether or not a function terminates in an error state, is, as far as I know, undecidable. Thus, if our type system could reject something like this, it would be quite an impressive system!
+
+I think the general thought is: if our type system is static, it's likely possible to include all the necessary checks into the abstract syntax. Perhaps not in Haskell, but in a language like Idris or Coq. However, as soon as we make our types dynamic, it becomes impossible to accept precisely all valid programs in a language, and nothing more.
+
+Although.... some type systems are in themselves undecideable. So maybe even for a static type system, things may not be as easy.
+
+TL;DR: __No__.