Data & function encoding

Protocol Design
22

I’m responding to @cwgoes direct question “does this proposal make … sense to you”, where ‘this proposal’ refers to the post by @terence here.

I’m afraid that I don’t have a clear answer to this, but I can make some general comments:

  1. Generally speaking, expressing something simple in terms of primitives that are more complex, is not advised.
    There may be good reasons for this – e.g. if the more-complex primitives are inherently canonical (e.g. characterising the natural numbers as \omega); or fixed by some environment that we decide we want to live in (e.g. the impredicative characterisations that come out of System F) – but if so, this needs to be carefully justified. Such a justification is not evident to me from reading the text (though this may reflect a lack of background knowledge on my part, of course).
    Can such a justification be provided, preferably in elementary terms?

  2. The assertion “If we were to characterize FinSet in terms of finite limits and colimits (and exponential objects) rather than just finite products and coproducts” invites the question of why we would want to characterise FinSet in such terms in the first place (cf. previous point).
    I don’t mean this in a hostile way; it just seems to be assumed in the post that this is desirable. Why?

  3. Is some fixed type regime assumed here (Haskell? Idris? Something else?)? Or are we contemplating building one from scratch?

  4. A standard technique is to write down whatever types you want (just as they are and without trying to shoehorn them into another system) and develop intro- and elim-rules and a term language to populate them in Curry-Howard style. The discussion in this thread seems to invite such an analysis. Has this been considered?

2 Likes