Today we reviewed some of the equality eliminators of Pie, including cong, replace, symm, and trans, and gave implementations of cong, symm, and trans in terms of replace. We considered briefly the ind-= eliminator, which appears to offer additional power over replace, although we're currently at a bit of a loss as to how to use it.
Please read through Chapter 13 for next time.
We worked through the proof double=twice, discovering how Pie handles equality as a type, including the use of cong, and trans.
Note that there will be no meeting on 10/23 (Prof. Kurtz has a College Council meeting), and so our next scheduled meeting is for 10/30.
For next time, read through Chapter 10.
We worked through a variety of functional programs in Pie, including a correct version of the concat program. Along the way, we discussed Π-types, and about how -> is a special case of Π.
For next time, read through the Recess following Chapter 7 of “The Little Typer.”
I've had an email list set up for our conspiracy. To join, just go to deep-state, provide your credentials, and you're good to go.
At our first meeting, we
We'll be moving to JCL 298.
Now that RSS readers are no longer really a thing, we should set up an email list to augment the blog.
I'd also like to suggest a slight extension to our agreement, as I believe it's realistic to work through Chapter 5, and that by doing so, we can possibly hold the “Little Typer” part of our conspiracy to three weeks.
As a final note, I observed during the seminar that the implementation of concat in the book is bogus, as it reverses its second argument. This raises the interesting problem of giving a correct implementation for concat, i.e., a version of append that relies on recursion on its second argument, and uses snoc to post-pend an element to a list. Please try. I have one, and would like to compare solutions next time.
