Compare commits
No commits in common. "068d0218b0fbbbfc6cd200fd0c268b9cdab1e15f" and "7623787b1cbb16e73ba5caf326bbe40ac50855a7" have entirely different histories.
068d0218b0
...
7623787b1c
@ -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
|
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,
|
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
|
and instead decided to pattern match on types inside of `typecheck`, we would've quickly
|
||||||
found that this only works for languages with finitely many types. When we add polymorphic tuples
|
found that this only works for types with finitely many values. When we add polymorphic tuples
|
||||||
and lists, we start being able to construct an arbitrary number of types: `[a]`. `[[a]]`, and
|
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
|
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`.
|
solution. I think that this leads us back to `decEq`.
|
||||||
|
@ -54,10 +54,6 @@ div.highlight table {
|
|||||||
code {
|
code {
|
||||||
border: none;
|
border: none;
|
||||||
}
|
}
|
||||||
|
|
||||||
span {
|
|
||||||
margin: 0 !important;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
.container {
|
.container {
|
||||||
|
Loading…
Reference in New Issue
Block a user