Logs: freenode/#haskell
| 2020-09-17 15:40:58 | <carter> | In hott land, the equality type is sortah like an open data family. Sortah? Dolio sclv am I wrong? |
| 2020-09-17 15:41:12 | <ski> | something like that |
| 2020-09-17 15:41:21 | <carter> | So you could conceivably annotate the extra proof terms with a priority weight |
| 2020-09-17 15:41:32 | <carter> | Or so something like a sibling to deriving via |
| 2020-09-17 15:41:39 | <dolio> | Kind of. It's complex. :) |
| 2020-09-17 15:41:40 | <carter> | With some preference ordering |
| 2020-09-17 15:42:10 | <carter> | In some ways it veers into wanting relational programming In your functional programming |
| 2020-09-17 15:42:18 | <ski> | you mean priorities for eq-via-permutation and eq-via-sorting, e.g. ? |
| 2020-09-17 15:42:37 | <carter> | Yeah |
| 2020-09-17 15:42:45 | <carter> | It’s still a fuzzy idea of mine |
| 2020-09-17 15:43:02 | × | arianvp quits (~weechat@arianvp.me) (Quit: WeeChat 2.7.1) |
| 2020-09-17 15:43:05 | <ski> | heh, i've recently been thinking about how to construct isomorphisms between types .. and that (in my mind) ties a bit into relational/logic programming |
| 2020-09-17 15:43:11 | <dolio> | The interesting thing about quotients in HoTT to me is that the equalities between equal quotient values are computationally relevant. |
| 2020-09-17 15:43:13 | → | gestone joins (~gestone@c-73-97-137-216.hsd1.wa.comcast.net) |
| 2020-09-17 15:43:35 | → | arianvp joins (~weechat@arianvp.me) |
| 2020-09-17 15:43:44 | <ski> | yes |
| 2020-09-17 15:43:47 | × | sid_cypher quits (~quassel@200116b80060a70031488a0eec1b5c23.dip.versatel-1u1.de) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2020-09-17 15:43:49 | <carter> | Ski I’ve been way overdue to write down some of my ideas in this space. |
| 2020-09-17 15:44:04 | → | sid_cypher joins (~quassel@200116b80060a70031488a0eec1b5c23.dip.versatel-1u1.de) |
| 2020-09-17 15:44:22 | × | DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Remote host closed the connection) |
| 2020-09-17 15:44:24 | <carter> | Plague time plus forcing myself to look into new jobs for a change of pace have eaten into bandwidth. Current job is great. But kinda want a change of pace |
| 2020-09-17 15:44:30 | → | lemmih_ joins (~lemmih@58.182.131.25) |
| 2020-09-17 15:44:34 | <dolio> | So you can possibly do 'different' things for 'equal' values, but those things are still able to be mediated between by some other computation. |
| 2020-09-17 15:44:40 | <ski> | (my "reflective syntax" idea, that i introduced for effectful computations, also seems to fit nicely, with some modifications, to equality proofs, and to computing with such HITs) |
| 2020-09-17 15:44:43 | → | kw joins (ac4a6125@cpe-172-74-97-37.nc.res.rr.com) |
| 2020-09-17 15:44:48 | → | DavidEichmann joins (~david@43.240.198.146.dyn.plus.net) |
| 2020-09-17 15:45:01 | <carter> | Ski how’d you get your logic programming thoughts |
| 2020-09-17 15:45:41 | → | spew joins (uid195861@gateway/web/irccloud.com/x-dhwinilivvllyihf) |
| 2020-09-17 15:46:18 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 272 seconds) |
| 2020-09-17 15:46:56 | × | lemmih quits (~lemmih@2406:3003:2072:44:251c:6ccc:226:e43d) (Ping timeout: 244 seconds) |
| 2020-09-17 15:47:02 | <ski> | well. if you e.g. express an isomorphism between `Nat' and `Fin n * Nat', you're expressing a bidirectional translation. that's like a binary predicate (except that you enforce it being functional, in both directions). so the "body" of your definition will effectively come after something corresponding to `:-' in Prolog |
| 2020-09-17 15:47:19 | → | proofofkeags joins (~proofofke@174-29-30-112.hlrn.qwest.net) |
| 2020-09-17 15:47:27 | <carter> | i'm not super literate at prolog |
| 2020-09-17 15:47:29 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:59f2:1ee3:fe3e:b848) |
| 2020-09-17 15:47:35 | <carter> | more strict relational plus datalog |
| 2020-09-17 15:48:03 | <ski> | `:-' is converse implication `<=', basically. or maybe converse entailment `-|', if you prefer |
| 2020-09-17 15:48:13 | <dolio> | Which in some ways makes it "easier" to write functions from quotients. You don't need to decide some canonical representative of each equivalence class and produce an identical result. You just need to show how to mediate between the results when someone presents you with how two values are 'equal'. |
| 2020-09-17 15:48:44 | <carter> | dolio: which referent? |
| 2020-09-17 15:49:29 | × | DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Remote host closed the connection) |
| 2020-09-17 15:50:23 | → | DavidEichmann joins (~david@43.240.198.146.dyn.plus.net) |
| 2020-09-17 15:50:24 | × | sid_cypher quits (~quassel@200116b80060a70031488a0eec1b5c23.dip.versatel-1u1.de) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2020-09-17 15:50:26 | <dolio> | Eh? |
| 2020-09-17 15:50:32 | → | fendor joins (~fendor@t204-126.demo.tuwien.ac.at) |
| 2020-09-17 15:50:43 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 2020-09-17 15:50:59 | <ski> | carter : i still have to consider more how computations with these isomorphism / type-equality definitions will actually work. but it seems to naturally want to express itself in logic programming terms, to me, when i'm following the way i'm trying to express things |
| 2020-09-17 15:51:00 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Client Quit) |
| 2020-09-17 15:52:00 | × | fendor__ quits (~fendor@e237-037.eduroam.tuwien.ac.at) (Ping timeout: 272 seconds) |
| 2020-09-17 15:52:42 | <carter> | dolio: couldn't figure you which thing you were referrring to ;) |
| 2020-09-17 15:52:47 | <carter> | ski: i can totally see that |
| 2020-09-17 15:52:50 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 256 seconds) |
| 2020-09-17 15:52:53 | <carter> | full linear logic seems relevant to me |
| 2020-09-17 15:53:01 | <carter> | cause its a really nice way to think about certain relations |
| 2020-09-17 15:53:09 | → | martin___ joins (uid411878@gateway/web/irccloud.com/x-mpsimrgxgomecjvf) |
| 2020-09-17 15:53:10 | <dolio> | I've just been rambling, so it's referring to stuff I've said, probably. |
| 2020-09-17 15:53:39 | → | machinedgod joins (~machinedg@45.78.189.122) |
| 2020-09-17 15:53:52 | <carter> | Fun rambles |
| 2020-09-17 15:54:15 | × | kw quits (ac4a6125@cpe-172-74-97-37.nc.res.rr.com) (Ping timeout: 245 seconds) |
| 2020-09-17 15:54:50 | <dolio> | It's kind of interesting, really. If you think about the details, it's tying up 'propositions as types' in a really satisfying way. |
| 2020-09-17 15:54:55 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:b0dc:6c54:247b:ece) (Remote host closed the connection) |
| 2020-09-17 15:55:00 | × | hololeap quits (~hololeap@unaffiliated/hololeap) (Quit: KVIrc 5.0.1 Aria http://www.kvirc.net/) |
| 2020-09-17 15:55:22 | <ski> | carter : .. including also sometimes wanting to be able to use disjunction (not just conjunction), in the body of a rule |
| 2020-09-17 15:55:32 | <carter> | which disjunction? |
| 2020-09-17 15:55:32 | <dolio> | Because, the 'propositions as types' approach was originally like "well, A + B is used for A ∨ B, and we don't care that the former might have more than one distinct value." |
| 2020-09-17 15:55:33 | <carter> | :) |
| 2020-09-17 15:55:52 | <carter> | ski have you skimmed mike shulmans linear logic for constructive math? |
| 2020-09-17 15:56:01 | <carter> | it kinda touches on this in a really cool way |
| 2020-09-17 15:56:02 | <ski> | hm, i think i did, at some point, yes |
| 2020-09-17 15:56:16 | <ski> | in what way are you seeing connections to linear logic ? |
| 2020-09-17 15:56:18 | <carter> | its a weird paper , but for a conceputal flavor for full linear lgoic |
| 2020-09-17 15:56:39 | <carter> | well, the duality structure for *full* linear logic is really good for functional programming / duality / logic programming |
| 2020-09-17 15:56:40 | <dolio> | And most attempts to fix that latter part kind of try to make it _not_ have more than one value. |
| 2020-09-17 15:56:40 | <carter> | idk |
| 2020-09-17 15:56:48 | <carter> | err |
| 2020-09-17 15:57:00 | <carter> | poke me about this in a few days, i need to mull how to explain this better |
| 2020-09-17 15:57:02 | → | wgolden joins (~wgolden@178.162.204.238) |
| 2020-09-17 15:57:11 | × | acidjnk_new3 quits (~acidjnk@p200300d0c736587164f46f145ae9b6a7.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2020-09-17 15:57:23 | ski | nods to dolio re functions from quotients |
| 2020-09-17 15:57:26 | <dolio> | But the HoTT approach is kind of the opposite. It has more than one value, but there are mediating values between them that make it sort of equivalent to having only one value. |
| 2020-09-17 15:57:51 | <ski> | (carter : at least if it's the slides i think it is. link ?) |
| 2020-09-17 15:58:01 | <dolio> | More than one value in a strict sense, but not 'up to paths'. |
| 2020-09-17 15:58:07 | → | pera joins (~pera@unaffiliated/pera) |
| 2020-09-17 15:58:14 | <carter> | https://arxiv.org/abs/1805.07518 ? |
| 2020-09-17 15:59:04 | <ski> | hm, i think i didn't see this paper (maybe i saw slides of a presentation of it, not sure) |
| 2020-09-17 15:59:07 | <ski> | ty |
| 2020-09-17 15:59:08 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-94-225.w86-212.abo.wanadoo.fr) |
| 2020-09-17 15:59:14 | × | inkbottle quits (~inkbottle@aaubervilliers-654-1-114-91.w86-198.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 2020-09-17 15:59:45 | → | ph88 joins (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) |
| 2020-09-17 16:00:05 | × | Maxdamantus quits (~Maxdamant@unaffiliated/maxdamantus) (Ping timeout: 240 seconds) |
| 2020-09-17 16:00:29 | → | Rudd0 joins (~Rudd0@185.189.115.103) |
| 2020-09-17 16:00:45 | × | ph88_ quits (~ph88@2a02:8109:9e40:2704:85f2:8dce:6e30:a554) (Ping timeout: 272 seconds) |
| 2020-09-17 16:00:52 | ← | brnzhg[m] parts (brnzhgmatr@gateway/shell/matrix.org/x-giqbkbtzwixrtmho) ("Kicked by @appservice-irc:matrix.org : Idle for 30+ days") |
| 2020-09-17 16:01:57 | × | Saukk quits (~Saukk@2001:998:dc:4a67:1c59:9bb5:b94c:4) (Remote host closed the connection) |
| 2020-09-17 16:02:03 | → | borne joins (~fritjof@200116b8641fc4005e981dab12496c3b.dip.versatel-1u1.de) |
| 2020-09-17 16:02:13 | → | Maxdamantus joins (~Maxdamant@unaffiliated/maxdamantus) |
| 2020-09-17 16:02:22 | <ski> | carter : "which disjunction?" -- well .. in this case, additive, i suppose you'd say |
| 2020-09-17 16:02:39 | <carter> | is that the usual one? |
| 2020-09-17 16:02:47 | <ski> | carter : but i've sometimes been pondering how one could program with multiplicative disjunction, as well |
| 2020-09-17 16:02:49 | <carter> | the thing is ... the other one is also really nice |
| 2020-09-17 16:02:52 | <ski> | the usual constructive one, yes |
| 2020-09-17 16:03:25 | <carter> | ski: i have a tiny model of all 4 in haskell code https://github.com/cartazio/symmetric-monoidal/blob/master/src/Control/Monoidal.hs |
All times are in UTC.