3 ms·

from 2.1 集合论 p17 of https://www.cs.toronto.edu/~hehner/aPToP/chineseaPToP.pdf https://www.cs.toronto.edu/~hehner/aPToP/chineseaPToP.pdf > 可以有集合的集合, 表的表, 但没有束的束

from 2.1 集合论 p17 of https://www.cs.toronto.edu/~hehner/aPToP/chineseaPToP.pdf https://www.cs.toronto.edu/~hehner/aPToP/chineseaPToP.pdf > 可以有集合的集合, 表的表, 但没有束的束和串的串。 You'll notice that often CS papers will get the equivalent of bunches by declaring an abuse of notation such that the singleton E is to be interpreted as {E}, and Haskell gets the equivalent of strings by putting the burden of proof of following the "monad laws" on the implementer/user of a monad, but I think it simplifies things if the very notation already has monoidicity baked into it. (that's the UX argument: the CX [compiler experience] argument is that by making monoidal values explicit, we give our implementations a clear signal that they have lots of freedom to rearrange the computation as written into an order which sympathises with the machinery)

gsf_emergency 2y ago
Simplified but care-full application of notation: "no empty bunches"? And (,much less care-fully maybe a little machinationally,) what do you call the op that maps bunches to open sets and sets to closed sets? 空即是合，束不可空 (expectedly trad) Somehow.. Hehner could be better rendered in Classical..
- 082349872349872 2y ago
  the empty bunch (unit for `,`) is usually[0] spelled null. I don't recall that Hehner goes as far as topology (his bunches behave in a boolean manner, so the elementary bunches must all be clopen; going beyond his windowless[1] functions was my inspiration for attempting Junk) so he doesn't have any affordance for open/closed. [0] 名可名也，非一名也。I sometimes wonder why Dijkstra footnoted that if it were allowed in his guarded command notation, nullary if fi would be abort and do od, skip — but it's not allowed. It can't be a desire for uniqueness, because there are too many other different ways to write abort and skip. (although it would have been convenient were it to have been possible to syntactically distinguish skip from arbitrary code) [1] after spending years on Junk, I can very well appreciate why, even if he'd thought further, he chose to stop where he did for the book. That said, every few years he seems to manage to narrow the difference between lists and contiguous N->element functions a little more. (and at the moment I am not convinced that it's possible to make more than a pragmatic decision to declare a particular partial order to be the <= at a given datatype, but I am convinced that it's helpful to declare the existence of a [clerical] total order over all datatypes — which leads to annoying subtleties with equality)
  - gsf_emergency 2y ago
    Thanks. It just felt like being unable to spell out the empty bunch should be as interesting as the nonexistence of bunches o' bunches. I've heard from the students of RLC that quotient types are potentially useful** so should I wait to find out from you when those subtleties turn out to be less annoying or schlep on my current path till I bump up against bumpkin-type*-related annoyances not entirely of my own making ? *Sum & product types,I'm either always told not to worry about them, or be asked to pay attention in a way that I think I probably shouldn't ** itswise.. for bits-schlepping often end up needing more marketing than it's worth, imex
    - 082349872349872 2y ago
      Re: quotient types, I believe so, even bitswise... but it's exactly the projection forgetting all that stuff that's in the same class as zero that's easier mathematically than computationally. (guess I should see what Lean does here) incidentally, rummaging by way of Hagino and Charity leads to Burstall87: http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-LFCS-87-25.pdf http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-L... (what Burstall has written as ind case is what we'd currently call fold) in particular, 5. Equational data types (cut down by eq's <== quotients) which has the interesting observation: > Notice that the initial algebra gives rise to an induction principle and to use this we have to invent a suitable predicate to prove by induction. This comes from the 'no junk' property of the initial algebra. The 'no confusion' property gives rise to inequations, and here to do proofs we have to invent a suitable discriminant function. There is some pleasant feeling of duality here.
      - gsf_emergency 2y ago
        So there's already pleasance?? Sorry, can't add anything substantive, but the following might save some time? https://proofassistants.stackexchange.com/questions/908/what-exactly-is-setoid-hell/927#927 https://proofassistants.stackexchange.com/questions/908/what... https://eprints.illc.uva.nl/id/document/12673 https://eprints.illc.uva.nl/id/document/12673

gsf_emergency 2y ago

Simplified but care-full application of notation: "no empty bunches"? And (,much less care-fully maybe a little machinationally,) what do you call the op that maps bunches to open sets and sets to closed sets? 空即是合，束不可空 (expectedly trad) Somehow.. Hehner could be better rendered in Classical..

082349872349872 2y ago
the empty bunch (unit for `,`) is usually[0] spelled null. I don't recall that Hehner goes as far as topology (his bunches behave in a boolean manner, so the elementary bunches must all be clopen; going beyond his windowless[1] functions was my inspiration for attempting Junk) so he doesn't have any affordance for open/closed. [0] 名可名也，非一名也。I sometimes wonder why Dijkstra footnoted that if it were allowed in his guarded command notation, nullary if fi would be abort and do od, skip — but it's not allowed. It can't be a desire for uniqueness, because there are too many other different ways to write abort and skip. (although it would have been convenient were it to have been possible to syntactically distinguish skip from arbitrary code) [1] after spending years on Junk, I can very well appreciate why, even if he'd thought further, he chose to stop where he did for the book. That said, every few years he seems to manage to narrow the difference between lists and contiguous N->element functions a little more. (and at the moment I am not convinced that it's possible to make more than a pragmatic decision to declare a particular partial order to be the <= at a given datatype, but I am convinced that it's helpful to declare the existence of a [clerical] total order over all datatypes — which leads to annoying subtleties with equality)
- gsf_emergency 2y ago
  Thanks. It just felt like being unable to spell out the empty bunch should be as interesting as the nonexistence of bunches o' bunches. I've heard from the students of RLC that quotient types are potentially useful** so should I wait to find out from you when those subtleties turn out to be less annoying or schlep on my current path till I bump up against bumpkin-type*-related annoyances not entirely of my own making ? *Sum & product types,I'm either always told not to worry about them, or be asked to pay attention in a way that I think I probably shouldn't ** itswise.. for bits-schlepping often end up needing more marketing than it's worth, imex
  - 082349872349872 2y ago
    Re: quotient types, I believe so, even bitswise... but it's exactly the projection forgetting all that stuff that's in the same class as zero that's easier mathematically than computationally. (guess I should see what Lean does here) incidentally, rummaging by way of Hagino and Charity leads to Burstall87: http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-LFCS-87-25.pdf http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-25/ECS-L... (what Burstall has written as ind case is what we'd currently call fold) in particular, 5. Equational data types (cut down by eq's <== quotients) which has the interesting observation: > Notice that the initial algebra gives rise to an induction principle and to use this we have to invent a suitable predicate to prove by induction. This comes from the 'no junk' property of the initial algebra. The 'no confusion' property gives rise to inequations, and here to do proofs we have to invent a suitable discriminant function. There is some pleasant feeling of duality here.
    - gsf_emergency 2y ago
      So there's already pleasance?? Sorry, can't add anything substantive, but the following might save some time? https://proofassistants.stackexchange.com/questions/908/what-exactly-is-setoid-hell/927#927 https://proofassistants.stackexchange.com/questions/908/what... https://eprints.illc.uva.nl/id/document/12673 https://eprints.illc.uva.nl/id/document/12673