Kindz

By Scott

Hey everyone! On Friday, round 2 of PFPL 43 on Singleton and Dependent Kinds went off famously, and next we move on to chapter 44, for realz this time. Meeting at the usual time and place, 6:30pm at Gamma Space on Friday Dec 9th.

We had a longer than usual off-topic welcoming discussion that veered into Acadian history and the social organization of early North American colonies. But with the arrival of Leo though we swung back on topic, into Singleton Kinds just after the equivalences 43.2 but before 43.3, where we went through the illustrative examples. We discussed subkinding quite a bit; in particular the relation expressed in 43.3, and I’m not sure we ever landed on a consensus of how to best interpret the meaning of the subkinding relation. We are planning to revisit the question after seeing more applications in the next chapter.

Dependent Kinds at first seemed like a natural extension of the previous section, however as we discussed them we identified several differences that we hadn’t noticed at first; for instance the covariance and contravariance relationships of the product and function kinds. We were able to put together some simple examples applying the different constructs, but I don’t think we ever hit on one that truly needed the full power of Dependent Kinds, so we will have to keep working on coming up with examples.

Near the end, Ben brought up the paper the five stages of accepting constructive mathematics which is worth taking a look at, for myself I think I’m out of denial and into bargaining myself…

Until next time, Scott