Jacques Carette

Since stdlib amounts to multiple person-years' worth of effort, the first bit is passed no problem (and all the others from the same guidelines too). [Too bad my student's contributions...

So there's a problem with using the definitions in `Data.Rational.Properties`: the notion of `NonZero` that it uses is different than the notion that `AlmostLeftCancellative` uses. So I'm not sure we...

I like the shorter alternatives. If we have to put in the relation wrt which we're working, I'm wondering about putting it in the other order, i.e. `_≡↑⟨_⟩_`. I think...

I also would dislike the arrows inside the brackets. Having them after is better than inside [though not necessarily the best choice].

Email about chapter 4 sent.

The "generic" type of such a function would need dependent types (as it would depend on parameters $n$ and $k$), but any given instance would have $n$ and $k$ fixed,...

I was most definitely thinking of doing method 2. I don't quite understand why QuantityDict is involved though...

Can you expand on your above comment? I've simply forgotten the details, so I can't recall what the first 'involved' in your reply actually means (same with the two occurrences...

Ok, I've rebooted my brain on this issue. And I think the passage of time has helped. Originally, the elegance of trying to piggyback on Haskell's type system really appealed...

Re: bidirectional typing. It is covered in PLFA. This [Haskell implementation](https://github.com/samuela/bidirectional-typing) might be an easier read. The [informal explanation](https://proofassistants.stackexchange.com/questions/1090/what-is-bidirectional-type-checking) on SE is decent. You may also enjoy [this tutorial](https://davidchristiansen.dk/tutorials/bidirectional.pdf). We...