Logs: liberachat/#haskell
| 2021-07-30 09:47:12 | <yahb> | dminuoso: Foldable t => (a -> b -> b) -> b -> t a -> b |
| 2021-07-30 09:47:19 | <dminuoso> | dexterfoo: This is too liberabl on a. |
| 2021-07-30 09:48:03 | <dminuoso> | It's the same reason why we cant have Functor on Set |
| 2021-07-30 09:48:04 | × | eggplant_ quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2021-07-30 09:48:43 | <tomsmeding> | how exactly would foldr on vector be different (semantically) from \f x v -> foldr f x (toList v) |
| 2021-07-30 09:49:17 | <tomsmeding> | Unboxed.Vector can't be Functor for the reason you mention, but it could be Foldable, right? |
| 2021-07-30 09:49:18 | <dminuoso> | You can have MonoFoldable for it though. |
| 2021-07-30 09:50:09 | <dminuoso> | tomsmeding: No. |
| 2021-07-30 09:50:15 | <dminuoso> | foldr has to work for *all* a. |
| 2021-07-30 09:50:23 | → | MoC joins (~moc@user/moc) |
| 2021-07-30 09:50:26 | <tomsmeding> | given that you have a 't a', yes |
| 2021-07-30 09:50:48 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de) |
| 2021-07-30 09:50:49 | <tomsmeding> | oh right, the point is that an unboxed vector doesn't carry its Unbox dict with it? |
| 2021-07-30 09:51:03 | <dminuoso> | Not even that, it's that foldr is too general |
| 2021-07-30 09:51:47 | <tomsmeding> | well if I would define: data V a where V :: Unbox a => Unboxed.Vector a -> V a |
| 2021-07-30 09:51:50 | <dminuoso> | An `instance Foldable UnboxedVector` would need to impose an additional constraint on `a`, namely that its Unbox, such that you can actually make use of it. |
| 2021-07-30 09:51:57 | <dminuoso> | Oh well |
| 2021-07-30 09:51:59 | <dminuoso> | Yes you are right |
| 2021-07-30 09:52:11 | <tomsmeding> | I see |
| 2021-07-30 09:52:16 | <dminuoso> | If the dictionary was embedded and accessible, it seems possible |
| 2021-07-30 09:53:06 | <tomsmeding> | not saying that an unboxed vector should carry its Unbox dict with it -- not at all, just trying to understand :) |
| 2021-07-30 09:53:14 | <tomsmeding> | dexterfoo: ^ |
| 2021-07-30 09:53:24 | <dminuoso> | Sure. |
| 2021-07-30 09:54:16 | <dminuoso> | Though I think its hard to say what seems possible and what that would even mean, without an exact specification. |
| 2021-07-30 09:54:32 | <dminuoso> | So Ill stick to: Not possible |
| 2021-07-30 09:54:42 | <dminuoso> | MonoFoldable however can possibly get half the way |
| 2021-07-30 09:55:07 | <dminuoso> | Depending on your needs that is |
| 2021-07-30 09:55:43 | → | dhil joins (~dhil@195.213.192.47) |
| 2021-07-30 09:57:41 | <tomsmeding> | This compiles: |
| 2021-07-30 09:57:42 | <tomsmeding> | import qualified Data.Vector.Unboxed as U |
| 2021-07-30 09:57:42 | <tomsmeding> | data FatUVector a where FatUVector :: U.Unbox a => U.Vector a -> FatUVector a |
| 2021-07-30 09:57:42 | <tomsmeding> | instance Foldable FatUVector where foldr f x (FatUVector v) = U.foldr f x v |
| 2021-07-30 09:58:05 | <nshepperd> | you can totally have Foldable on a wrapper that carries the Unbox dict |
| 2021-07-30 09:59:03 | <nshepperd> | still can't have functor though ofc |
| 2021-07-30 09:59:46 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-30 10:00:41 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-30 10:00:42 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 240 seconds) |
| 2021-07-30 10:03:24 | → | oxide joins (~lambda@user/oxide) |
| 2021-07-30 10:06:26 | × | mthvedt quits (uid501949@id-501949.stonehaven.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-07-30 10:09:06 | × | Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Ping timeout: 276 seconds) |
| 2021-07-30 10:10:47 | × | OscarH quits (~OscarH@97e0e7ba.skybroadband.com) (Ping timeout: 265 seconds) |
| 2021-07-30 10:11:00 | → | drd joins (~drd@2001:b07:a70:9f1f:1562:34de:f50f:77d4) |
| 2021-07-30 10:12:58 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-30 10:13:20 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-30 10:15:46 | × | azeem quits (~azeem@dynamic-adsl-94-34-48-122.clienti.tiscali.it) (Ping timeout: 240 seconds) |
| 2021-07-30 10:15:52 | × | pe200012_ quits (~pe200012@183.236.83.77) (Remote host closed the connection) |
| 2021-07-30 10:16:19 | → | pe200012_ joins (~pe200012@113.105.10.33) |
| 2021-07-30 10:16:31 | pe200012_ | is now known as pe200012 |
| 2021-07-30 10:19:45 | → | azeem joins (~azeem@176.200.236.58) |
| 2021-07-30 10:23:33 | × | jonathanx quits (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) (Read error: Connection reset by peer) |
| 2021-07-30 10:23:34 | → | jonathanx_ joins (~jonathan@h-178-174-176-109.A357.priv.bahnhof.se) |
| 2021-07-30 10:25:28 | × | euandreh quits (~euandreh@2804:14c:33:9fe5:9526:d20a:c7ef:dc9b) (Quit: WeeChat 3.2) |
| 2021-07-30 10:26:00 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-30 10:28:42 | × | burnsidesLlama quits (~burnsides@dhcp168-019.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-07-30 10:35:03 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-30 10:35:40 | → | bens joins (~bens@www.typius.com) |
| 2021-07-30 10:37:00 | × | jespada quits (~jespada@90.254.247.46) (Ping timeout: 250 seconds) |
| 2021-07-30 10:39:24 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 2021-07-30 10:39:31 | → | jespada joins (~jespada@90.254.247.46) |
| 2021-07-30 10:41:34 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-07-30 10:44:50 | × | hueso quits (~root@user/hueso) (Ping timeout: 252 seconds) |
| 2021-07-30 10:48:00 | × | acidjnk_new quits (~acidjnk@p200300d0c72b9507354aa6404eb54f37.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2021-07-30 10:48:44 | → | hueso joins (~root@user/hueso) |
| 2021-07-30 10:54:50 | × | michalz quits (~michalz@185.246.204.40) (Ping timeout: 252 seconds) |
| 2021-07-30 10:55:54 | → | fef joins (~thedawn@user/thedawn) |
| 2021-07-30 10:56:43 | × | Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Quit: WeeChat 2.8) |
| 2021-07-30 10:57:05 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-07-30 10:58:21 | → | hexfive joins (~eric@50.35.83.177) |
| 2021-07-30 11:00:12 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-30 11:00:28 | → | burnsidesLlama joins (~burnsides@dhcp168-019.wadham.ox.ac.uk) |
| 2021-07-30 11:04:19 | × | mattil quits (~mattilinn@87-92-232-85.rev.dnainternet.fi) (Quit: Leaving) |
| 2021-07-30 11:05:57 | × | burnsidesLlama quits (~burnsides@dhcp168-019.wadham.ox.ac.uk) (Ping timeout: 245 seconds) |
| 2021-07-30 11:09:22 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-30 11:13:03 | ← | jakalx parts (~jakalx@base.jakalx.net) () |
| 2021-07-30 11:13:58 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 2021-07-30 11:15:32 | → | mikoto-chan joins (~mikoto-ch@ip-193-121-10-50.dsl.scarlet.be) |
| 2021-07-30 11:16:31 | × | Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Ping timeout: 265 seconds) |
| 2021-07-30 11:19:28 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-30 11:21:30 | × | azeem quits (~azeem@176.200.236.58) (Ping timeout: 240 seconds) |
| 2021-07-30 11:22:19 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 2021-07-30 11:22:45 | → | azeem joins (~azeem@176.200.236.58) |
| 2021-07-30 11:23:59 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds) |
| 2021-07-30 11:28:42 | × | Vajb quits (~Vajb@2001:999:62:1d53:26b1:6c9b:c1ed:9c01) (Read error: Connection reset by peer) |
| 2021-07-30 11:29:19 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) |
| 2021-07-30 11:29:28 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-07-30 11:29:59 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2021-07-30 11:31:03 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) |
| 2021-07-30 11:33:12 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-07-30 11:34:10 | × | drd quits (~drd@2001:b07:a70:9f1f:1562:34de:f50f:77d4) (Ping timeout: 240 seconds) |
| 2021-07-30 11:35:47 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-30 11:37:22 | × | fossdd quits (~fossdd@sourcehut/user/fossdd) (Ping timeout: 240 seconds) |
| 2021-07-30 11:37:53 | → | fossdd joins (~fossdd@sourcehut/user/fossdd) |
| 2021-07-30 11:38:57 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-07-30 11:41:24 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 276 seconds) |
| 2021-07-30 11:43:10 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2021-07-30 11:43:10 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 2021-07-30 11:43:13 | allbery_b | is now known as geekosaur |
| 2021-07-30 11:43:58 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-30 11:44:10 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 2021-07-30 11:45:32 | → | nate3 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
All times are in UTC.