Add Homework 6

DeBruijn.hs

@@ -0,0 +1,454 @@
+-- | This module illustrates beta-reduction on nameless lambda calculus
+--   terms using de Bruijn indexes.
+module DeBruijn where
+
+import Prelude hiding (print,and,or,not,pred,succ,fst,snd,either,length,sum,product)
+
+
+--
+-- * Syntax
+--
+
+-- ** Abstract syntax
+
+-- | The de Bruijn index of a variable.
+type Var = Int
+
+-- | Nameless lambda calculus terms. Note that we can check alpha-equivalence
+--   with plain old Haskell (==). This is a more complicated and expensive
+--   operation in named lambda calculuses.
+data Exp
+   = Ref Var       -- ^ variable reference
+   | App Exp Exp   -- ^ application
+   | Abs Exp       -- ^ lambda abstraction
+  deriving (Eq,Show)
+ 
+
+-- ** Syntactic sugar
+
+-- | Build an abstraction that takes two arguments.
+abs2 :: Exp -> Exp
+abs2 = Abs . Abs
+
+-- | Build an abstraction that takes three arguments.
+abs3 :: Exp -> Exp
+abs3 = abs2 . Abs
+
+-- | Build an abstraction that takes four arguments.
+abs4 :: Exp -> Exp
+abs4 = abs3 . Abs
+
+-- | Build an application to apply a function to two arguments.
+app2 :: Exp -> Exp -> Exp -> Exp
+app2 f e1 e2 = App (App f e1) e2
+
+-- | Build an application to apply a function to three arguments.
+app3 :: Exp -> Exp -> Exp -> Exp -> Exp
+app3 f e1 e2 e3 = App (app2 f e1 e2) e3
+
+-- | Build an application to apply a function to four arguments.
+app4 :: Exp -> Exp -> Exp -> Exp -> Exp -> Exp
+app4 f e1 e2 e3 e4 = App (app3 f e1 e2 e3) e4
+
+
+-- ** Pretty printing
+
+-- | Pretty print a nameless lambda calculus expression.
+pretty :: Exp -> String
+pretty e = case e of
+    Ref x   -> show x
+    Abs e   -> "λ" ++ pretty e
+    App l r -> inAppL l ++ " " ++ group r
+  where
+    group (Ref x) = show x
+    group e       = "(" ++ pretty e ++ ")"
+    inAppL (App l r) = inAppL l ++ " " ++ group r
+    inAppL e         = group e
+
+-- | Print a pretty-printed lambda calculus expression to standard output.
+print :: Exp -> IO ()
+print = putStrLn . pretty
+
+
+--
+-- * Semantics
+--
+
+-- ** Substitution
+
+-- | Variable substitution. `sub x arg e` substitues arg for every x in e.
+--
+--   Both the abstraction and reference cases are interesting.
+--
+--   Each time we enter a new abstraction in e, we must:
+--    1. Increment the x that we're looking for.
+--    2. Increment all of the free variables in arg since now the references
+--       will have to skip over one more lambda to get to the lambda they
+--       refer to.
+--
+--   For each variable reference y in e, there are three possibilities:
+--     1. It's the variable x we're looking for, in which case we replace it.
+--     2. It's a variable bound in e (y < x), in which case we do nothing.
+--     3. It's a variable that is free in e (y > x), in which case we
+--        decrement it since now the reference has to skip over one less
+--        lambda (i.e. the lambda that we beta-reduced away) to get to the
+--        lambda it refers to.
+--   
+--   >>> sub 0 (Ref 1) (Abs (Ref 1))
+--   Abs (Ref 2)
+--
+sub :: Var -> Exp -> Exp -> Exp
+sub x arg (App l r) = App (sub x arg l) (sub x arg r)
+sub x arg (Abs e)  = Abs (sub (x+1) (inc 0 arg) e)
+sub x arg (Ref y)
+    | y == x = arg        -- found an x, replace it!
+    | y < x  = Ref y      -- not x and bound in e, leave it alone
+    | y > x  = Ref (y-1)  -- not x and free in e, decrement it
+
+-- | Increment the free variables in an expression.
+-- 
+--   The argument d (for "depth") indicates the number of abstractions we
+--   have recursed into so far. A variable that is smaller than the depth
+--   is not free, and so should not be incremented.
+--
+--   >>> inc 0 (Ref 0)
+--   Ref 1
+--
+--   >>> inc 0 (App (Ref 1) (Abs (Ref 0)))
+--   App (Ref 2) (Abs (Ref 0))
+--
+inc :: Int -> Exp -> Exp
+inc d (App l r) = App (inc d l) (inc d r)
+inc d (Abs e)   = Abs (inc (d+1) e)
+inc d (Ref x)   = Ref (if x < d then x else x+1)
+
+
+-- ** Small-step semantics
+
+-- | Do one step of normal order reduction and return the result.
+--   If no redex is found, return Nothing.
+--
+--   The first case matches a redex and does a substitution. The rest of
+--   the cases implement a search for next redex.
+--
+--   >>> step (App (Abs (Ref 0)) (Ref 1))
+--   Just (Ref 1)
+--
+--   >>> step (App (abs2 (App (Ref 0) (Ref 1))) (Ref 2))
+--   Just (Abs (App (Ref 0) (Ref 3)))
+--
+--   >>> step (App (abs2 (App (Ref 2) (Ref 1))) (Ref 0))
+--   Just (Abs (App (Ref 1) (Ref 1)))
+--
+step :: Exp -> Maybe Exp
+step (App (Abs e) r) = Just (sub 0 r e)  -- found a redex, do beta reduction!
+step (App l r)       = case step l of
+                         Just l' -> Just (App l' r)
+                         Nothing -> fmap (App l) (step r)
+step (Abs e)         = fmap Abs (step e)
+step (Ref _)         = Nothing
+
+
+-- | Evaluate an expression to normal form using normal order recution.
+--   Return a list of expressions produced by each step of reduction.
+--   Note that this list may be infinite if the reduction never reaches
+--   a normal form!
+steps :: Exp -> [Exp]
+steps e = e : case step e of
+                Nothing -> []
+                Just e' -> steps e'
+
+-- | Evaluate an expression to normal form using normal order reduction.
+--   Note that this function will not terminate if the reduction never
+--   reaches a normal form!
+eval :: Exp -> Exp
+eval = last . steps
+
+-- | Print a reduction sequence for an expression.
+printReduce :: Exp -> IO ()
+printReduce = mapM_ print . steps
+
+
+--
+-- * Church encodings
+--
+
+-- ** Church booleans
+
+-- | λxy.x
+true :: Exp
+true = abs2 (Ref 1)
+
+-- | λxy.y
+false :: Exp
+false = abs2 (Ref 0)
+
+-- | λbte.bte
+if_ :: Exp
+if_ = abs3 (app2 (Ref 2) (Ref 1) (Ref 0))
+
+-- | λb. if b false true
+not :: Exp
+not = Abs (app3 if_ (Ref 0) false true)
+
+-- | λpq. if p q p
+and :: Exp
+and = abs2 (app3 if_ (Ref 1) (Ref 0) (Ref 1))
+
+-- | λpq. if p p q
+or :: Exp
+or = abs2 (app3 if_ (Ref 1) (Ref 1) (Ref 0))
+
+-- | Church Boolean tests:
+--
+--   >>> true == eval (app2 and (app2 or false true) (App not false))
+--   True
+--   
+--   >>> false == eval (app2 or (App not true) (app2 and true false))
+--   True
+
+
+-- ** Church numerals
+
+-- | λfx.x
+zero :: Exp
+zero = abs2 (Ref 0)
+
+-- | λfx.fx
+one :: Exp
+one = abs2 (App (Ref 1) (Ref 0))
+
+-- | λfx.f(fx)
+two :: Exp
+two = abs2 (App (Ref 1) (App (Ref 1) (Ref 0)))
+
+-- | λfx.f(f(fx))
+three :: Exp
+three = abs2 (App (Ref 1) (App (Ref 1) (App (Ref 1) (Ref 0))))
+
+-- | Build a Church numeral for an arbitrary natural number.
+--   
+--   >>> map num [0,1,2,3] == [zero,one,two,three]
+--   True
+--
+num :: Int -> Exp
+num n = abs2 (help n (Ref 0))
+  where help 0 e = e
+        help n e = App (Ref 1) (help (n-1) e)
+
+-- | λnfx.f(nfx)
+succ :: Exp
+succ = abs3 (App (Ref 1) (app2 (Ref 2) (Ref 1) (Ref 0)))
+
+-- | λnmfx.nf(mfx)
+add :: Exp
+add = abs4 (app2 (Ref 3) (Ref 1) (app2 (Ref 2) (Ref 1) (Ref 0)))
+
+-- | λnmf.n(mf)
+mult :: Exp
+mult = abs3 (App (Ref 2) (App (Ref 1) (Ref 0)))
+
+-- | λn. n (λx.false) true
+isZero :: Exp
+isZero = Abs (app2 (Ref 0) (Abs false) true)
+
+-- | λnfx.n (λgh.h(gf)) (λu.x) (λu.u) 
+--
+--   See: https://en.wikipedia.org/wiki/Church_encoding#Derivation_of_predecessor_function
+pred :: Exp
+pred = abs3 (app3 (Ref 2) 
+                  (abs2 (App (Ref 0) (App (Ref 1) (Ref 3))))
+                  (Abs (Ref 1))
+                  (Abs (Ref 0)))
+
+-- | Church numeral tests:
+--
+--   >>> three == eval (app2 add two one)
+--   True
+--
+--   >>> num 15 == eval (app2 mult (app2 add two three) three)
+--   True
+--
+--   >>> num 5 == eval (App pred (num 6))
+--   True
+
+
+-- ** Church tuples
+
+-- | λxys.sxy
+--
+--   >>> two == eval (App fst (app2 pair two true))
+--   True
+--
+--   >>> true == eval (App snd (app2 pair two true))
+--   True
+--
+pair :: Exp
+pair = abs3 (app2 (Ref 0) (Ref 2) (Ref 1))
+
+-- | λt.t(λxy.x)
+fst :: Exp
+fst = Abs (App (Ref 0) true)
+
+-- | λt.t(λxy.y)
+snd :: Exp
+snd = Abs (App (Ref 0) false)
+
+-- | λxyzs.sxyz
+--
+--   >>> one == eval (App sel13 (app3 tuple3 one two three))
+--   True
+--
+--   >>> two == eval (App sel23 (app3 tuple3 one two three))
+--   True
+--
+--   >>> three == eval (App sel33 (app3 tuple3 one two three))
+--   True
+--
+tuple3 :: Exp
+tuple3 = abs4 (app3 (Ref 0) (Ref 3) (Ref 2) (Ref 1))
+
+-- | λt.t(λxyz.x)
+sel13 :: Exp
+sel13 = Abs (App (Ref 0) (abs3 (Ref 2)))
+
+-- | λt.t(λxyz.y)
+sel23 :: Exp
+sel23 = Abs (App (Ref 0) (abs3 (Ref 1)))
+
+-- | λt.t(λxyz.z)
+sel33 :: Exp
+sel33 = Abs (App (Ref 0) (abs3 (Ref 0)))
+
+
+-- ** Church sums
+
+-- | λfgu.ufg
+--
+--   >>> three == eval (app3 either succ not (App inL two))
+--   True
+--
+--   >>> false == eval (app3 either succ not (App inR true))
+--   True
+--
+either :: Exp
+either = pair
+
+-- | λxfg.fx
+inL :: Exp
+inL = abs3 (App (Ref 1) (Ref 2))
+
+-- | λxfg.gx
+inR :: Exp
+inR = abs3 (App (Ref 0) (Ref 2))
+
+-- | λfghu.ufgh
+--
+--   >>> three == eval (app4 case3 succ not fst (App in13 two))
+--   True
+--
+--   >>> false == eval (app4 case3 succ not fst (App in23 true))
+--   True
+--
+--   >>> one == eval (app4 case3 succ not fst (App in33 (app2 pair one two)))
+--   True
+--
+case3 :: Exp
+case3 = tuple3
+
+-- | λxfgh.fx
+in13 :: Exp
+in13 = abs4 (App (Ref 2) (Ref 3))
+
+-- | λxfgh.gx
+in23 :: Exp
+in23 = abs4 (App (Ref 1) (Ref 3))
+
+-- | λxfgh.hx
+in33 :: Exp
+in33 = abs4 (App (Ref 0) (Ref 3))
+
+
+-- ** Fixpoint combinator
+
+-- | λf. (λx.f(xx)) (λx.f(xx))
+fix :: Exp
+fix = Abs (App (Abs (App (Ref 1) (App (Ref 0) (Ref 0))))
+               (Abs (App (Ref 1) (App (Ref 0) (Ref 0)))))
+
+-- | fix (λrn. if (isZero n) one (mult n (r (pred n))))
+--
+--   >>> num 6 == eval (App fac three)
+--   True
+--
+--   >>> num 24 == eval (App fac (num 4))
+--   True
+--
+fac :: Exp
+fac = App fix (abs2
+          (app3 if_
+                (App isZero (Ref 0))  -- condition
+                one                   -- base case
+                (app2 mult            -- recursive case
+                      (Ref 0)
+                      (App (Ref 1) (App pred (Ref 0))))))
+
+
+-- ** Church-encoded lists
+
+-- | inL (λx.x)
+nil :: Exp
+nil = App inL (Abs (Ref 0))
+
+-- | λht. inR (pair h t)
+cons :: Exp
+cons = abs2 (App inR (app2 pair (Ref 1) (Ref 0)))
+
+-- | fix (λrfbl. either (λx.b) (λp. f (fst p) (r f b (snd p))) l)
+fold :: Exp
+fold = App fix (abs4
+           (app3 either
+                 (Abs (Ref 2))
+                 (Abs (app2 (Ref 3) 
+                            (App fst (Ref 0)) 
+                            (app3 (Ref 4) (Ref 3) (Ref 2) (App snd (Ref 0)))))
+                 (Ref 0)))
+
+-- | Smart constructor to build a Church-encoded list of natural numbers.
+list :: [Int] -> Exp
+list = foldr (app2 cons . num) nil
+
+-- | fold (λh. add one) zero
+--
+--   >>> three == eval (App length (list [2,3,4]))
+--   True
+--
+length :: Exp
+length = app2 fold (Abs (App add one)) zero
+
+-- | fold add zero
+--
+--   >>> num 9 == eval (App sum (list [2,3,4]))
+--   True
+--
+--   >>> num 55 == eval (App sum (list [1..10]))
+--   True
+--
+sum :: Exp
+sum = app2 fold add zero
+
+-- | fold mult one
+--
+--   >>> num 24 == eval (App product (list [2,3,4]))
+--   True
+--
+product :: Exp
+product = app2 fold mult one
+
+-- | λf. fold (\h. cons (f h)) nil
+--
+--   >>> eval (list [4,5,6]) == eval (app2 map' (App add two) (list [2,3,4]))
+--   True
+--
+map' :: Exp
+map' = Abs (app2 fold (Abs (App cons (App (Ref 1) (Ref 0)))) nil)

HW4.idr

@@ -0,0 +1,46 @@
+data Ty = IntTy | BoolTy
+data Reg = A | B | R
+
+StateTy : Type
+StateTy = (Ty, Ty, Ty)
+
+getRegTy : Reg -> StateTy -> Ty
+getRegTy A (a, _, _) = a
+getRegTy B (_, b, _) = b
+getRegTy R (_, _, r) = r
+
+setRegTy : Reg -> Ty -> StateTy -> StateTy
+setRegTy A a (_, b, r) = (a, b, r)
+setRegTy B b (a, _, r) = (a, b, r)
+setRegTy R r (a, b, _) = (a, b, r)
+
+data Expr : StateTy -> Ty -> Type where
+  Lit : Int -> Expr s IntTy
+  Load : (r : Reg) -> Expr s (getRegTy r s)
+  Add : Expr s IntTy -> Expr s IntTy -> Expr s IntTy
+  Leq : Expr s IntTy -> Expr s IntTy -> Expr s BoolTy
+  Not : Expr s BoolTy -> Expr s BoolTy
+
+mutual
+  data Stmt : StateTy -> StateTy -> Type where
+    Store : (r : Reg) -> Expr s t -> Stmt s (setRegTy r t s)
+    If : Expr s BoolTy -> Prog s n -> Prog s n -> Stmt s n
+    Loop : Prog s s -> Stmt s s
+    Break : Stmt s s
+  
+  data Prog : StateTy -> StateTy -> Type where
+    Nil : Prog s s
+    (::) : Stmt s n -> Prog n m -> Prog s m
+
+initialState : StateTy
+initialState = (IntTy, IntTy, IntTy)
+
+testProg : Prog Main.initialState Main.initialState
+testProg =
+  [ Store A (Lit 1 `Leq` Lit 2)
+  , If (Load A)
+    [ Store A (Lit 1) ]
+    [ Store A (Lit 2) ]
+  , Store B (Lit 2)
+  , Store R (Add (Load A) (Load B))
+  ]

HW4.md

@@ -0,0 +1,265 @@
+# Part 1: Solution Discussion
+## Benjamin's Solution
+Looks like Ben opted to literally translate the `Prog` nonterminal into Haskell. This is perfectly valid: if anything, it's a more faithful translation of the syntax. However, as you probably know, the definition is isomorphic to a list:
+
+```Haskell
+data Prog = Empty | Stmt Stmt Prog
+data List Stmt = Nil | Cons Stmt (List Stmt)
+```
+
+So, you could've defined `Prog` to be `[Stmt]`. There are a few small advantages to this, mostly in terms of using Haskell as a metalanguage. Here's a line from my interpreter for this language:
+
+```Haskell
+stmt (Loop p) = prog (cycle p) `catchError` (const $ return ())
+```
+
+In order to implement the looping behavior of `Loop`, I used Haskell's built-in `cycle :: [a] -> [a]` function. This function infinitely repeats a list:
+
+```
+cycle [1,2,3] = [1,2,3,1,2,3,1,2,3,...]
+```
+
+The more compact list notation is another advantage to this approach. 
+
+I appreciated the following comment in the code:
+
+```
+- Starting register A at x, set R to zero, and add to R until A passes y (my approach above)
+- Same as above, but use y-x as the boundary instead of y, and adjust accordingly
+- Don't use a do loop, and instead hardcode out y-x additions of x+1 each time
+```
+
+What about a closed form approach? Something like `(b-a+1)(b+a)/2`. If `*` and `/` were O(1) operations, this would make the whole summation O(1). 
+
+## Owen's Solution
+Looks like Owen had some trouble with this homework assignment. From what I can tell, the code should not compile; there are a few things here that can be improved.
+
+### Allowing `Expr` to be `Int`
+I'm looking at this line of code:
+
+```Haskell
+-- since there is already an int type in Haskell, I think I can consider it already encoded
+data Expr = Int
+```
+
+Unfortunately, this isn't quite right. This creates a constructor (value!) `Int` of type `Expr`. This value `Int` has nothing to do with the type `Int` (integers). Thus, `Expr` can't contain integers like you intended. The proper syntax would be
+something like:
+
+```Haskell
+data Expr = Lit Int 
+```
+
+Unlike the previous version, this will create a constructor called `Lit` with type `Int -> Expr`. _This_ time, the `Int` refers to the type `Int`, and so, `Lit 3` will represent an expression that contains the number `3`.
+
+### Defining `Reg`
+Haskell's `type` is a way to create a _type alias_. So, if you have a type you use a lot (perhaps `Maybe String`), you
+can give it another name:
+
+```Haskell
+type MyType = Maybe String
+```
+
+Then, `Maybe String` and `MyType` mean the same thing. For defining `Reg`, you want to use `data`:
+
+```Haskell
+data Reg = A | B | C
+```
+
+### Using `undefined` or `_holes`
+It's hard to get the whole program compiling in one go. Haskell supports placeholders, which can be used anywhere, and will compile (mostly) no matter what. Of course, they'll either crash at runtime (`undefined`) or not _really_ compile (`_holes`). However, if you have something like:
+
+```Haskell
+while = -- can't quite do this yet
+
+sumFromTo = ... -- but now there's a parse error!
+```
+
+You can use `undefined`:
+
+```Haskell
+while = undefined
+```
+
+This way, there's no parse error, and GHC goes on to check the rest of your program. Holes are useful when you're in the middle of a complicated expression:
+
+```Haskell
+foldr _help 1 [1,2,3]
+```
+This will almost compile, except that at the very end, Haskell will tell you the type of the expression you need to fill in for `_help`. It will also suggest what you can put for `_help`!
+
+### Parenthesization
+This is a small nitpick. Instead of writing `RegStore A (x)`, you would write `RegStore A x`. In this case, you probably wanted `RegStore A (Lit x)` (you do need parentheses here!).
+
+### Making Type Errors Impossible
+I'm looking at this part of Part 2:
+
+```Haskell
+data Stmt = RegStore Reg IntExpr
+	| RegStore Reg BoolExpr
+	| Contitional IntExpr Prog Prog
+	| Contitional BoolExpr Prog Prog
+	| Loop Prog
+	| BreakLoop
+```
+
+You were on the right track! 
+
+> I think this should make it so that I have the full functionality of the previous setting but now I have one version for each type of expr?
+
+You're exactly right. You can represent any program from Part 1 using this syntax. However, the point was: you don't need to! Programs in the form `Conditional IntExpr Prog Prog` are specifcally __broken__! You can't use a number as a condition for `if/then/else`, and  `IntExpr` is guaranteed to produce a number! The same is true for `RegStore Reg BoolExpr`: you aren't allowed to store booleans into registers! See this part of the homework description: 
+
+> Note that although the expression language may produce both booleans and integers, the registers may only contain integers.
+
+So, it is in fact sufficient to leave out the duplicate constructors you have:
+
+```Haskell
+data Stmt = RegStore Reg IntExpr
+	| Contitional BoolExpr Prog Prog
+	| Loop Prog
+	| BreakLoop
+```
+
+Hope all this helps!
+
+## Jaspal's Solution
+Notably different in Jaspal's solution from the others in this group is that they used strings for registers instead of a data type definition. I think this was allowed by this homework assignment; however, I think that using a data type is better for our purposes. 
+
+The issue is, if your register is a string, it can be _any_ string. You can have register `"A"`, register `"a"`, register `"Hello World"`, and so on. But our language only has three registers: `A`, `B`, and `R`. If we define a data type as follows:
+
+```Haskell
+data Reg = A | B | R
+```
+
+Then a value of type `Reg` can _only_ be either `A`, `B`, or `R`. This means that we can't represent programs like
+
+```
+Hello := 5
+```
+
+Which is good!
+
+This solution also uses variables to encode programs. I think that's a nice touch! It makes some expressions
+less bulky than they otherwise would be.
+
+It doesn't look like the code compiles; here are a few things you can do to bring it closer to a working state.
+
+### Type Names and Constructor Names
+Type names (`Expr`, `Int`, `Bool`) all _have to_ start with an uppercase letter. Thus, you should change the following line:
+
+```Haskell
+data expr
+```
+
+To the following:
+
+```Haskell
+data Expr
+```
+
+And so on.
+
+The exception to this rule is _type variables_ for when things are _polymorphic_. For instance, we have
+
+```Haskell
+data Maybe a = Nothing | Just a
+```
+
+Here, `a` _is_ lowercase, but tht's because `a` is actually a _placeholder_ for an arbitrary type. You can tell because
+it also occurs on the left side of the `=` : `data Maybe a`. 
+
+Constructor names also have to start with an uppercase letter. So, you would have:
+
+```Haskell
+data Stmt
+  = Eql Reg Expr 
+  | IfElse Expr Prog Prog 
+  | Do Prog 
+  | Break 
+```
+
+### String Notation
+I have made a case that you _shouldn't_ be using strings for this homework. However, you'll probably use them in the future. So, I want to point out: `'A'` does _not_ mean the string "A". It means a single _character_, like `'A'` in C. To create a String in Haskell, you want to use double quotes: `"A"`.
+
+Other than those two things, it looks like this should work!
+
+## 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:
+
+```Haskell
+data Expr a where
+    Lit :: Int -> Expr Int
+    Reg :: Reg -> Expr Int
+    Plus :: Expr Int -> Expr Int -> Expr Int
+    Leq :: Expr Int -> Expr Int -> Expr Bool
+    Not :: Expr Bool -> Expr Bool
+```
+
+This defines an `Expr` type that's parameterized by a type `a`. I defined `a` to be "the type the expression evaluates to". So,
+
+* `Expr Int` is an expression that is guaranteed to produce an integer
+* `Expr Bool` is an expression that is guaranteed to produce a boolean.
+
+Unlike regular ADTs, you can restrict how one can create instances of `Expr a`. Thus, I can make it so that it's only possible to create `Expr Int` using `Lit` and `Reg`; the constructors `Plus`, `Leq`, and `Not` produce `Expr Bool`. 
+
+Why in the world would you use this? The benefits aren't immediately obvious in this language; however, suppose you had a ternary expression like `a ? b : c` in C or C++. Using our `BExpr` and `IExpr` we'd have to add constructors to _both_:
+
+```Haskell
+data IExpr
+    = -- ...
+    | ITern BExpr IExpr IExpr
+    | -- ...
+    
+data BExpr
+    = -- ...
+    | BTern BExpr BExpr BExpr
+    | -- ...
+```
+
+However, using the GADT definition, you should just be able to write:
+
+```
+data Expr a where
+    -- ...
+    Tern :: Expr Bool -> Expr b -> Expr b -> Expr b
+```
+
+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!
+
+# 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__.

HW4Part1.hs

@@ -32,7 +32,7 @@ program =
     ]
 
 while :: Expr -> Prog -> Stmt
-while cond body = Loop $ If cond [] [ Break ] : body
+while cond body = Loop [ If cond body [ Break ] ]
 
 sumFromTo :: Int -> Int -> Prog
 sumFromTo f t =

HW4Part2.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+module HW4Part2 where
 {-
  - int ::= (any integer)
  -
@@ -18,7 +20,6 @@
  - prog ::= \epsilon | stmt; prog
  -}
 
-{-# LANGUAGE GADTs #-}
 import Control.Monad.Except
 import Control.Monad.State
 import Data.Bool

HW6.hs

@@ -0,0 +1,224 @@
+module HW6 where
+
+import Prelude hiding (print,and,or,not,pred,succ,fst,snd,either,length,sum,product)
+
+import DeBruijn
+
+
+--
+-- * Part 1: Nameless lambda calculus
+--
+
+-- | λx. (λx.x) x
+--
+--   >>> eval ex1
+--   Abs (Ref 0)
+--
+ex1 :: Exp
+ex1 = Abs (App (Abs (Ref 0)) (Ref 0))
+
+-- | (λxy.xz) z z
+--
+--   >>> eval ex2
+--   App (Ref 0) (Ref 0)
+--
+ex2 :: Exp
+ex2 = App (App (Abs (Abs (App (Ref 1) (Ref 2)))) (Ref 0)) (Ref 0)
+
+-- | λy. (λxy.yx) y z
+--
+--   >>> eval ex3
+--   Abs (App (Ref 1) (Ref 0))
+--   
+ex3 :: Exp
+ex3 = Abs (App (App (Abs (Abs (App (Ref 0) (Ref 1)))) (Ref 0)) (Ref 1))
+
+
+-- | Is the given nameless lambda calculus term a closed expression? That is,
+--   does it contain no free variables?
+--
+--   >>> closed (Ref 0)
+--   False
+--
+--   >>> closed (Abs (Ref 0))
+--   True
+--
+--   >>> closed (Abs (App (Ref 0) (Ref 1)))
+--   False
+--
+--   >>> closed (Abs (App (Abs (App (Ref 0) (Ref 1))) (Ref 0)))
+--   True
+--
+closed :: Exp -> Bool
+closed = cl 0
+    where
+        cl n (Ref i) = i < n
+        cl n (App l r) = cl n l && cl n r
+        cl n (Abs e) = cl (n+1) e
+
+
+--
+-- * Part 2: Church pair update functions
+--
+
+-- | Write a lambda calculus function that replaces the first element in a
+--   Church-encoded pair. The first argument to the function is the new
+--   first element, the second argument is the original pair.
+--
+--   >>> :{
+--     eval (app2 pair true (num 3)) ==
+--     eval (app2 setFst true (app2 pair (num 2) (num 3)))
+--   :}
+--   True
+--
+setFst :: Exp
+setFst = Abs $ Abs $ Abs $ App (Ref 1) (Abs $ Abs $ App (App (Ref 2) (Ref 4)) (Ref 0))
+    -- \x -> \p -> \f -> p (\a -> \b -> f x b)
+
+-- | Write a lambda calculus function that replaces the second element in a
+--   Church-encoded pair. The first argument to the function is the new
+--   second element, the second argument is the original pair.
+--
+--   >>> :{
+--     eval (app2 pair (num 2) true) ==
+--     eval (app2 setSnd true (app2 pair (num 2) (num 3)))
+--   :}
+--   True
+--
+setSnd :: Exp
+setSnd = Abs $ Abs $ Abs $ App (Ref 1) (Abs $ Abs $ App (App (Ref 2) (Ref 1)) (Ref 4))
+    -- \x -> \p -> \f -> p (\a -> \b -> f a x)
+
+--
+-- * Part 3: Church encoding a Haskell program
+--
+
+-- | Pretend Haskell's Int is restricted to Nats.
+type Nat = Int
+
+-- | A simple data for representing shapes.
+data Shape
+   = Circle    Nat
+   | Rectangle Nat Nat
+  deriving (Eq,Show)
+
+-- | A smart constructor for building squares.
+square :: Nat -> Shape
+square l = Rectangle l l
+
+-- | Compute the area of a shape using a rough approximation of pi.
+area :: Shape -> Nat
+area (Circle r)      = 3 * r * r
+area (Rectangle l w) = l * w
+
+-- | Compute the perimeter of a shape using a rough approximation of pi.
+perimeter :: Shape -> Nat
+perimeter (Circle r)      = 2 * 3 * r
+perimeter (Rectangle l w) = 2 * l + 2 * w
+
+-- | Encode the circle constructor as a lambda calculus term. The term
+--   should be a function that takes a Church-encoded natural number as input
+--   and produces a Church-encoded shape as output.
+circleExp :: Exp
+circleExp = inL
+
+-- | Encode the rectangle constructor as a lambda calculus term. The term
+--   should be a function that takes two Church-encoded natural numbers as
+--   input and produces a Church-encoded shape as output.
+rectangleExp :: Exp
+rectangleExp = Abs $ Abs $ App inR $ app2 pair (Ref 1) (Ref 0)
+
+-- | Convert a shape into a lambda calculus term. This function helps to
+--   illustrate how your encodings of the constructors should work.
+encodeShape :: Shape -> Exp
+encodeShape (Circle r)      = App circleExp (num r)
+encodeShape (Rectangle l w) = app2 rectangleExp (num l) (num w)
+
+-- | Encode the square function as a lambda calculus term.
+squareExp :: Exp
+squareExp = Abs $ app2 rectangleExp (Ref 0) (Ref 0)
+
+-- | Encode the area function as a lambda calculus term.
+areaExp :: Exp
+areaExp = Abs $ app2 (Ref 0)
+    (Abs $ app2 mult (num 3) (app2 mult (Ref 0) (Ref 0)))
+    (Abs $ App (Ref 0) mult)
+
+-- | Encode the perimeter function as a lambda calculus term.
+perimeterExp :: Exp
+perimeterExp = Abs $ app2 (Ref 0)
+    (Abs $ app2 mult (num 6) (Ref 0))
+    (Abs $ App (Ref 0) $ Abs $ Abs $ app2 mult (num 2) (app2 add (Ref 0) (Ref 1)))
+
+-- | Some tests of your lambda calculus encodings.
+--
+--   >>> :{
+--     checkEval (area (Circle 3))
+--       (App areaExp (App circleExp (num 3)))
+--   :}
+--   True
+--
+--   >>> :{
+--     checkEval (area (Rectangle 3 5))
+--       (App areaExp (app2 rectangleExp (num 3) (num 5)))
+--   :}
+--   True
+--
+--   >>> :{
+--     checkEval (area (square 4))
+--       (App areaExp (App squareExp (num 4)))
+--   :}
+--   True
+--
+--   >>> :{
+--     checkEval (perimeter (Circle 3))
+--       (App perimeterExp (App circleExp (num 3)))
+--   :}
+--   True
+--
+--   >>> :{
+--     checkEval (perimeter (Rectangle 3 5))
+--       (App perimeterExp (app2 rectangleExp (num 3) (num 5)))
+--   :}
+--   True
+--
+--   >>> :{
+--     checkEval (perimeter (square 4))
+--       (App perimeterExp (App squareExp (num 4)))
+--   :}
+--   True
+-- 
+checkEval :: Nat -> Exp -> Bool
+checkEval n e = num n == eval e
+
+-- Alright, extra practice, let's go.
+-- Part 1: 4-tuples (Bonus: n-tuples)
+absN :: Int -> Exp -> Exp
+absN n = flip (foldr $ const Abs) $ replicate n ()
+
+apps :: Exp -> [Exp] -> Exp
+apps e = foldl App e
+
+tupleN :: Int -> Exp
+tupleN n = absN (n+1) $ apps (Ref 0) $ map Ref $ [n, (n-1) .. 1]
+
+selN :: Int -> Int -> Exp
+selN n m = Abs $ App (Ref 0) $ absN m $ Ref $ m - n
+
+tuple4 :: Exp
+tuple4 = tupleN 4
+
+sel14 :: Exp
+sel14 = selN 1 4
+
+sel24 :: Exp
+sel24 = selN 2 4
+
+sel34 :: Exp
+sel34 = selN 3 4
+
+sel44 :: Exp
+sel44 = selN 4 4
+
+-- Wait, the extra credit practice is mostly mechanical?
+-- Boo!