plfa.github.io
plfa.github.io copied to clipboard
plfa
Exercise Suggestion: Pi-syntax
Hi. I like this book a lot, but I think it could have more exercises. In the quantifiers chapter, there's an example on the use of the syntax keyword that introduces the existential quantifier. As an extra exercise, I defined a datatype that captures dependent functions and declared a syntax similar to the Sigma syntax. The Pi type turned out to be almost the same as Sigma type, only with different associativity in the type of the value constructor. I think that making this discovery might be useful for newcomers like myself. It helps to appreciate the difference between dependent sum and product types.
@jllang I'm pretty sure you can do this just fine without defining a datatype for it. Just a bit of syntax should be enough.
Wow, I even managed to define an infix arrow syntax x ↦ M corresponding with λ x → M constructing values of my Pi type!
@jllang They're pretty special, in the sense that you can't pattern match on their structure. Their syntax is also special, as it's a special case in the parser, e.g., you can't hide function arrows and define your own replacement.
OK, that's true. Still, I'm quite surprised that I could define my own lambda abstraction equivalent, as well as the Pi type.
If you want to propose a new exercise for the book, please submit it in a pull request and I will be happy to review it. From the description above, it wasn't clear to me exactly what you had in mind.
