improved beta-equivalence

README.md

@@ -60,6 +60,10 @@ Some kind of definition system would be a difficult and substantial addition, bu
 
 Sidenote: With a definition system, I would greatly prefer Haskell-style type annotations to ML-style type annotations, though the latter are likely way easier to implement. It serves as a nice bit of documentation, de-clutters the function definition, and follows the familiar mathematical statement-proof structure.
 
+1.  TODO Add support for named free variables to `Expr`
+
+    I’m taking the locally nameless approach. Dealing with free variables as de Bruijn indices greater than the context sounds terrible. This requires adding support for δ reductions, as well as performing reductions and type checking operations in an environment. NOTE: I’ll probably want to use the [Reader monad](https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Reader.html).
+
 
 ### TODO Inference
 
@@ -68,12 +72,12 @@ Obviously not fully decidable, but I might be able to implement some basic unifi
 
 ### TODO Implicits
 
-Much, much more useful than [inference](#orgb6a8c28), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
+Much, much more useful than [inference](#orgb32d6a9), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none.
 
 
 ### TODO Universes?
 
-Not really necessary without [inductive definitions](#org136d92d), but could be fun.
+Not really necessary without [inductive definitions](#orgc763d54), but could be fun.
 
 
 ### TODO Inductive Definitions
@@ -101,9 +105,11 @@ For even better usage in the future, check out [optparse](https://hackage.haskel
 The error messages currently aren’t terrible, but it would be nice to have, e.g. line numbers. `megaparsec` allows for semantic errors, so somehow hook into that like what I’m doing for unbound variables?
 
 
-### TODO Improve β-equivalence check
+### DONE Improve β-equivalence check
 
-The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without [inductive definitions](#org136d92d)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it’s certainly not a bad idea.
+The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn’t the best strategy. This is much less of an issue without [inductive definitions](#orgc763d54)/recursion, as far less computation gets done in general, let alone at the type level. That being said, it’s certainly not a bad idea.
+
+Improved the β-equivalence check to first reduce both terms to WHNF then walk the syntax tree and recursively compare the terms. I figured this would be a necessary precondition to adding definitions, since fully normalizing everything with definitions (recursively unfolding all definitions) seems absolutely horrendous. Also implementing this wasn’t nearly as hard as I would have thought.
 
 
 ### DONE Better testing

README.org

@@ -54,6 +54,9 @@ Some kind of definition system would be a difficult and substantial addition, bu
 
 Sidenote: With a definition system, I would greatly prefer Haskell-style type annotations to ML-style type annotations, though the latter are likely way easier to implement. It serves as a nice bit of documentation, de-clutters the function definition, and follows the familiar mathematical statement-proof structure.
 
+**** TODO Add support for named free variables to =Expr=
+I'm taking the locally nameless approach. Dealing with free variables as de Bruijn indices greater than the context sounds terrible. This requires adding support for \delta reductions, as well as performing reductions and type checking operations in an environment. NOTE: I'll probably want to use the [[https://hackage.haskell.org/package/mtl-2.3.1/docs/Control-Monad-Reader.html][Reader monad]].
+
 *** TODO Inference
 Obviously not fully decidable, but I might be able to implement some basic unification algorithm. This isn't super necessary though, I find leaving off the types of arguments to generally be a bad idea, but in some cases it can be worth it.
 
@@ -79,9 +82,11 @@ For even better usage in the future, check out [[https://hackage.haskell.org/pac
 *** TODO Improve error messages
 The error messages currently aren't terrible, but it would be nice to have, e.g. line numbers. =megaparsec= allows for semantic errors, so somehow hook into that like what I'm doing for unbound variables?
 
-*** TODO Improve β-equivalence check
+*** DONE Improve β-equivalence check
 The check for β-equivalence could certainly be a lot smarter. Right now it just fully normalizes both terms and checks if the normal forms are equal, which isn't the best strategy. This is much less of an issue without [[Inductive Definitions][inductive definitions]]/recursion, as far less computation gets done in general, let alone at the type level. That being said, it's certainly not a bad idea.
 
+Improved the β-equivalence check to first reduce both terms to WHNF then walk the syntax tree and recursively compare the terms. I figured this would be a necessary precondition to adding definitions, since fully normalizing everything with definitions (recursively unfolding all definitions) seems absolutely horrendous. Also implementing this wasn't nearly as hard as I would have thought.
+
 *** DONE Better testing
 Using some kind of testing framework, like [[https://hackage.haskell.org/package/QuickCheck][QuickCheck]] and/or [[https://hackage.haskell.org/package/HUnit][HUnit]] seems like a good idea. I would like to avoid regressions as I keep working on this, and a suite of unit tests would make me feel much more comfortable.
 

lib/Expr.hs

@@ -133,5 +133,16 @@ betaNF e = if e == e' then e else betaNF e'
   where
     e' = betaReduce e
 
+whnf :: Expr -> Expr
+whnf (App (Abs _ _ v) n) = whnf $ subst 0 n v
+whnf e = e
+
 betaEquiv :: Expr -> Expr -> Bool
-betaEquiv = on (==) betaNF
+betaEquiv e1 e2
+    | e1 == e2 = True
+    | otherwise = case (whnf e1, whnf e2) of
+        (Var k1 _, Var k2 _) -> k1 == k2
+        (Star, Star) -> True
+        (Abs _ t1 v1, Abs _ t2 v2) -> betaEquiv t1 t2 && betaEquiv v1 v2
+        (Pi _ t1 v1, Pi _ t2 v2) -> betaEquiv t1 t2 && betaEquiv v1 v2
+        _ -> False -- remaining cases impossible or false