5 ms·

...and the homelab is a feminine art, while nursing is a masculine profession. Will have to read some BoJo[0] columns so I can manually do the style transfer, b

...and the homelab is a feminine art, while nursing is a masculine profession. Will have to read some BoJo[0] columns so I can manually do the style transfer, but sounds worth attempting. (though I still owe you lattice.ch) SPPL: wrt https://news.ycombinator.com/item?id=42416615 https://news.ycombinator.com/item?id=42416615 VR says: We harbor contempt for technology that is simpler than we perceive ourselves to be (unless you’re a particular sort of mystic seeking to become one with a simple tool like a sword...) but the key is that while the sword itself is a simple tool, the behaviours around it are complex: even at the highest level on one side, there are the legs, the hand(s), and the heart/head animating them (4H is not ecchi[1]); tensor that with all of those components from the dual side of the duel, and you wind up with a (largely incorporeal) technology[2] that is much more complex than its most distal tool: a piece of metal with very distinct moments of inertia. Come to think of it, could the reason that the Wii-swordplay minigame was ultimately so disappointing be the same reasoning the Original Greekstas were disappointed in scrolls? The lack of repartée?[3] [0] is ABdPJ post-literate? In one Covid-era address-from-home he appeared to have shelved not by-title or by-author but by-colour... [1] a friend once discovered that walking around Tokyo holding hands with his Harvard sweatshirt-clad boyfriend caused much tittering among the young ladies passing by; evidently a Bishie with a huge "H" was just too hilarious. [2] much of Bruce Lee's output seems strongly influenced by western fencing, but I don't know if that's just me parochially seeing only the terrain just under the lamppost[4]. Do you have any idea what, syntactically, I might search for to figure out how the chinese martial arts discussed control over distance? (and if, like the japanese, they also used the same term for temporal gaps?) [3] consider how many orders of magnitude Aramis covered, going between defending a line (2e1 ms) and writing a thesis to defend (1e11 ms?) [4] https://www.youtube.com/watch?v=YjXC4N1HXf0 https://www.youtube.com/watch?v=YjXC4N1HXf0 EDIT: forgot to mention that SSPL might lead us to Girardian logic, in a duel between code and data: with sum types, data has the initiative, and code must be ready, beforehand, to parry and riposte appropriately for all possibilities; with product types, code has the initiative, and data must be ready, beforehand, to parry and riposte appropriately for all possibilities. Eliminating sums is a projection operator on code; eliminating products is a projection operator on data.

gsf_emergency 2y ago
Didn't 成瀬関次 in 戦ふ日本刀 gripe that distance management as traditionally taught didn't make sense in actual combat? https://www.zhihu.com/question/275790138/answer/2721437682?utm_id=0 https://www.zhihu.com/question/275790138/answer/2721437682?u... 间隔/間隔 https://m.sohu.com/a/448392173_120754270/ https://m.sohu.com/a/448392173_120754270/ I should probably take this opp to ask if Hehner described explicitly how bunches are distinguished from sets.. boundaries? Ah you haven't been referring to the swordlike nature of the barycentre all along? (A rather fuzzy distribution in practice?)
- 082349872349872 2y ago
  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

Didn't 成瀬関次 in 戦ふ日本刀 gripe that distance management as traditionally taught didn't make sense in actual combat? https://www.zhihu.com/question/275790138/answer/2721437682?utm_id=0 https://www.zhihu.com/question/275790138/answer/2721437682?u... 间隔/間隔 https://m.sohu.com/a/448392173_120754270/ https://m.sohu.com/a/448392173_120754270/ I should probably take this opp to ask if Hehner described explicitly how bunches are distinguished from sets.. boundaries? Ah you haven't been referring to the swordlike nature of the barycentre all along? (A rather fuzzy distribution in practice?)

082349872349872 2y ago
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)