| 2024-02-11 00:10:05 +0100 | <Axman6> | 3/exit |
| 2024-02-11 00:10:15 +0100 | <Axman6> | oops... goodbye! |
| 2024-02-11 00:10:19 +0100 | Axman6 | (~Axman6@user/axman6) (Remote host closed the connection) |
| 2024-02-11 00:24:31 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) (Ping timeout: 268 seconds) |
| 2024-02-11 00:26:29 +0100 | Axman6 | (~Axman6@user/axman6) |
| 2024-02-11 00:27:48 +0100 | azr4e1 | (~azr4e1@137.220.68.193) (Remote host closed the connection) |
| 2024-02-11 00:33:30 +0100 | <energizer> | why does length (1,2) give 1? |
| 2024-02-11 00:34:55 +0100 | <c_wraith> | Types |
| 2024-02-11 00:35:02 +0100 | <c_wraith> | :t length |
| 2024-02-11 00:35:03 +0100 | <lambdabot> | Foldable t => t a -> Int |
| 2024-02-11 00:35:34 +0100 | <energizer> | so we have a Foldable and length returns an Int. so far so good |
| 2024-02-11 00:35:44 +0100 | <energizer> | why is that Int 1 |
| 2024-02-11 00:35:54 +0100 | <c_wraith> | If you match that `t a` against `(,) b c` you get (t ~ ((,) b) and (a ~ c) |
| 2024-02-11 00:36:15 +0100 | <c_wraith> | How many values of type c are there in a (b, c) value? |
| 2024-02-11 00:38:14 +0100 | <c_wraith> | err, (t ~ ((,) b)) if I count my closing parens properly |
| 2024-02-11 00:40:06 +0100 | <energizer> | oh that's pretty strange |
| 2024-02-11 00:40:13 +0100 | <c_wraith> | length in terms of foldable gives the same result as (length . toList) does |
| 2024-02-11 00:40:40 +0100 | <c_wraith> | > toList ("foo", False) |
| 2024-02-11 00:40:41 +0100 | <lambdabot> | [False] |
| 2024-02-11 00:41:08 +0100 | <energizer> | yeah that's just an unusual definition of , |
| 2024-02-11 00:41:59 +0100 | <c_wraith> | It's more or less what you have to end up with if you follow the types and keep things as simple as you can. |
| 2024-02-11 00:42:27 +0100 | harveypwca | (~harveypwc@2601:246:c201:d680:59a0:7761:1557:ead5) (Quit: Leaving) |
| 2024-02-11 00:45:39 +0100 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2024-02-11 00:46:23 +0100 | <energizer> | > foldr1 (+) (1,2) |
| 2024-02-11 00:46:24 +0100 | <lambdabot> | 2 |
| 2024-02-11 00:48:22 +0100 | <probie> | Is there a law for `Foldable` involving `length`? |
| 2024-02-11 00:48:45 +0100 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 272 seconds) |
| 2024-02-11 00:49:19 +0100 | acidjnk_new | (~acidjnk@p200300d6e737e7742d33f4d70f70ba9d.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2024-02-11 00:49:58 +0100 | <probie> | `foldl' (+) 0 (1,2)` is necessarily 1, but given that a `Foldable` can define its own length, what's stopping it from being 2? |
| 2024-02-11 00:50:22 +0100 | <yushyin> | "The length method must agree with a foldMap mapping each element to Sum 1" -- https://hackage.haskell.org/package/base-4.19.0.0/docs/Data-Foldable.html#laws |
| 2024-02-11 00:50:28 +0100 | <probie> | sadness |
| 2024-02-11 00:52:19 +0100 | <dsal> | > foldr1 (+) ('a', 1) |
| 2024-02-11 00:52:21 +0100 | <lambdabot> | 1 |
| 2024-02-11 00:53:03 +0100 | <dsal> | There's not much else that could do other than refuse to compile which would be kind. |
| 2024-02-11 00:53:07 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-02-11 00:55:42 +0100 | <[Leary]> | Apart from one optional law relating to Functor, the Foldable laws seem to just be coherence conditions ensuring that the secondary methods have the expected semantics relative to `foldMap`; the actual core of Foldable is virtually unconstrained. It would be completely lawful to write `instance Foldable ((,) a) where foldMap f (_, x) = f x <> f x` and obtain `length (1, 2) = 2`. |
| 2024-02-11 00:55:47 +0100 | ell15 | (~ellie@user/ellie) (Quit: Leaving) |
| 2024-02-11 00:56:53 +0100 | <c_wraith> | Yes, but then that instance would not be consistent with a lawful Traversable instance |
| 2024-02-11 00:56:59 +0100 | <c_wraith> | which does in fact have more laws |
| 2024-02-11 00:57:20 +0100 | <c_wraith> | and it's sort of expected that if you have a Traversable instance, your Foldable instance is consistent with it |
| 2024-02-11 00:58:19 +0100 | <monochrom> | Javascript insists that sum ("1", 1) = 2 >:) |
| 2024-02-11 00:58:27 +0100 | <ncf> | c_wraith: oh i guess that's true |
| 2024-02-11 00:59:58 +0100 | <c_wraith> | I'm really not sure Traversable should have a Foldable requirement. There are a lot of cases where I want traverse or sequenceA where I think the consistent Foldable instance is sort of silly |
| 2024-02-11 01:00:22 +0100 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 276 seconds) |
| 2024-02-11 01:00:52 +0100 | <energizer> | (a,b) having length but (a,b,c) not having it makes me think (a,b) isnt quite the 2-tuple, it's really a separate Pair type |
| 2024-02-11 01:01:17 +0100 | <ncf> | Foldable is just the "getter" half of Traversable |
| 2024-02-11 01:01:34 +0100 | <ski> | a pair is a `2'-tuple |
| 2024-02-11 01:01:49 +0100 | gooba | (~gooba@90-231-13-185-no3430.tbcn.telia.com) (Remote host closed the connection) |
| 2024-02-11 01:02:26 +0100 | <energizer> | why would a 2 tuple have length but a 3 tuple not. no i think (a,b) is Pair |
| 2024-02-11 01:02:58 +0100 | gooba | (~gooba@90-231-13-185-no3430.tbcn.telia.com) |
| 2024-02-11 01:03:50 +0100 | <energizer> | which is more like a single element k-v map |
| 2024-02-11 01:04:08 +0100 | <monochrom> | Um is this the "Pair vs APair" debate again? >:) |
| 2024-02-11 01:04:09 +0100 | <ski> | it's just that further instances are not present |
| 2024-02-11 01:04:25 +0100 | <yushyin> | because no one bothered to implement the Foldable instance |
| 2024-02-11 01:05:17 +0100 | <ncf> | you could have instances for n-tuples applied to n - 1 type parameters, and they would all have length constantly 1 |
| 2024-02-11 01:08:37 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 2024-02-11 01:09:58 +0100 | <ski> | % length $(return (TupE [Just (LitE (IntegerL 42))])) |
| 2024-02-11 01:09:58 +0100 | <yahb2> | 1 |
| 2024-02-11 01:10:36 +0100 | <ncf> | uh |
| 2024-02-11 01:10:40 +0100 | <ncf> | is that Solo? |
| 2024-02-11 01:10:43 +0100 | <ski> | yes |
| 2024-02-11 01:10:54 +0100 | <ski> | % :t $(return (TupE [Just (LitE (IntegerL 42))])) |
| 2024-02-11 01:10:54 +0100 | <yahb2> | $(return (TupE [Just (LitE (IntegerL 42))])) :: Num a => Solo a |
| 2024-02-11 01:11:02 +0100 | <geekosaur> | "it's really a separate Pair type" --- that's how tuples work in Haskell |
| 2024-02-11 01:11:09 +0100 | <geekosaur> | they are not funny-looking lists |
| 2024-02-11 01:11:13 +0100 | yoo | (~yo0O0o@user/mobivme) (Ping timeout: 264 seconds) |
| 2024-02-11 01:12:12 +0100 | <geekosaur> | they are anonymous product types |
| 2024-02-11 01:12:25 +0100 | <geekosaur> | (or "record types" if you prefer) |
| 2024-02-11 01:13:19 +0100 | <monochrom> | I think there are people out there who insist "product types" because they make a big fuss about "record types" having field names. :) |
| 2024-02-11 01:13:32 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 255 seconds) |
| 2024-02-11 01:13:53 +0100 | <monochrom> | I was very surprised but they totally said "they are different!" |
| 2024-02-11 01:14:02 +0100 | rvalue | (~rvalue@user/rvalue) |
| 2024-02-11 01:15:23 +0100 | <ski> | record types are labelled product types. tuple types are positional product types |
| 2024-02-11 01:15:36 +0100 | <energizer> | `length (Person "alice" 25 "main")` doesnt work tho |
| 2024-02-11 01:15:59 +0100 | <monochrom> | OK I guess there is a natural way to give a subtyping system to record types and we don't do it to tuple types. |
| 2024-02-11 01:16:03 +0100 | <ski> | because there's no `Foldable' instance, for that type |
| 2024-02-11 01:16:09 +0100 | <geekosaur> | it could if you provided a Foldable instance for it; most people don't |
| 2024-02-11 01:17:01 +0100 | <ncf> | that doesn't look functorial |
| 2024-02-11 01:17:04 +0100 | <ski> | tuple types, in SML, are merely record types, whose field names/labels are all positive integers up to the number of components |
| 2024-02-11 01:18:29 +0100 | <monochrom> | You can always map (x,y,z) to ((x,y),z) and then you can enjoy Foldable methods. |
| 2024-02-11 01:21:03 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 01:21:52 +0100 | waleee | (~waleee@176.10.144.38) (Ping timeout: 268 seconds) |
| 2024-02-11 01:23:48 +0100 | EvanR | (~EvanR@user/evanr) |
| 2024-02-11 01:33:20 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 255 seconds) |
| 2024-02-11 01:34:25 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-02-11 01:40:30 +0100 | <EvanR> | > print(x) |
| 2024-02-11 01:40:31 +0100 | <lambdabot> | <IO ()> |
| 2024-02-11 01:53:36 +0100 | bilegeek | (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13) |
| 2024-02-11 01:57:01 +0100 | Square | (~Square@user/square) (Ping timeout: 268 seconds) |
| 2024-02-11 02:01:11 +0100 | <monochrom> | You're pretty late for print(x). :) |
| 2024-02-11 02:13:35 +0100 | <EvanR> | figured |
| 2024-02-11 02:15:08 +0100 | mjs2600 | (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) |
| 2024-02-11 02:15:13 +0100 | mjs2600_ | (~mjs2600@c-174-169-225-239.hsd1.vt.comcast.net) (Read error: Connection reset by peer) |
| 2024-02-11 02:15:46 +0100 | tessier | (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) (Ping timeout: 276 seconds) |
| 2024-02-11 02:17:01 +0100 | tessier | (~treed@ip72-220-57-194.sd.sd.cox.net) |
| 2024-02-11 02:22:02 +0100 | tessier | (~treed@ip72-220-57-194.sd.sd.cox.net) (Ping timeout: 252 seconds) |
| 2024-02-11 02:23:15 +0100 | tessier | (~treed@ec2-184-72-149-67.compute-1.amazonaws.com) |
| 2024-02-11 02:25:00 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2024-02-11 02:46:19 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2024-02-11 02:46:25 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-02-11 02:47:17 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds) |
| 2024-02-11 02:47:47 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2024-02-11 02:53:53 +0100 | falafel | (~falafel@141.156.241.57) |
| 2024-02-11 02:54:36 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2024-02-11 02:58:01 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 264 seconds) |
| 2024-02-11 03:07:01 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-02-11 03:12:38 +0100 | mulk | (~mulk@pd9514242.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-02-11 03:13:47 +0100 | mulk | (~mulk@p5b112899.dip0.t-ipconnect.de) |
| 2024-02-11 03:18:49 +0100 | otto_s | (~user@p5b04400d.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2024-02-11 03:20:00 +0100 | otto_s | (~user@p4ff27640.dip0.t-ipconnect.de) |
| 2024-02-11 03:22:35 +0100 | motherfsck | (~motherfsc@user/motherfsck) |
| 2024-02-11 03:38:07 +0100 | Feuermagier | (~Feuermagi@user/feuermagier) |
| 2024-02-11 03:47:38 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-02-11 03:50:16 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 2024-02-11 04:05:03 +0100 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2024-02-11 04:05:31 +0100 | op_4 | (~tslil@user/op-4/x-9116473) |
| 2024-02-11 04:08:32 +0100 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.8.2+deb4+b2 - https://znc.in) |
| 2024-02-11 04:11:21 +0100 | mhatta | (~mhatta@www21123ui.sakura.ne.jp) |
| 2024-02-11 04:16:11 +0100 | falafel | (~falafel@141.156.241.57) (Ping timeout: 264 seconds) |
| 2024-02-11 04:33:29 +0100 | td_ | (~td@i53870917.versanet.de) (Ping timeout: 252 seconds) |
| 2024-02-11 04:35:17 +0100 | td_ | (~td@i5387093C.versanet.de) |
| 2024-02-11 04:45:18 +0100 | bilegeek | (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13) (Quit: Leaving) |
| 2024-02-11 04:49:29 +0100 | jargon | (~jargon@157.sub-174-205-162.myvzw.com) (Remote host closed the connection) |
| 2024-02-11 04:54:20 +0100 | falafel | (~falafel@141.156.241.57) |
| 2024-02-11 05:08:49 +0100 | falafel | (~falafel@141.156.241.57) (Ping timeout: 264 seconds) |
| 2024-02-11 05:21:35 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-02-11 05:39:52 +0100 | Guest30 | (~Guest57@2405:201:12:3dae:f726:6f38:f016:3459) |
| 2024-02-11 05:40:07 +0100 | <Guest30> | @free fmap :: (a -> b) -> f a -> f b |
| 2024-02-11 05:40:07 +0100 | <lambdabot> | Extra stuff at end of line |
| 2024-02-11 05:40:55 +0100 | <Guest30> | @free fmap :: (a -> b) -> F a -> F b |
| 2024-02-11 05:40:55 +0100 | <lambdabot> | g . h = k . f => $map_F g . fmap h = fmap k . $map_F f |
| 2024-02-11 05:41:24 +0100 | <Guest30> | @free pure :: a -> F a |
| 2024-02-11 05:41:24 +0100 | <lambdabot> | $map_F f . pure = pure . f |
| 2024-02-11 05:42:00 +0100 | <Guest30> | @free bind :: F a -> (a -> F b) -> F b |
| 2024-02-11 05:42:00 +0100 | <lambdabot> | $map_F g . h = k . f => $map_F g (bind x h) = bind ($map_F f x) k |
| 2024-02-11 05:47:39 +0100 | aforemny_ | (~aforemny@i59F516F6.versanet.de) |
| 2024-02-11 05:47:43 +0100 | aforemny | (~aforemny@2001:9e8:6cfa:c300:ed38:1b4d:cf6e:9f22) (Ping timeout: 260 seconds) |
| 2024-02-11 06:01:54 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 06:01:57 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Client Quit) |
| 2024-02-11 06:02:07 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 06:03:08 +0100 | mulk | (~mulk@p5b112899.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2024-02-11 06:05:10 +0100 | mulk | (~mulk@p5b2dcdd6.dip0.t-ipconnect.de) |
| 2024-02-11 06:05:54 +0100 | bilegeek | (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13) |
| 2024-02-11 06:10:01 +0100 | JordiGH | (~jordi@user/jordigh) (Ping timeout: 264 seconds) |
| 2024-02-11 06:12:04 +0100 | qqq | (~qqq@92.43.167.61) |
| 2024-02-11 06:12:12 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2024-02-11 06:16:37 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Ping timeout: 264 seconds) |
| 2024-02-11 06:18:35 +0100 | fansly | (~fansly@103.3.221.176) |
| 2024-02-11 06:20:22 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-02-11 06:35:54 +0100 | Guest30 | (~Guest57@2405:201:12:3dae:f726:6f38:f016:3459) (Quit: Client closed) |
| 2024-02-11 06:38:36 +0100 | fansly | (~fansly@103.3.221.176) (Read error: Connection reset by peer) |
| 2024-02-11 06:39:56 +0100 | fansly | (~fansly@182.2.141.93) |
| 2024-02-11 06:43:00 +0100 | fansly | (~fansly@182.2.141.93) (Read error: Connection reset by peer) |
| 2024-02-11 06:43:18 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 06:58:43 +0100 | Guest67 | (~Guest57@49.36.11.6) |
| 2024-02-11 06:59:06 +0100 | <Guest67> | @free filter :: (a -> Boolean) -> F a -> F a |
| 2024-02-11 06:59:06 +0100 | <lambdabot> | $map_F f . filter (g . f) = filter g . $map_F f |
| 2024-02-11 07:01:16 +0100 | <Guest67> | @free safeExtract :: a -> F a -> a |
| 2024-02-11 07:01:16 +0100 | <lambdabot> | f . safeExtract x = safeExtract (f x) . $map_F f |
| 2024-02-11 07:02:02 +0100 | <Guest67> | @free unsafeExtract :: f a -> a |
| 2024-02-11 07:02:02 +0100 | <lambdabot> | Extra stuff at end of line |
| 2024-02-11 07:02:09 +0100 | <Guest67> | @free unsafeExtract :: F a -> a |
| 2024-02-11 07:02:10 +0100 | <lambdabot> | f . unsafeExtract = unsafeExtract . $map_F f |
| 2024-02-11 07:03:07 +0100 | <Guest67> | @free toEither :: e -> F a -> G e a |
| 2024-02-11 07:03:08 +0100 | <lambdabot> | Plugin `free' failed with: Sorry, this type is too difficult for me. |
| 2024-02-11 07:03:08 +0100 | <lambdabot> | CallStack (from HasCallStack): |
| 2024-02-11 07:03:08 +0100 | <lambdabot> | error, called at src/Lambdabot/Plugin/Haskell/Free/FreeTheorem.hs:296:31 in lambdabot-haskell-plugins-5.3-KdjsqvMFsLeLZemJqobWap:Lambdabot.Plugin.Haskell.Free.FreeTheorem |
| 2024-02-11 07:03:40 +0100 | <Guest67> | @free toEither :: b -> F a -> F b a |
| 2024-02-11 07:03:41 +0100 | <lambdabot> | Plugin `free' failed with: Sorry, this type is too difficult for me. |
| 2024-02-11 07:03:41 +0100 | <lambdabot> | CallStack (from HasCallStack): |
| 2024-02-11 07:03:41 +0100 | <lambdabot> | error, called at src/Lambdabot/Plugin/Haskell/Free/FreeTheorem.hs:296:31 in lambdabot-haskell-plugins-5.3-KdjsqvMFsLeLZemJqobWap:Lambdabot.Plugin.Haskell.Free.FreeTheorem |
| 2024-02-11 07:03:56 +0100 | <Guest67> | @free toEither :: b -> F a -> G b a |
| 2024-02-11 07:03:56 +0100 | <lambdabot> | Plugin `free' failed with: Sorry, this type is too difficult for me. |
| 2024-02-11 07:03:57 +0100 | <lambdabot> | CallStack (from HasCallStack): |
| 2024-02-11 07:03:57 +0100 | <lambdabot> | error, called at src/Lambdabot/Plugin/Haskell/Free/FreeTheorem.hs:296:31 in lambdabot-haskell-plugins-5.3-KdjsqvMFsLeLZemJqobWap:Lambdabot.Plugin.Haskell.Free.FreeTheorem |
| 2024-02-11 07:04:17 +0100 | Guest67 | (~Guest57@49.36.11.6) () |
| 2024-02-11 07:04:37 +0100 | mulk | (~mulk@p5b2dcdd6.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-02-11 07:08:51 +0100 | johnw | (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 2024-02-11 07:16:40 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Quit: Quit) |
| 2024-02-11 07:20:51 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 07:23:18 +0100 | bzm3r | (~bzm3r@d205-250-253-229.bchsia.telus.net) |
| 2024-02-11 07:37:15 +0100 | mulk | (~mulk@pd95144c1.dip0.t-ipconnect.de) |
| 2024-02-11 07:41:01 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 07:41:57 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Remote host closed the connection) |
| 2024-02-11 07:42:22 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 07:44:52 +0100 | RaspbellySwirl | (~Raspbelly@host-213-235-142-6.ip.topnet.cz) |
| 2024-02-11 07:45:22 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 07:50:45 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Read error: Connection reset by peer) |
| 2024-02-11 07:50:55 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 07:52:59 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Remote host closed the connection) |
| 2024-02-11 07:55:26 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2024-02-11 08:02:56 +0100 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 2024-02-11 08:08:31 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) |
| 2024-02-11 08:11:49 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Remote host closed the connection) |
| 2024-02-11 08:12:07 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-02-11 08:12:18 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2024-02-11 08:12:30 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:12:40 +0100 | euleritian | (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) |
| 2024-02-11 08:13:00 +0100 | euleritian | (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:13:18 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 08:19:46 +0100 | johnw | (~johnw@69.62.242.138) |
| 2024-02-11 08:20:00 +0100 | johnw | (~johnw@69.62.242.138) (Remote host closed the connection) |
| 2024-02-11 08:21:40 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:22:35 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 08:24:36 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:25:06 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 08:30:18 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 2024-02-11 08:32:25 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:33:00 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 08:36:59 +0100 | qqq | (~qqq@92.43.167.61) (Remote host closed the connection) |
| 2024-02-11 08:39:25 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 2024-02-11 08:40:25 +0100 | johnw | (~johnw@69.62.242.138) |
| 2024-02-11 08:44:24 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:44:53 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 08:44:58 +0100 | gcdsefhu^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-02-11 08:45:39 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 256 seconds) |
| 2024-02-11 08:49:51 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-02-11 08:50:21 +0100 | trev | (~trev@user/trev) (Ping timeout: 260 seconds) |
| 2024-02-11 08:52:07 +0100 | trev | (~trev@109-252-43-67.nat.spd-mgts.ru) |
| 2024-02-11 08:55:08 +0100 | trev | (~trev@109-252-43-67.nat.spd-mgts.ru) (Client Quit) |
| 2024-02-11 08:56:03 +0100 | trev | (~trev@109-252-43-67.nat.spd-mgts.ru) |
| 2024-02-11 08:56:29 +0100 | trev | (~trev@109-252-43-67.nat.spd-mgts.ru) (Changing host) |
| 2024-02-11 08:56:29 +0100 | trev | (~trev@user/trev) |
| 2024-02-11 08:57:26 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:58:08 +0100 | euleritian | (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) |
| 2024-02-11 08:58:30 +0100 | euleritian | (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 08:58:55 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 09:00:07 +0100 | tt1231 | (~tt123@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat) |
| 2024-02-11 09:00:11 +0100 | Natch | (~natch@92.34.7.158) (Remote host closed the connection) |
| 2024-02-11 09:00:14 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-02-11 09:00:37 +0100 | trev | (~trev@user/trev) (Client Quit) |
| 2024-02-11 09:00:52 +0100 | trev | (~trev@user/trev) |
| 2024-02-11 09:02:08 +0100 | tt1231 | (~tt123@2603-6010-8700-4a81-219f-50d3-618a-a6ee.res6.spectrum.com) |
| 2024-02-11 09:02:41 +0100 | bilegeek | (~bilegeek@2600:1008:b04e:c81e:502b:3dae:f3e9:cb13) (Quit: Leaving) |
| 2024-02-11 09:03:27 +0100 | gcdsefhu^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 2024-02-11 09:05:29 +0100 | Natch | (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
| 2024-02-11 09:06:38 +0100 | acidjnk_new | (~acidjnk@p200300d6e737e77464baf57332386b26.dip0.t-ipconnect.de) |
| 2024-02-11 09:35:49 +0100 | fansly | (~fansly@2001:448a:2010:476e:fcb4:b4a9:3c44:892e) (Ping timeout: 264 seconds) |
| 2024-02-11 09:38:16 +0100 | fansly | (~fansly@103.3.221.176) |
| 2024-02-11 09:38:49 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2024-02-11 09:39:19 +0100 | euleritian | (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) |
| 2024-02-11 09:41:03 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 2024-02-11 09:41:46 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-02-11 09:52:04 +0100 | euleritian | (~euleritia@dynamic-176-007-008-211.176.7.pool.telefonica.de) (Ping timeout: 276 seconds) |
| 2024-02-11 09:52:57 +0100 | euleritian | (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) |
| 2024-02-11 09:55:48 +0100 | eb20 | (~eb@41.189.245.59) |
| 2024-02-11 09:57:50 +0100 | rscastilho2024 | (~rscastilh@189.61.140.215) |
| 2024-02-11 09:58:34 +0100 | fansly | (~fansly@103.3.221.176) (Ping timeout: 276 seconds) |
| 2024-02-11 09:59:28 +0100 | rscastilho2024 | (~rscastilh@189.61.140.215) (Remote host closed the connection) |
| 2024-02-11 09:59:47 +0100 | <eb20> | anyone her use hugs? |
| 2024-02-11 10:00:28 +0100 | fansly | (~fansly@182.2.165.191) |
| 2024-02-11 10:10:01 +0100 | <kaol> | Yes. Recently, unlikely. I last did anything with it when ghc 6 was new. |
| 2024-02-11 10:10:29 +0100 | euleritian | (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 10:10:46 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 10:16:46 +0100 | elkcl | (~elkcl@broadband-95-84-226-240.ip.moscow.rt.ru) (Ping timeout: 276 seconds) |
| 2024-02-11 10:16:49 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2024-02-11 10:20:50 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-02-11 10:25:13 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2024-02-11 10:27:56 +0100 | fansly | (~fansly@182.2.165.191) (Read error: Connection reset by peer) |
| 2024-02-11 10:29:57 +0100 | euleritian | (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) |
| 2024-02-11 10:31:26 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-02-11 10:31:48 +0100 | Tuplanolla | (~Tuplanoll@91-159-68-95.elisa-laajakaista.fi) |
| 2024-02-11 10:32:41 +0100 | euleritian | (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 10:32:59 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 10:33:32 +0100 | <mauke> | there was someone on matrix who still uses it |
| 2024-02-11 10:33:49 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-02-11 10:35:32 +0100 | gmg | (~user@user/gehmehgeh) |
| 2024-02-11 10:37:16 +0100 | bzm3r | (~bzm3r@d205-250-253-229.bchsia.telus.net) (Ping timeout: 250 seconds) |
| 2024-02-11 10:42:31 +0100 | todi | (~todi@p4fd1aef3.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in) |
| 2024-02-11 10:52:29 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2024-02-11 10:52:34 +0100 | todi | (~todi@p4fd1aef3.dip0.t-ipconnect.de) |
| 2024-02-11 10:52:54 +0100 | euleritian | (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) |
| 2024-02-11 10:54:12 +0100 | megaTherion | (~therion@unix.io) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-02-11 10:55:15 +0100 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-02-11 11:01:02 +0100 | megaTherion | (~therion@unix.io) |
| 2024-02-11 11:01:47 +0100 | euleritian | (~euleritia@dynamic-176-000-156-161.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 11:02:05 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 11:02:53 +0100 | acidjnk_new | (~acidjnk@p200300d6e737e77464baf57332386b26.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2024-02-11 11:06:06 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-02-11 11:09:56 +0100 | alexherbo2 | (~alexherbo@33.134.22.93.rev.sfr.net) |
| 2024-02-11 11:15:55 +0100 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2024-02-11 11:18:04 +0100 | megaTherion | (~therion@unix.io) (Remote host closed the connection) |
| 2024-02-11 11:21:22 +0100 | megaTherion | (~therion@unix.io) |
| 2024-02-11 11:23:45 +0100 | michalz | (~michalz@185.246.207.205) |
| 2024-02-11 11:36:49 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) |
| 2024-02-11 11:36:58 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-02-11 11:40:08 +0100 | alexherbo2 | (~alexherbo@33.134.22.93.rev.sfr.net) (Remote host closed the connection) |
| 2024-02-11 11:40:29 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3340-93db-fd9e-1a08-c9e1-df21.rev.sfr.net) |
| 2024-02-11 11:58:57 +0100 | Lycurgus | (~georg@user/Lycurgus) |
| 2024-02-11 12:18:39 +0100 | sroso | (~sroso@user/SrOso) |
| 2024-02-11 12:20:59 +0100 | infinity0 | (~infinity0@pwned.gg) |
| 2024-02-11 12:24:34 +0100 | infinity0_ | (~infinity0@pwned.gg) |
| 2024-02-11 12:24:35 +0100 | infinity0 | Guest7389 |
| 2024-02-11 12:24:35 +0100 | infinity0_ | infinity0 |
| 2024-02-11 12:25:37 +0100 | Guest7389 | (~infinity0@pwned.gg) (Ping timeout: 264 seconds) |
| 2024-02-11 12:27:20 +0100 | Axman6 | (~Axman6@user/axman6) (Remote host closed the connection) |
| 2024-02-11 12:33:12 +0100 | mmhat | (~mmh@p200300f1c740af4dee086bfffe095315.dip0.t-ipconnect.de) |
| 2024-02-11 12:38:06 +0100 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-02-11 12:39:12 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-02-11 12:51:43 +0100 | yotta | (~cha0s@14.191.144.106) |
| 2024-02-11 12:53:01 +0100 | mmhat | (~mmh@p200300f1c740af4dee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 4.2.1) |
| 2024-02-11 12:56:23 +0100 | Square | (~Square@user/square) |
| 2024-02-11 12:58:13 +0100 | <yotta> | When passing multiple MutableByteArray# to a C function, it is correct to use Array# MutableByteArray# or MutableArray# MutableByteArray# ? The C function writes to the bytearrays. |
| 2024-02-11 13:01:25 +0100 | mrmr155334 | (~mrmr@user/mrmr) (Quit: Bye, See ya later!) |
| 2024-02-11 13:01:59 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2024-02-11 13:03:13 +0100 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2024-02-11 13:04:57 +0100 | <int-e> | yotta: oh https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/ffi.html actually has an example of this (look for sum_first)... you need to poke into RTS internals |
| 2024-02-11 13:05:36 +0100 | mrmr155334 | (~mrmr@user/mrmr) |
| 2024-02-11 13:05:44 +0100 | qqq | (~qqq@92.43.167.61) |
| 2024-02-11 13:08:34 +0100 | <int-e> | (For mutation, use Array# MutableByteArray#) |
| 2024-02-11 13:10:29 +0100 | <yotta> | thank |
| 2024-02-11 13:31:59 +0100 | Lycurgus | (~georg@user/Lycurgus) (Quit: leaving) |
| 2024-02-11 13:35:01 +0100 | yoo | (~yo0O0o@130.105.162.162) |
| 2024-02-11 13:46:59 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-02-11 13:47:20 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 13:58:26 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-02-11 14:03:54 +0100 | Axman6 | (~Axman6@user/axman6) |
| 2024-02-11 14:05:31 +0100 | fbytez_ | (~uid@user/fbytez) |
| 2024-02-11 14:08:00 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 14:08:41 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 14:10:36 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-02-11 14:11:49 +0100 | EvanR | (~EvanR@user/evanr) (Read error: Connection reset by peer) |
| 2024-02-11 14:11:59 +0100 | EvanR | (~EvanR@user/evanr) |
| 2024-02-11 14:12:44 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 14:14:20 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-02-11 14:22:10 +0100 | eb20 | (~eb@41.189.245.59) (Ping timeout: 250 seconds) |
| 2024-02-11 14:25:36 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-02-11 14:33:05 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3340-93db-fd9e-1a08-c9e1-df21.rev.sfr.net) (Remote host closed the connection) |
| 2024-02-11 14:48:04 +0100 | __monty__ | (~toonn@user/toonn) |
| 2024-02-11 14:48:49 +0100 | average | (uid473595@user/average) (Quit: Connection closed for inactivity) |
| 2024-02-11 14:54:41 +0100 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2024-02-11 14:54:56 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-cfe3-0966-2558-23d8-f964.rev.sfr.net) |
| 2024-02-11 14:58:20 +0100 | [_] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 268 seconds) |
| 2024-02-11 15:04:00 +0100 | <haskellbridge> | <Jade> I'm often seeing an idiom along the line of `length [ () | pat <- some_list ]` where the pattern match would be identical to an `==`. Would it not make sense to have something like `count :: Eq a => a -> [a] -> Int` for these? |
| 2024-02-11 15:04:08 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-02-11 15:04:09 +0100 | <haskellbridge> | <Jade> in base specifically* |
| 2024-02-11 15:05:05 +0100 | <haskellbridge> | <Jade> It could even be `count :: (a -> Bool) -> [a] -> Int` |
| 2024-02-11 15:05:32 +0100 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-02-11 15:06:14 +0100 | elkcl | (~elkcl@broadband-95-84-226-240.ip.moscow.rt.ru) |
| 2024-02-11 15:06:27 +0100 | <Axman6> | the pattern match is likely to be more efficient, and that's not quite the same thing - the code you pasted counts how many items match a geven pattern, not what's equal to another value |
| 2024-02-11 15:07:04 +0100 | <haskellbridge> | <Jade> yeah I saw a lot of those with strings and the "pattern" being a character literal |
| 2024-02-11 15:07:44 +0100 | <haskellbridge> | <Jade> and it always takes a second or so to click, but with a `count 'x' list` that would be a lot easier |
| 2024-02-11 15:07:46 +0100 | <ski> | > replicateM 2 (Const (Sum 7)) |
| 2024-02-11 15:07:48 +0100 | <lambdabot> | Const (Sum {getSum = 14}) |
| 2024-02-11 15:07:53 +0100 | <haskellbridge> | <Jade> s/list/string |
| 2024-02-11 15:08:09 +0100 | <ski> | > replicateM 2 (Const (Product 7)) |
| 2024-02-11 15:08:11 +0100 | <lambdabot> | Const (Product {getProduct = 49}) |
| 2024-02-11 15:08:11 +0100 | <ski> | i guess |
| 2024-02-11 15:09:18 +0100 | <haskellbridge> | <Jade> wait why is that happening |
| 2024-02-11 15:09:31 +0100 | <haskellbridge> | <Jade> Oh I see |
| 2024-02-11 15:09:53 +0100 | <int-e> | https://wiki.haskell.org/Fairbairn_threshold is a factor here |
| 2024-02-11 15:10:45 +0100 | <haskellbridge> | <Jade> The Monad instances of these newtype wrappers for Monoids are the same as the identity monad |
| 2024-02-11 15:12:05 +0100 | <ncf> | Applicative, not Monad (Const k isn't a monad unless k is ()) |
| 2024-02-11 15:12:14 +0100 | <ncf> | :t replicateM |
| 2024-02-11 15:12:15 +0100 | <lambdabot> | Applicative m => Int -> m a -> m [a] |
| 2024-02-11 15:13:15 +0100 | driib | (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
| 2024-02-11 15:14:04 +0100 | <ncf> | (and no, this isn't the identity applicative) |
| 2024-02-11 15:14:44 +0100 | JordiGH | (~jordi@user/jordigh) |
| 2024-02-11 15:15:19 +0100 | <ski> | "No instance for (MonadFail (Const (Product Integer)))" :( |
| 2024-02-11 15:17:01 +0100 | <ncf> | can't MonadFail if it Fails to Monad |
| 2024-02-11 15:20:15 +0100 | Midjak | (~MarciZ@82.66.147.146) (Read error: Connection reset by peer) |
| 2024-02-11 15:20:42 +0100 | MarciZ | (~MarciZ@82.66.147.146) |
| 2024-02-11 15:21:42 +0100 | <ski> | exactly |
| 2024-02-11 15:26:37 +0100 | <haskellbridge> | <irregularsphere> ski: ...how exactly is it going to implement `String -> Product Integer` anyway |
| 2024-02-11 15:27:20 +0100 | <haskellbridge> | <irregularsphere> sorry, `fail :: forall a. String -> Const (Product Integer) a` |
| 2024-02-11 15:31:30 +0100 | <haskellbridge> | <irregularsphere> my best guess is to put a `Maybe` somewhere but I'm not sure |
| 2024-02-11 15:32:39 +0100 | <haskellbridge> | <irregularsphere> maybe `Compose Maybe (Const (Product Integer))`? |
| 2024-02-11 15:32:51 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-02-11 15:35:38 +0100 | driib | (~driib@vmi931078.contaboserver.net) |
| 2024-02-11 15:38:05 +0100 | <haskellbridge> | <irregularsphere> nvm about the compose thing |
| 2024-02-11 15:40:27 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-02-11 15:42:04 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-02-11 15:42:23 +0100 | euleritian | (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 2024-02-11 15:43:02 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-02-11 15:43:50 +0100 | acidjnk_new | (~acidjnk@p5dd87f44.dip0.t-ipconnect.de) |
| 2024-02-11 15:45:14 +0100 | <ncf> | fail _ = Const mempty ? |
| 2024-02-11 15:45:18 +0100 | <ncf> | Fail isn't the problem, it's Monad |
| 2024-02-11 15:48:14 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 15:48:42 +0100 | MarciZ | (~MarciZ@82.66.147.146) (Read error: Connection reset by peer) |
| 2024-02-11 15:50:59 +0100 | <haskellbridge> | <irregularsphere> Ah. |
| 2024-02-11 15:57:02 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 2024-02-11 15:57:14 +0100 | JordiGH | (~jordi@user/jordigh) (Ping timeout: 268 seconds) |
| 2024-02-11 16:01:01 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 264 seconds) |
| 2024-02-11 16:01:29 +0100 | euleritian | (~euleritia@dynamic-176-006-191-101.176.6.pool.telefonica.de) |
| 2024-02-11 16:01:47 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 264 seconds) |
| 2024-02-11 16:03:33 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2024-02-11 16:13:34 +0100 | euleritian | (~euleritia@dynamic-176-006-191-101.176.6.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 2024-02-11 16:14:10 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-02-11 16:18:49 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 276 seconds) |
| 2024-02-11 16:19:25 +0100 | Midjak | (~MarciZ@82.66.147.146) (Read error: Connection reset by peer) |
| 2024-02-11 16:19:37 +0100 | euleritian | (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de) |
| 2024-02-11 16:19:55 +0100 | euleritian | (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 16:20:12 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-02-11 16:20:29 +0100 | JordiGH | (~jordi@user/jordigh) |
| 2024-02-11 16:21:04 +0100 | <haskellbridge> | <irregularsphere> If `Monad (Const (Product Integer))` were to ever happen, then `join`'s only expected behaviour is `id`, thus `xs >>= f = xs >>= (\x -> id (f x)) = xs >>= (\x -> return (f x) >>= id) = xs >>= (\x -> (return . f) x >>= id) = (xs >>= return . f) >>= id = (fmap f xs) >>= id = join (fmap f xs) = fmap f xs = xs` |
| 2024-02-11 16:21:09 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 16:23:18 +0100 | <ncf> | what? |
| 2024-02-11 16:23:19 +0100 | <haskellbridge> | <irregularsphere> (join's expected behaviour is id because join has type `Const (Product Integer) (Const (Product Integer) a) -> Const (Product Integer) a`, which is saying `\(Const x) -> ...`, in which it is most reasonable to be `\(Const x) -> Const x = id` |
| 2024-02-11 16:23:41 +0100 | <haskellbridge> | <irregularsphere> ncf: I fear that `xs >>= f = xs` for all `xs` and `f`. |
| 2024-02-11 16:24:08 +0100 | <haskellbridge> | <irregularsphere> ok gn |
| 2024-02-11 16:24:14 +0100 | <ncf> | "most reasonable" isn't a proof |
| 2024-02-11 16:25:01 +0100 | <haskellbridge> | <irregularsphere> fair |
| 2024-02-11 16:25:08 +0100 | <ncf> | you have to show that whatever you pick for join (which is a function m → m where m is a monoid), the laws can't be satisfied |
| 2024-02-11 16:26:00 +0100 | <ncf> | there are as many functions forall m. Monoid m => m → m as there are natural numbers, can you see why? |
| 2024-02-11 16:26:05 +0100 | <haskellbridge> | <irregularsphere> actually you can reverse define `xs >>= f = join (fmap f xs)` which all laws will automatically be satisfied |
| 2024-02-11 16:26:16 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2024-02-11 16:26:30 +0100 | <haskellbridge> | <irregularsphere> but `fmap f xs = xs` by definition |
| 2024-02-11 16:26:38 +0100 | <haskellbridge> | <irregularsphere> so `xs >>= f = join xs` |
| 2024-02-11 16:27:14 +0100 | <ncf> | yes, it's usually easier to reason about join than >>= |
| 2024-02-11 16:27:25 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-02-11 16:27:32 +0100 | <haskellbridge> | <irregularsphere> what i'm trying to point out is that |
| 2024-02-11 16:27:37 +0100 | <haskellbridge> | <irregularsphere> `f` is discarded |
| 2024-02-11 16:28:15 +0100 | <ncf> | sure |
| 2024-02-11 16:28:41 +0100 | <haskellbridge> | <irregularsphere> so with all definitions of `join`, `>>=` is already useless |
| 2024-02-11 16:29:20 +0100 | <haskellbridge> | <irregularsphere> yeah in my super long explanation you can omit last step |
| 2024-02-11 16:29:29 +0100 | <haskellbridge> | <irregularsphere> and apply `fmap f xs = xs` |
| 2024-02-11 16:29:40 +0100 | <ski> | irregularsphere : the point was to use refutable patterns, not `MonadFail' per se |
| 2024-02-11 16:30:06 +0100 | <haskellbridge> | <irregularsphere> (most of the blob of text is me proving `xs >>= f = join (fmap f xs)`) |
| 2024-02-11 16:30:10 +0100 | euleritian | (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 2024-02-11 16:30:20 +0100 | euleritian | (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de) |
| 2024-02-11 16:30:25 +0100 | <ncf> | that's the definition of >>= |
| 2024-02-11 16:30:40 +0100 | euleritian | (~euleritia@dynamic-046-114-170-060.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 16:30:41 +0100 | <haskellbridge> | <irregularsphere> ski: oh, huh |
| 2024-02-11 16:30:57 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 16:33:10 +0100 | <haskellbridge> | <irregularsphere> ncf: unfortunately it isn't like that in haskell source :( would like to push a pr though, but it's currently half past ten at night for me |
| 2024-02-11 16:33:20 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 255 seconds) |
| 2024-02-11 16:33:24 +0100 | <haskellbridge> | <irregularsphere> gn everyone! |
| 2024-02-11 16:33:51 +0100 | <ncf> | ok if you take >>= as primitive and define join as _>>= id then you do have to prove that, but it should just be an application of naturality |
| 2024-02-11 16:34:15 +0100 | <ncf> | in particular there's no reason to involve return |
| 2024-02-11 16:34:25 +0100 | rscastilho2024 | (~rscastilh@189.61.140.215) |
| 2024-02-11 16:34:45 +0100 | <haskellbridge> | <irregularsphere> `return` was simply part of my proof that `xs >>= f = join (fmap f xs)` |
| 2024-02-11 16:36:04 +0100 | <ncf> | i'm saying you don't need to mention return to prove that |
| 2024-02-11 16:36:12 +0100 | Midjak | (~MarciZ@82.66.147.146) (Read error: Connection reset by peer) |
| 2024-02-11 16:36:45 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 16:36:46 +0100 | <haskellbridge> | <irregularsphere> different proofs same conclusion hehe |
| 2024-02-11 16:39:05 +0100 | <haskellbridge> | <irregularsphere> yea what i'm trying to detail is that no matter how hard you try while adhering to laws you'd always do `xs >>= f` = `xs >>= id` in some way or another |
| 2024-02-11 16:40:17 +0100 | pastly | (~pastly@gateway/tor-sasl/pastly) |
| 2024-02-11 16:40:31 +0100 | <haskellbridge> | <irregularsphere> (the case for trying to define `Monad (Const a)` by the way) |
| 2024-02-11 16:41:27 +0100 | <ski> | i've before pondered having operations like `forall a b. m a -> (a -> n b) -> n b'. e.g. `m = State sr',`n = Reader sr', or `m = []',`n = Count' (`Const (Product Integer))' above) |
| 2024-02-11 16:41:52 +0100 | <haskellbridge> | <irregularsphere> *meanwhile me saying "gn" 11 minutes ago |
| 2024-02-11 16:42:29 +0100 | <ski> | btw, your `id' has type `(forall a. Const c a) -> (forall a. Const c a)' |
| 2024-02-11 16:42:41 +0100 | <haskellbridge> | <irregularsphere> yup |
| 2024-02-11 16:42:47 +0100 | <haskellbridge> | <irregularsphere> what's wrong about that |
| 2024-02-11 16:42:51 +0100 | Midjak | (~MarciZ@82.66.147.146) (Read error: Connection reset by peer) |
| 2024-02-11 16:42:53 +0100 | <ski> | @src (>>=) Either |
| 2024-02-11 16:42:53 +0100 | <lambdabot> | Source not found. This mission is too important for me to allow you to jeopardize it. |
| 2024-02-11 16:43:05 +0100 | <ski> | @src Either (>>=) |
| 2024-02-11 16:43:05 +0100 | <lambdabot> | Left l >>= _ = Left l |
| 2024-02-11 16:43:05 +0100 | <lambdabot> | Right r >>= k = k r |
| 2024-02-11 16:43:08 +0100 | <ncf> | ski: isn't that just a left n-module? |
| 2024-02-11 16:43:27 +0100 | <ncf> | i.e. mn ~> n |
| 2024-02-11 16:43:27 +0100 | <haskellbridge> | <irregularsphere> (wait lambdabot can _do_ that?) |
| 2024-02-11 16:43:31 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 16:43:42 +0100 | <ski> | ncf : i was thinking about something like actions, or perhaps retract situations, yea |
| 2024-02-11 16:44:18 +0100 | <ski> | (i also had `forall a. n a -> m a', and some laws relating the operations) |
| 2024-02-11 16:44:20 +0100 | <geekosaur> | irregularsphere, it has a small database of sources which is sometimes inaccurate for ghc (it's mostly cribbed from the haskell 2010 report) |
| 2024-02-11 16:44:28 +0100 | <ski> | irregularsphere : do what ? |
| 2024-02-11 16:44:35 +0100 | <geekosaur> | it doesn't know how to search for actual source code, sadly |
| 2024-02-11 16:44:39 +0100 | <haskellbridge> | <irregularsphere> the @src command |
| 2024-02-11 16:44:46 +0100 | <ski> | anyway, imagine if it was defined like |
| 2024-02-11 16:45:07 +0100 | <ski> | Right a >>= k = k a |
| 2024-02-11 16:45:16 +0100 | <ski> | m >>= _ = m |
| 2024-02-11 16:45:49 +0100 | <ski> | and now imagine if this `m' had type `forall b. Either a b' (due to `m' not matching `Right a') |
| 2024-02-11 16:47:32 +0100 | <ski> | or, if you prefer |
| 2024-02-11 16:47:41 +0100 | <ski> | m@(Left _) >>= _ = m |
| 2024-02-11 16:47:49 +0100 | jmdaemon | (~jmdaemon@user/jmdaemon) (Ping timeout: 264 seconds) |
| 2024-02-11 16:49:31 +0100 | son0p | (~ff@186.121.50.114) |
| 2024-02-11 16:50:50 +0100 | <ski> | irregularsphere : oh, and types are not inferred for higher-rank operations |
| 2024-02-11 16:51:03 +0100 | <ski> | (iow, that `id' won't be inferred) |
| 2024-02-11 17:09:10 +0100 | target_i | (~target_i@217.175.14.39) |
| 2024-02-11 17:12:54 +0100 | fendor | (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 2024-02-11 17:15:20 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-02-11 17:21:32 +0100 | Pixi` | (~Pixi@user/pixi) |
| 2024-02-11 17:24:35 +0100 | Pixi | (~Pixi@user/pixi) (Ping timeout: 252 seconds) |
| 2024-02-11 17:31:05 +0100 | coot | (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 2024-02-11 17:33:26 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-02-11 17:33:32 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-02-11 17:34:58 +0100 | jargon | (~jargon@157.sub-174-205-162.myvzw.com) |
| 2024-02-11 17:46:15 +0100 | AlexZenon | (~alzenon@94.233.241.194) (Ping timeout: 256 seconds) |
| 2024-02-11 17:51:23 +0100 | AlexZenon | (~alzenon@94.233.241.194) |
| 2024-02-11 18:06:04 +0100 | AstraGravityGirl | (~astra@181.42.52.150) |
| 2024-02-11 18:08:16 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-cfe3-0966-2558-23d8-f964.rev.sfr.net) (Remote host closed the connection) |
| 2024-02-11 18:11:07 +0100 | alexherbo2 | (~alexherbo@143.132.22.93.rev.sfr.net) |
| 2024-02-11 18:11:28 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 2024-02-11 18:11:56 +0100 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2024-02-11 18:15:37 +0100 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-02-11 18:15:48 +0100 | alexherbo2 | (~alexherbo@143.132.22.93.rev.sfr.net) (Remote host closed the connection) |
| 2024-02-11 18:15:53 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-02-11 18:17:16 +0100 | myxos | (~myxos@065-028-251-121.inf.spectrum.com) (Remote host closed the connection) |
| 2024-02-11 18:28:11 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 256 seconds) |
| 2024-02-11 18:28:26 +0100 | euleritian | (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) |
| 2024-02-11 18:28:55 +0100 | yotta | (~cha0s@14.191.144.106) (Quit: WeeChat 4.2.1) |
| 2024-02-11 18:29:49 +0100 | <noumenon> | what's a "rank"? |
| 2024-02-11 18:31:41 +0100 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds) |
| 2024-02-11 18:33:40 +0100 | <monochrom> | https://wiki.haskell.org/Rank-N_types may help |
| 2024-02-11 18:36:02 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2024-02-11 18:36:15 +0100 | myxos | (~myxos@065-028-251-121.inf.spectrum.com) |
| 2024-02-11 18:39:13 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 276 seconds) |
| 2024-02-11 18:40:11 +0100 | AstraGravityGirl | (~astra@181.42.52.150) (Ping timeout: 264 seconds) |
| 2024-02-11 18:40:27 +0100 | euleritian | (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 18:40:34 +0100 | yoo | (~yo0O0o@130.105.162.162) (Changing host) |
| 2024-02-11 18:40:34 +0100 | yoo | (~yo0O0o@user/mobivme) |
| 2024-02-11 18:40:38 +0100 | <ncf> | rank(a -> b) = 1 + rank a; rank _ = 0 |
| 2024-02-11 18:40:44 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 18:40:58 +0100 | <ncf> | er no |
| 2024-02-11 18:46:20 +0100 | AstraGravityGirl | (~AstraGrav@181.42.52.150) |
| 2024-02-11 18:46:23 +0100 | <ncf> | i guess it's slightly tricky to define by induction on types. two mutually recursive functions should do it |
| 2024-02-11 18:46:30 +0100 | <APic> | Indeed. |
| 2024-02-11 18:46:56 +0100 | Midjak | (~MarciZ@82.66.147.146) (Read error: Connection reset by peer) |
| 2024-02-11 18:47:30 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 18:47:56 +0100 | rvalue | (~rvalue@user/rvalue) |
| 2024-02-11 18:51:55 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 255 seconds) |
| 2024-02-11 18:52:35 +0100 | euleritian | (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) |
| 2024-02-11 18:55:26 +0100 | euleritian | (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 18:55:43 +0100 | euleritian | (~euleritia@77.22.252.56) |
| 2024-02-11 19:01:01 +0100 | AstraGravityGirl | (~AstraGrav@181.42.52.150) (Quit: AstraGravityGirl) |
| 2024-02-11 19:05:47 +0100 | tzh | (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 2024-02-11 19:07:13 +0100 | Midjak | (~MarciZ@82.66.147.146) (Ping timeout: 255 seconds) |
| 2024-02-11 19:13:35 +0100 | AstraGravityGirl | (~AstraGrav@181.42.52.150) |
| 2024-02-11 19:15:04 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-02-11 19:15:47 +0100 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 256 seconds) |
| 2024-02-11 19:15:47 +0100 | AstraGravityGirl | (~AstraGrav@181.42.52.150) (Client Quit) |
| 2024-02-11 19:18:32 +0100 | euleritian | (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) |
| 2024-02-11 19:25:40 +0100 | <ski> | noumenon : briefly, it's when a function take a polymorphic operation as *argument*, or when a function takes such a function as argument, &c. |
| 2024-02-11 19:26:07 +0100 | <ski> | so `(forall a. ..a..) -> ...' or `((forall a. ..a..) -> ...) -> ...' or .. |
| 2024-02-11 19:27:41 +0100 | <ski> | (some people say "higher-rank polymorphism", but i don't think the first of those examples is like polymorphism at all (more like existentials, cf. `... -> (exists a. ..a..)'. the next one is "kinda like polymorphism", though, so we alternate between "kinda existential" and "kinda universal") |
| 2024-02-11 19:30:10 +0100 | <ski> | (oh, and "higher-rank" means rank greater than one. rank one is plain polymorphism, values of type `forall a. ..a..'. sometimes people call (ordinary, without `forall' and `exists') monomorphic operations, "rank zero") |
| 2024-02-11 19:31:39 +0100 | <ski> | (and that issue with "non-ranked" operations is what ncf ran into above) |
| 2024-02-11 19:43:54 +0100 | coot | (~coot@89.69.206.216) |
| 2024-02-11 19:47:02 +0100 | pyooque | (~puke@user/puke) |
| 2024-02-11 19:47:02 +0100 | puke | Guest9035 |
| 2024-02-11 19:47:02 +0100 | Guest9035 | (~puke@user/puke) (Killed (tungsten.libera.chat (Nickname regained by services))) |
| 2024-02-11 19:47:02 +0100 | pyooque | puke |
| 2024-02-11 19:47:30 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-cfe3-f821-77e5-e4a1-a519.rev.sfr.net) |
| 2024-02-11 19:47:39 +0100 | <noumenon> | ski: so, can you rank ranks? |
| 2024-02-11 19:53:05 +0100 | euleritian | (~euleritia@dynamic-176-005-134-152.176.5.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 19:53:22 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 19:56:34 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 2024-02-11 19:57:11 +0100 | Midjak | (~MarciZ@82.66.147.146) |
| 2024-02-11 19:57:59 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-02-11 19:59:42 +0100 | euleritian | (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) |
| 2024-02-11 20:00:09 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 272 seconds) |
| 2024-02-11 20:02:26 +0100 | Guest33 | (~Guest33@2804:7f7:ddab:a8cd:9c91:258e:279f:d997) |
| 2024-02-11 20:03:59 +0100 | Guest33 | (~Guest33@2804:7f7:ddab:a8cd:9c91:258e:279f:d997) (Client Quit) |
| 2024-02-11 20:06:49 +0100 | coot | (~coot@89.69.206.216) (Quit: coot) |
| 2024-02-11 20:07:56 +0100 | ursa-major | (~ursa-majo@c-174-63-24-92.hsd1.co.comcast.net) |
| 2024-02-11 20:08:11 +0100 | rvalue | (~rvalue@user/rvalue) |
| 2024-02-11 20:10:44 +0100 | euleritian | (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 20:11:02 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 20:12:34 +0100 | <ski> | noumenon : how do you mean ? |
| 2024-02-11 20:14:38 +0100 | <noumenon> | ski: oh, nvm, I was confusing it with "kind" |
| 2024-02-11 20:15:37 +0100 | <noumenon> | something about forming a fractal hierarchy |
| 2024-02-11 20:16:36 +0100 | <noumenon> | having sorts of kinds, and so on |
| 2024-02-11 20:17:04 +0100 | <noumenon> | species of sorts |
| 2024-02-11 20:17:09 +0100 | <noumenon> | varieties of species |
| 2024-02-11 20:17:33 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-02-11 20:17:39 +0100 | <noumenon> | I wonder if you can abstract even that fractal nesting somehow |
| 2024-02-11 20:19:23 +0100 | <EvanR> | you run out of jargon so fast, might as well call the type universes by number |
| 2024-02-11 20:19:39 +0100 | <EvanR> | Type 1 : Type 2 : Type 3, etc |
| 2024-02-11 20:20:52 +0100 | euleritian | (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) |
| 2024-02-11 20:21:03 +0100 | <noumenon> | sounds more reasonable |
| 2024-02-11 20:21:06 +0100 | <ncf> | it's called agda |
| 2024-02-11 20:24:55 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3341-cfe3-f821-77e5-e4a1-a519.rev.sfr.net) (Remote host closed the connection) |
| 2024-02-11 20:30:34 +0100 | rscastilho2024 | (~rscastilh@189.61.140.215) (Remote host closed the connection) |
| 2024-02-11 20:31:02 +0100 | euleritian | (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 20:31:24 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 20:35:10 +0100 | rscastilho2024 | (~rscastilh@189.61.140.215) |
| 2024-02-11 20:37:52 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-02-11 20:39:37 +0100 | ld | (~ld@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 20:39:45 +0100 | ld | (~ld@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection) |
| 2024-02-11 20:40:16 +0100 | <noumenon> | lol |
| 2024-02-11 20:40:18 +0100 | <noumenon> | https://iohk.io/en/research/library/papers/reasonable-agda-is-correct-haskell-writing-verified-has… |
| 2024-02-11 20:40:20 +0100 | euleritian | (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) |
| 2024-02-11 20:40:25 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 20:40:28 +0100 | <noumenon> | and just when I thought Haskell was the biggest shark in the water |
| 2024-02-11 20:40:52 +0100 | <Rembane> | noumenon: There are always bigger sharks. :) |
| 2024-02-11 20:41:13 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection) |
| 2024-02-11 20:41:56 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 20:41:59 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection) |
| 2024-02-11 20:42:31 +0100 | <ncf> | haskell is nothing |
| 2024-02-11 20:42:38 +0100 | <ncf> | -- bob harper, probably |
| 2024-02-11 20:42:42 +0100 | <noumenon> | Rembane: there has to be some ultimate language, one which perfectly abstracts anything; the biggest shark |
| 2024-02-11 20:43:12 +0100 | <Rembane> | noumenon: Maybe. Lambda calculus perhaps? |
| 2024-02-11 20:43:34 +0100 | Guest92 | (~Guest92@97-120-50-87.ptld.qwest.net) |
| 2024-02-11 20:43:37 +0100 | <noumenon> | maybe that's what we should be programming with |
| 2024-02-11 20:44:33 +0100 | <ncf> | it's called agda (bis) |
| 2024-02-11 20:44:50 +0100 | <ncf> | cubical agda, even |
| 2024-02-11 20:45:14 +0100 | euleritian | (~euleritia@dynamic-046-114-170-184.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-02-11 20:45:16 +0100 | <probie> | Is cubical agda the hott extension to agda? |
| 2024-02-11 20:45:32 +0100 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-02-11 20:45:45 +0100 | <noumenon> | >open import Cubical.Core.Everything |
| 2024-02-11 20:45:55 +0100 | <noumenon> | well, that does sound like something you'd write before coding the universe |
| 2024-02-11 20:45:59 +0100 | <ncf> | the *computational* hott extension to agda |
| 2024-02-11 20:47:24 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 20:47:38 +0100 | <geekosaur> | noumenon: abstracts how? there are multiple kinds of abstraction |
| 2024-02-11 20:47:39 +0100 | <ncf> | (you don't need any extensions to do hott; in fact you need to *remove* an axiom (--without-K). but if you want your proofs to actually compute, then you need a metric shitton of complicated stuff) |
| 2024-02-11 20:48:39 +0100 | <geekosaur> | LC is one form of abstraction. the Ωmega language abstracts in a different way. etc. |
| 2024-02-11 20:50:22 +0100 | <noumenon> | geekosaur: something that abstracts abstraction itself, the ultimate abstraction, the Megalodon of languages |
| 2024-02-11 20:50:51 +0100 | <noumenon> | hopefully with intuitive syntax |
| 2024-02-11 20:51:02 +0100 | <geekosaur> | didn't Gödel have something to say about that? |
| 2024-02-11 20:51:34 +0100 | <noumenon> | until Gödel proves his theorems with Agda I don't believe them |
| 2024-02-11 20:53:22 +0100 | pmk | (6afe4476a1@2a03:6000:1812:100::26d) |
| 2024-02-11 20:58:33 +0100 | Guest92 | (~Guest92@97-120-50-87.ptld.qwest.net) (Quit: Client closed) |
| 2024-02-11 21:02:52 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection) |
| 2024-02-11 21:04:29 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2024-02-11 21:08:20 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 21:08:35 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection) |
| 2024-02-11 21:09:07 +0100 | finsternis | (~X@23.226.237.192) |
| 2024-02-11 21:09:09 +0100 | bzm3r | (~bzm3r@d205-250-253-229.bchsia.telus.net) |
| 2024-02-11 21:09:12 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 21:09:26 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Remote host closed the connection) |
| 2024-02-11 21:10:06 +0100 | rscastilho2024 | (~rscastilh@189.61.140.215) (Remote host closed the connection) |
| 2024-02-11 21:16:07 +0100 | Achylles | (~Achylles_@45.182.57.125) |
| 2024-02-11 21:20:21 +0100 | <EvanR> | noumenon, haskell is the gateway drug of advanced programming languages |
| 2024-02-11 21:20:44 +0100 | <EvanR> | you may never heard of what's out there until you do haskell and then people tell you that's nothing |
| 2024-02-11 21:22:02 +0100 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-02-11 21:23:15 +0100 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-02-11 21:41:11 +0100 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) (Read error: Connection reset by peer) |
| 2024-02-11 21:48:45 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-02-11 21:52:06 +0100 | ricardo_1 | (~ricardo@shabang.toppoint.de) (Read error: Connection reset by peer) |
| 2024-02-11 21:54:55 +0100 | michalz | (~michalz@185.246.207.205) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-02-11 21:55:17 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) |
| 2024-02-11 21:55:31 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-02-11 21:56:45 +0100 | hamster | (~ham@user/ham) |
| 2024-02-11 21:58:23 +0100 | Achylles | (~Achylles_@45.182.57.125) (Quit: Leaving) |
| 2024-02-11 21:58:49 +0100 | Achylles | (~Achylles_@45.182.57.125) |
| 2024-02-11 21:59:03 +0100 | Achylles | (~Achylles_@45.182.57.125) (Max SendQ exceeded) |
| 2024-02-11 21:59:13 +0100 | ham2 | (~ham@user/ham) (Ping timeout: 264 seconds) |
| 2024-02-11 22:01:16 +0100 | <TMA> | well, Gödel theorems are just the tip of the iceberg. if you happen to have a "nice" theory of first order logic [nice ~ consistent, complete] the axioms are not recursively enumerable |
| 2024-02-11 22:03:03 +0100 | <TMA> | there cannot be the biggest shark |
| 2024-02-11 22:05:23 +0100 | raoul | (~raoul@95.179.203.88) (Quit: Ping timeout (120 seconds)) |
| 2024-02-11 22:05:42 +0100 | raoul | (~raoul@95.179.203.88) |
| 2024-02-11 22:07:26 +0100 | target_i | (~target_i@217.175.14.39) (Quit: leaving) |
| 2024-02-11 22:08:13 +0100 | <haskellbridge> | <Liamzee> hi noumenon, I'm phenomenon, how are you doing? :) |
| 2024-02-11 22:11:22 +0100 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 256 seconds) |
| 2024-02-11 22:11:57 +0100 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2024-02-11 22:14:19 +0100 | RaspbellySwirl | (~Raspbelly@host-213-235-142-6.ip.topnet.cz) (Ping timeout: 246 seconds) |
| 2024-02-11 22:16:33 +0100 | ursa-major | (~ursa-majo@c-174-63-24-92.hsd1.co.comcast.net) (Quit: WeeChat 4.2.1) |
| 2024-02-11 22:17:11 +0100 | hololeap | (~quassel@user/hololeap) (Quit: Bye) |
| 2024-02-11 22:18:17 +0100 | hololeap | (~quassel@user/hololeap) |
| 2024-02-11 22:24:05 +0100 | ski | idly ponders time cubical agda |
| 2024-02-11 22:25:07 +0100 | <ski> | noumenon left, about half an hour ago |
| 2024-02-11 22:26:13 +0100 | <EvanR> | is that what dr gene ray used. Time is cubic: top bottom and two sides |
| 2024-02-11 22:28:20 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 2024-02-11 22:33:51 +0100 | ski | . o O ( "The 4-equidistant time points can be considered as Time Square imprinted upon the circle of Earth. In a single rotation of the Earth sphere, each Time corner point rotates through the other 3-corner Time points, thus creating 16 corners, 96 hours and 4-simultaneous 24-hour Days within a single rotation of Earth – equated to a Higher Order of Life Time Cube." ) |
| 2024-02-11 22:34:08 +0100 | <ski> | clearly this is talking about suspensions and stuff |
| 2024-02-11 22:34:30 +0100 | <EvanR> | you're somehow right |
| 2024-02-11 22:34:40 +0100 | azr4e1 | (~azr4e1@2a01:4b00:8438:1700:eee4:f118:781d:97a0) (Ping timeout: 255 seconds) |
| 2024-02-11 22:39:12 +0100 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 2024-02-11 22:39:32 +0100 | <ncf> | suspensions of disbelief |
| 2024-02-11 22:43:35 +0100 | peterbecich | (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-02-11 22:56:11 +0100 | <ncf> | ski: surely "time cubical agda" would implement guarded cubical type theory (https://agda.readthedocs.io/en/latest/language/guarded.html) |
| 2024-02-11 23:00:03 +0100 | <ski> | hm, that's modal stuff, yes ? |
| 2024-02-11 23:00:38 +0100 | ski | 's reminded of Nanevski's "Contextual Modal Type Theory" |
| 2024-02-11 23:01:45 +0100 | <ncf> | there's a "later" modality, clock quantification... |
| 2024-02-11 23:02:25 +0100 | <ski> | .. i wonder how (if) this relates to MetaML/MetaOCaml stuff |
| 2024-02-11 23:02:47 +0100 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 2024-02-11 23:03:43 +0100 | <ski> | "Application t u for t : (@tick x : A) → B is restricted so that t is typable in the prefix of the context that does not include any @tick variables in u." -- what's the type of `u', here ? |
| 2024-02-11 23:05:17 +0100 | <ncf> | A |
| 2024-02-11 23:07:55 +0100 | todi | (~todi@p4fd1aef3.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in) |
| 2024-02-11 23:07:59 +0100 | dostoyevsky2 | (~sck@user/dostoyevsky2) (Quit: leaving) |
| 2024-02-11 23:08:18 +0100 | <haskellbridge> | <irregularsphere> EvanR: i felt stupid searching up "gateway drug" |
| 2024-02-11 23:08:22 +0100 | dostoyevsky2 | (~sck@user/dostoyevsky2) |
| 2024-02-11 23:09:34 +0100 | <geekosaur> | gotta be careful with those English idioms… |
| 2024-02-11 23:09:55 +0100 | <EvanR> | I just check urban dictionary to see if it would help. It does not |
| 2024-02-11 23:10:06 +0100 | puke | (~puke@user/puke) (Quit: puke) |
| 2024-02-11 23:13:28 +0100 | <haskellbridge> | <irregularsphere> noumenon: wdym agda is a "bigger shark" than haskell |
| 2024-02-11 23:13:44 +0100 | <haskellbridge> | <irregularsphere> it just looks like haskell but the compiler proves it |
| 2024-02-11 23:13:51 +0100 | <haskellbridge> | <irregularsphere> either way agda2hs seems nice |
| 2024-02-11 23:14:50 +0100 | <geekosaur> | noumenon left some time ago |
| 2024-02-11 23:16:01 +0100 | <geekosaur> | (the bridge doesn't relay joins/parts and I Have no intention of enabling that) |
| 2024-02-11 23:17:24 +0100 | <EvanR> | you do join part reporting just fine |
| 2024-02-11 23:17:30 +0100 | <EvanR> | thanks |
| 2024-02-11 23:18:47 +0100 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2024-02-11 23:19:56 +0100 | <haskellbridge> | <irregularsphere> wait is haskell intrinsically not always type correct |
| 2024-02-11 23:20:00 +0100 | <haskellbridge> | <irregularsphere> i hate to see it |
| 2024-02-11 23:20:17 +0100 | dostoyevsky2 | (~sck@user/dostoyevsky2) (Quit: leaving) |
| 2024-02-11 23:20:27 +0100 | <geekosaur> | it's type correct, but there are programs that are well typed that haskell's typechecker cannot so prove |
| 2024-02-11 23:20:28 +0100 | <haskellbridge> | <irregularsphere> ~~*meanwhile me putting up `undefined` in `Instance Num`~~ |
| 2024-02-11 23:20:33 +0100 | dostoyevsky2 | (~sck@user/dostoyevsky2) |
| 2024-02-11 23:20:44 +0100 | <haskellbridge> | <irregularsphere> type correct as in mathematically correct |
| 2024-02-11 23:20:44 +0100 | <geekosaur> | because it's relatively weak |
| 2024-02-11 23:20:45 +0100 | <EvanR> | well typed programs don't get stuck |
| 2024-02-11 23:21:15 +0100 | puke | (~puke@user/puke) |
| 2024-02-11 23:21:34 +0100 | <geekosaur> | agda, idris, and coq among others have stronger type checkers |
| 2024-02-11 23:22:26 +0100 | <geekosaur> | and agda and idris can translate to haskell basically by doing the typechecking and then wrapping everything in unsafeCoerce aka "just trust me on this, okay?" |
| 2024-02-11 23:22:51 +0100 | <haskellbridge> | <irregularsphere> is unsafeCoerce basically "yeah i proved this myself" |
| 2024-02-11 23:22:57 +0100 | <geekosaur> | yes |
| 2024-02-11 23:23:07 +0100 | <haskellbridge> | <irregularsphere> oh so that's what it's for |
| 2024-02-11 23:23:59 +0100 | <EvanR> | there are programs that make sense that can't be type checked in haskell. And there are type checked programs in haskell that crash disgracefully |
| 2024-02-11 23:24:15 +0100 | <haskellbridge> | <irregularsphere> i wonder what unsafeCoerce# is up to |
| 2024-02-11 23:24:51 +0100 | <haskellbridge> | <irregularsphere> to be put up with such funny documentation |
| 2024-02-11 23:25:01 +0100 | <haskellbridge> | <irregularsphere> > Highly, terribly dangerous coercion from one representation type to another. Misuse of this function can invite the garbage collector to trounce upon your data and then laugh in your face. You don't want this function. Really. |
| 2024-02-11 23:26:10 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-02-11 23:27:11 +0100 | <geekosaur> | unsafeCoerce reinterprets one LiftedRep as a different LiftedRep. this is somewhat dangerous if the two aren't actually representationally compatible |
| 2024-02-11 23:28:06 +0100 | <geekosaur> | unsafeCoerce# reinteprets any TypeRep as a different TypeRep. this is a very good way to cause core dumps if you don't know exactly what you're doing |
| 2024-02-11 23:32:14 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-02-11 23:33:08 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-02-11 23:34:36 +0100 | mechap | (~mechap@user/mechap) (Quit: WeeChat 4.2.1) |
| 2024-02-11 23:51:38 +0100 | azr4e1 | (~azr4e1@137.220.68.193) |
| 2024-02-11 23:51:54 +0100 | azr4e1 | (~azr4e1@137.220.68.193) (Remote host closed the connection) |
| 2024-02-11 23:53:55 +0100 | JordiGH | (~jordi@user/jordigh) (Ping timeout: 268 seconds) |
| 2024-02-11 23:57:28 +0100 | random-jellyfish | (~developer@user/random-jellyfish) |