|
|
|
@ -361,7 +361,7 @@ I think this is a good approach. Should we want to add more types to our languag |
|
|
|
|
lists, and so on, we will be able to extend our `decEq` approach to construct more complex equality |
|
|
|
|
proofs, and keep the `typecheck` method the same. Had we not used this approach, |
|
|
|
|
and instead decided to pattern match on types inside of `typecheck`, we would've quickly |
|
|
|
|
found that this only works for types with finitely many values. When we add polymorphic tuples |
|
|
|
|
found that this only works for languages with finitely many types. When we add polymorphic tuples |
|
|
|
|
and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and |
|
|
|
|
so on. Then, we cease to be able to enumerate all possible pairs of types, and require a recursive |
|
|
|
|
solution. I think that this leads us back to `decEq`. |
|
|
|
|