Logs: freenode/#haskell
| 2020-10-05 21:38:23 | <dolio> | (Still not really reasonable probably, but more reasonable.) |
| 2020-10-05 21:38:40 | <frdg> | is it possible to write `subset` with only a Foldable instance? https://dpaste.org/Vuo3 |
| 2020-10-05 21:39:25 | × | Buntspecht quits (~user@unaffiliated/siracusa) (Ping timeout: 240 seconds) |
| 2020-10-05 21:39:30 | × | wroathe_ quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 2020-10-05 21:39:45 | <ski> | frdg> :t member |
| 2020-10-05 21:39:59 | → | Buntspecht joins (~user@unaffiliated/siracusa) |
| 2020-10-05 21:40:13 | <frdg> | member :: (Foldable t, Eq a) => a -> t a -> Bool |
| 2020-10-05 21:40:31 | <monochrom> | @type \xs ys -> all (\x -> elem x ys) xs |
| 2020-10-05 21:40:33 | <lambdabot> | (Foldable t1, Foldable t2, Eq a) => t1 a -> t2 a -> Bool |
| 2020-10-05 21:40:37 | <ski> | try `flip member s2' instead of `member s2' |
| 2020-10-05 21:41:09 | <frdg> | ski: I was close :) |
| 2020-10-05 21:41:20 | <monochrom> | Also it means that the two sets don't have to have the same container type. |
| 2020-10-05 21:41:21 | <ski> | foldr ((&&) . (`member` s2)) True s1 -- would also be possible |
| 2020-10-05 21:42:32 | × | st8less quits (~st8less@inet-167-224-197-181.isp.ozarksgo.net) (Ping timeout: 244 seconds) |
| 2020-10-05 21:43:53 | <ski> | @let member x s = foldr ((||) . (== x)) False s |
| 2020-10-05 21:43:55 | <lambdabot> | Defined. |
| 2020-10-05 21:43:58 | <ski> | @type member |
| 2020-10-05 21:43:59 | <lambdabot> | (Foldable t, Eq a) => a -> t a -> Bool |
| 2020-10-05 21:44:12 | <ski> | @type \s0 s1 -> foldr ((&&) . (`member` s1)) True s0 |
| 2020-10-05 21:44:14 | <lambdabot> | (Foldable t1, Foldable t2, Eq a) => t1 a -> t2 a -> Bool |
| 2020-10-05 21:44:29 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2020-10-05 21:45:07 | × | NinjaTrappeur quits (~ninja@unaffiliated/ninjatrappeur) (Ping timeout: 240 seconds) |
| 2020-10-05 21:45:22 | <ski> | dolio : well, there's also "subfinite" and other such fuzzy things |
| 2020-10-05 21:45:29 | × | dcabrejas quits (bcd609cc@188.214.9.204) (Ping timeout: 245 seconds) |
| 2020-10-05 21:45:36 | ski | . o O ( Kripke semantics ) |
| 2020-10-05 21:45:41 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2020-10-05 21:45:45 | <monochrom> | What is subfinite? |
| 2020-10-05 21:45:51 | <ski> | a subset of a finite set |
| 2020-10-05 21:46:01 | <ski> | (which needn't be finite itself, constructively) |
| 2020-10-05 21:46:14 | <monochrom> | Yikes. |
| 2020-10-05 21:46:23 | <ski> | (that it, one can't prove it's not finite. but one can't always prove it's finite, either) |
| 2020-10-05 21:46:23 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2020-10-05 21:46:27 | → | NinjaTrappeur joins (~ninja@unaffiliated/ninjatrappeur) |
| 2020-10-05 21:46:46 | <monochrom> | Constructive math is too hard. :) |
| 2020-10-05 21:46:58 | <zoom84> | ski, here's what I came up with for your suggestion that MkPair a a would work. Compiles and runs. Lemme know if I missed anything: |
| 2020-10-05 21:47:17 | <zoom84> | data Pair a = MkSingle a | MkPair a a deriving(Show, Eq) |
| 2020-10-05 21:47:21 | <zoom84> | instance Functor (Pair) where |
| 2020-10-05 21:47:26 | <zoom84> | fmap :: (a -> b) -> Pair a -> Pair b |
| 2020-10-05 21:47:27 | <ski> | consider `{() | Goldbach}'. claiming this is finite amounts to having a bijection with a prefix of the natural numbers. which means that we could then decide Goldbach's conjecture from such a hypothetical proof of finiteness |
| 2020-10-05 21:47:31 | <zoom84> | fmap f (MkPair x y) = MkPair (f x) (f y) |
| 2020-10-05 21:47:35 | <zoom84> | fmap f (MkSingle x) = MkSingle (f x) |
| 2020-10-05 21:48:00 | <dolio> | ski: Subfinite is a notion from constructive mathematics, though. |
| 2020-10-05 21:48:05 | <ski> | zoom84 : that's fine. although in my version, i had no `MkSingle', just `MkPair' |
| 2020-10-05 21:48:09 | <ski> | dolio : yes |
| 2020-10-05 21:48:39 | <monochrom> | I still like the fact that constructive math/logic points out where I am using non-constructive choices. But I still insist on using those non-constructive choices. |
| 2020-10-05 21:48:48 | <ski> | one can model stages of knowledge about some mathematical object or structure, with Kripke semantics |
| 2020-10-05 21:48:50 | <dolio> | Also I mean, subfinite is a concept that arises once infinite things exist. |
| 2020-10-05 21:49:04 | <zoom84> | understood ski, thanks. i wanted to include a single var constructor as well because I wanted to see fmap work for both cases in a single type |
| 2020-10-05 21:49:14 | × | sep2 quits (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 2020-10-05 21:49:16 | <monochrom> | Also, I recognize that natural deduction for constructive logic is so nicely symmetric. |
| 2020-10-05 21:49:24 | <zoom84> | which can't be done for (a->b), at least with the standard functor |
| 2020-10-05 21:49:47 | <monochrom> | (However! Classical logic also also nicely symmetric in the lattice sense.) |
| 2020-10-05 21:50:11 | <ski> | so, we can have one stage ("possible world") in which neither `A' nor `not A' is known. and then have two alternative possible future stages, one in which `A' is known, and another in which `not A' is known. and the interpretation of `not Phi' is that it holds at a stage, if for no future stages (no accessible worlds) we have that `Phi' holds |
| 2020-10-05 21:50:11 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 2020-10-05 21:50:20 | <dolio> | Ah, but so is linear logic, which is properly constructive still. |
| 2020-10-05 21:50:27 | <ski> | so, at the initial stage, we can neither claim `A' nor `not A' |
| 2020-10-05 21:51:21 | <dolio> | There's kind of a sense in which linear logic takes constructiveness more seriously than intuitionism. |
| 2020-10-05 21:51:25 | <ski> | another thing one can model here is "discovering new elements of domains". we could know that `a' and `b' are elements (generators, say) of a presentation of a group. in a later stage, we may learn `c' is also a generator |
| 2020-10-05 21:51:47 | <ski> | and at different stages, we can also learn relations between "words" involving these generators |
| 2020-10-05 21:52:00 | <monochrom> | Ah, increasing stages of knowledge. I didn't think of that analogy when I learned this. |
| 2020-10-05 21:52:05 | <dolio> | Because the linear dual of something is like a positive disproof rather than 'assuming this leads to a contradiction.' |
| 2020-10-05 21:52:32 | <ski> | so, this is about being able to reason with partial knowledge, what holds for a group presentation where `a' and `b' are generators, but we haven't decided yet if there's to be any more ? (and possibly also not decided yet whether `a = b') |
| 2020-10-05 21:52:39 | <monochrom> | (A true formalist, I just learned and obeyed the rules of making a Kripke multiverse without asking why. :) ) |
| 2020-10-05 21:52:50 | <ski> | zoom84 : ah, ok |
| 2020-10-05 21:53:26 | <monochrom> | (I did have my intuition, but it's only based on "I tried many examples and they all work out, this looks solid". :) ) |
| 2020-10-05 21:53:30 | <ski> | dolio : "Also I mean, subfinite is a concept that arises once infinite things exist." -- yea, i suppose so |
| 2020-10-05 21:54:06 | <ski> | monochrom : "Also, I recognize that natural deduction for constructive logic is so nicely symmetric." -- but sequent calculus for classical logic is also very nicely symmetric (even a bit more so, i'd say) :) |
| 2020-10-05 21:54:16 | <monochrom> | Yeah! |
| 2020-10-05 21:54:38 | <monochrom> | But somehow I like the lattice story more than the sequent calculus story for classical logic. |
| 2020-10-05 21:54:44 | <ski> | monochrom : .. but the problem then is that cut-elimination (normalization of proofs, removing lemmata, going to canonical/direct proofs) is non-deterministic, for the classical case |
| 2020-10-05 21:55:00 | <monochrom> | Every powerset lattice is a boolean lattice \∩/ |
| 2020-10-05 21:55:14 | <ski> | (but then, classical linear logic somehow manages to be computational, not have such non-determinism ..) |
| 2020-10-05 21:55:38 | × | Franciman quits (~francesco@host-212-171-42-250.retail.telecomitalia.it) (Quit: Leaving) |
| 2020-10-05 21:55:38 | <ski> | (ah, dolio already mentioned linear logic :) |
| 2020-10-05 21:55:41 | × | fendor quits (~fendor@77.119.129.78.wireless.dyn.drei.com) (Remote host closed the connection) |
| 2020-10-05 21:56:10 | <dolio> | There's also some work on non-linear 'logic' that has this kind of duality. |
| 2020-10-05 21:56:37 | <dolio> | You get essentially all the same connectives, but they're distinct in a different way. |
| 2020-10-05 21:56:50 | <dolio> | And the difference is evaluation order. |
| 2020-10-05 21:57:13 | <ski> | monochrom : it's interesting that for finitely presented groups, we have the "word problem", that it's not decidable whether two presented elements are equal. this proposition is "affirmative", in the sense that if they are equal, then a search of the space will eventually find the proof using the relations/laws of the presentation |
| 2020-10-05 21:57:23 | → | GyroW_ joins (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) |
| 2020-10-05 21:57:23 | × | GyroW_ quits (~GyroW@ptr-48ujrfd1ztq5fjywfw3.18120a2.ip6.access.telenet.be) (Changing host) |
| 2020-10-05 21:57:23 | → | GyroW_ joins (~GyroW@unaffiliated/gyrow) |
| 2020-10-05 21:57:38 | × | GyroW quits (~GyroW@unaffiliated/gyrow) (Ping timeout: 260 seconds) |
| 2020-10-05 21:58:04 | <ski> | monochrom : otoh, for real numbers, defined in terms of Cauchy sequences, it's the other way around. if they're not equal (they're apart), we'll eventually learn so, by taking fine enough approximations. but if they're equal, then inspecting the approximations won't terminate |
| 2020-10-05 21:58:07 | <dolio> | So like, + is call-by-value, and \par is call-by-name. |
| 2020-10-05 21:59:21 | <ski> | dolio : i think Mike Shulman has been trying to make use of linear logic (or actually affine, iirc), to do interesting math, to more nicely explain things (like splitting of notions) in constructive math |
| 2020-10-05 21:59:40 | <dolio> | Yeah, that's one of the things I'm drawing from. |
| 2020-10-05 22:00:15 | <dolio> | I'm not sure it's even strictly affine in the paper. |
| 2020-10-05 22:00:25 | <ski> | (it may have been you who've mentioned some links to that here. i forgot whom) |
| 2020-10-05 22:00:46 | <ski> | (hm, last time, it may have been carter, i think ?) |
| 2020-10-05 22:00:57 | <carter> | eh? |
| 2020-10-05 22:01:14 | × | mirrorbird quits (~psutcliff@2a00:801:2d5:9d73:ff00:6553:d451:a276) (Quit: Leaving) |
| 2020-10-05 22:01:23 | <ski> | carter : you mentioned some paper by Mike Shulman, not too long ago, in here, yes ? |
| 2020-10-05 22:01:26 | <dolio> | Like, it suggests certain additional axioms that are based on the specific translation into intuitionistic logic. |
| 2020-10-05 22:01:27 | <carter> | yes |
| 2020-10-05 22:01:31 | → | polyrain joins (~polyrain@2001:8003:e501:6901:a41a:145a:3fce:c107) |
| 2020-10-05 22:01:43 | <carter> | but the linearity / affinity isn't the important part :) |
| 2020-10-05 22:01:47 | <dolio> | Like A×A -> !A. |
| 2020-10-05 22:02:04 | <dolio> | Once you have two, you have as many as you want. |
| 2020-10-05 22:02:31 | <int-e> | Oh I should really take advantage of the new-ish atomic readMVar in ivar-simple; that way an IVar would only have one MVar instead of two. |
All times are in UTC.