Logs: liberachat/#haskell
| 2021-05-28 17:28:04 | <yahb> | dminuoso: * -> * -> * |
| 2021-05-28 17:28:30 | × | Bartosz quits (~textual@50.35.215.151) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-28 17:29:04 | × | gzj quits (~GZJ0X@185.212.59.97.16clouds.com) (Ping timeout: 264 seconds) |
| 2021-05-28 17:29:25 | → | xff0x joins (~xff0x@2001:1a81:53ff:e00:12bf:9005:d371:65a7) |
| 2021-05-28 17:29:27 | → | holy_ joins (~h01y_b4z0@2400:adc1:178:c800:9e45:76a9:57f2:1665) |
| 2021-05-28 17:29:44 | → | Bartosz joins (~textual@50.35.215.151) |
| 2021-05-28 17:30:46 | × | zava quits (~zava@ip5f5bdf0f.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2021-05-28 17:32:33 | × | arjun quits (~user@user/arjun) (Ping timeout: 272 seconds) |
| 2021-05-28 17:32:33 | <hololeap> | um, I may have been somewhat mixed up, but the definition straight from my code is: type ValidityWrapper a :: Type -> Type |
| 2021-05-28 17:32:38 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Quit: mikoto-chan) |
| 2021-05-28 17:32:54 | <dminuoso> | Ah, yeah. |
| 2021-05-28 17:33:01 | <dminuoso> | That's the same as my definition above |
| 2021-05-28 17:33:12 | <hololeap> | so that's what I meant in any case |
| 2021-05-28 17:33:20 | <dminuoso> | Think of thit as `(ValidityWrapper a) :: Type -> Type` |
| 2021-05-28 17:33:38 | <dminuoso> | If that makes sense |
| 2021-05-28 17:33:43 | <hololeap> | Yeah that does |
| 2021-05-28 17:34:11 | <dminuoso> | Anyway, the thing is, to implement Functor here, you'd have to have magic |
| 2021-05-28 17:34:58 | <boxscape> | % :browse GHC.Magic |
| 2021-05-28 17:34:58 | <yahb> | boxscape: inline :: a -> a; GHC.Exts.lazy :: a -> a; noinline :: a -> a; oneShot :: (a -> b) -> a -> b; runRW# :: (State# RealWorld -> o) -> o |
| 2021-05-28 17:35:12 | × | rk04 quits (~rk04@103.232.8.236) (Changing host) |
| 2021-05-28 17:35:12 | → | rk04 joins (~rk04@user/rajk) |
| 2021-05-28 17:35:30 | <dminuoso> | Your implementation must work for *all* choices of `a` and `b` without knowing them beforehand, but you dont even know whether you even have an `a` or how to access it. |
| 2021-05-28 17:35:57 | <dminuoso> | The reason it could be something different entirely, is because the tyfam could give you anything else back |
| 2021-05-28 17:36:08 | <dminuoso> | say `type instance ValidityWrapper T = Const Int` |
| 2021-05-28 17:37:05 | <dminuoso> | So how would `fmap (f :: T -> Bool)` function here? You can't make up a T here. |
| 2021-05-28 17:37:43 | × | Bartosz quits (~textual@50.35.215.151) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-05-28 17:39:05 | <dminuoso> | So even if we had `type instance ValidityWrapper Bool = Identity`, just for this simple choice of types `T` and `Bool`, you can only make up values of Bool |
| 2021-05-28 17:39:14 | <dminuoso> | But you couldnt even use the supplied function to fmap |
| 2021-05-28 17:39:28 | <dminuoso> | That alone breaks `fmap id = id` |
| 2021-05-28 17:41:52 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-28 17:42:18 | → | Bartosz joins (~textual@50.35.215.151) |
| 2021-05-28 17:44:06 | × | isovector1 quits (~isovector@172.103.216.166) (Ping timeout: 264 seconds) |
| 2021-05-28 17:44:31 | × | rk04 quits (~rk04@user/rajk) (Quit: Client closed) |
| 2021-05-28 17:44:59 | → | lu joins (~lu@user/lu) |
| 2021-05-28 17:45:00 | → | rk04 joins (~rk04@user/rajk) |
| 2021-05-28 17:46:54 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 248 seconds) |
| 2021-05-28 17:47:44 | × | Torro quits (Torro@gateway/vpn/protonvpn/torro) (Quit: bye) |
| 2021-05-28 17:49:57 | × | thelounge92 quits (~thelounge@cpe-23-240-28-18.socal.res.rr.com) (Quit: The Lounge - https://thelounge.chat) |
| 2021-05-28 17:50:15 | → | thelounge92 joins (~thelounge@cpe-23-240-28-18.socal.res.rr.com) |
| 2021-05-28 17:50:55 | × | lu quits (~lu@user/lu) (Ping timeout: 272 seconds) |
| 2021-05-28 17:50:55 | × | simendsjo quits (~user@cm-84.211.91.241.getinternet.no) (Ping timeout: 272 seconds) |
| 2021-05-28 17:51:04 | → | moet joins (~moet@172.58.27.119) |
| 2021-05-28 17:51:35 | × | haskman quits (~haskman@106.201.28.184) (Quit: Going to sleep. ZZZzzz…) |
| 2021-05-28 17:52:12 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-05-28 17:52:38 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 2021-05-28 17:52:59 | → | rahguzar joins (~rahguzar@dynamic-adsl-84-220-228-254.clienti.tiscali.it) |
| 2021-05-28 17:54:16 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2021-05-28 17:56:01 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-05-28 17:56:32 | → | sondre joins (~sondrelun@eduroam-193-157-244-179.wlan.uio.no) |
| 2021-05-28 17:59:34 | → | amahl joins (~amahl@dxv5skyy95x-mzmyd9kkt-3.rev.dnainternet.fi) |
| 2021-05-28 17:59:45 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 2021-05-28 18:01:08 | × | ubert quits (~Thunderbi@p200300ecdf259d8974882ed522245916.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2021-05-28 18:01:27 | → | ubert joins (~Thunderbi@p200300ecdf259d8974882ed522245916.dip0.t-ipconnect.de) |
| 2021-05-28 18:01:29 | × | sondre quits (~sondrelun@eduroam-193-157-244-179.wlan.uio.no) (Ping timeout: 272 seconds) |
| 2021-05-28 18:01:44 | × | connrs quits (~connrs@s1.connrs.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-05-28 18:03:04 | × | Guest2189 quits (~Guest21@121-75-79-99.dyn.vf.net.nz) (Ping timeout: 250 seconds) |
| 2021-05-28 18:03:53 | → | tekul joins (~tekul@82-68-220-238.dsl.in-addr.zen.co.uk) |
| 2021-05-28 18:05:28 | → | Guest31 joins (~textual@cpc146410-hari22-2-0-cust124.20-2.cable.virginm.net) |
| 2021-05-28 18:07:22 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 2021-05-28 18:07:34 | → | nsilv joins (~nsilv@host-82-50-119-12.retail.telecomitalia.it) |
| 2021-05-28 18:07:58 | × | rk04 quits (~rk04@user/rajk) (Quit: Client closed) |
| 2021-05-28 18:09:46 | × | sbmsr quits (~pi@212.102.61.51) (Ping timeout: 264 seconds) |
| 2021-05-28 18:10:22 | → | connrs joins (~connrs@s1.connrs.uk) |
| 2021-05-28 18:11:30 | → | sbmsr joins (~pi@2600:1700:63d0:4830:9670:3c44:ca85:cefd) |
| 2021-05-28 18:12:19 | × | dyeplexer quits (~dyeplexer@user/dyeplexer) (Remote host closed the connection) |
| 2021-05-28 18:14:01 | × | connrs quits (~connrs@s1.connrs.uk) (Client Quit) |
| 2021-05-28 18:14:40 | → | connrs joins (~connrs@s1.connrs.uk) |
| 2021-05-28 18:15:16 | × | hiptobecubic quits (~john@c-73-55-99-95.hsd1.fl.comcast.net) (Ping timeout: 264 seconds) |
| 2021-05-28 18:15:39 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-05-28 18:16:38 | → | haskman joins (~haskman@106.201.28.184) |
| 2021-05-28 18:17:18 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 248 seconds) |
| 2021-05-28 18:19:58 | × | fizbin quits (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) (Ping timeout: 248 seconds) |
| 2021-05-28 18:20:35 | × | connrs quits (~connrs@s1.connrs.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-05-28 18:21:17 | → | connrs joins (~connrs@s1.connrs.uk) |
| 2021-05-28 18:21:46 | × | connrs quits (~connrs@s1.connrs.uk) (Client Quit) |
| 2021-05-28 18:21:55 | × | xsperry quits (~as@user/xsperry) () |
| 2021-05-28 18:22:09 | × | Gurkenglas quits (~Gurkengla@dslb-088-075-022-175.088.075.pools.vodafone-ip.de) (Read error: No route to host) |
| 2021-05-28 18:22:23 | → | connrs joins (~connrs@s1.connrs.uk) |
| 2021-05-28 18:24:45 | × | connrs quits (~connrs@s1.connrs.uk) (Client Quit) |
| 2021-05-28 18:25:08 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 2021-05-28 18:25:24 | → | connrs joins (~connrs@s1.connrs.uk) |
| 2021-05-28 18:27:00 | → | xsperry joins (~as@user/xsperry) |
| 2021-05-28 18:27:38 | → | sondre joins (~sondrelun@eduroam-193-157-188-177.wlan.uio.no) |
| 2021-05-28 18:28:49 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-05-28 18:29:27 | → | vicfred joins (~vicfred@user/vicfred) |
| 2021-05-28 18:29:56 | → | pavonia joins (~user@user/siracusa) |
| 2021-05-28 18:30:24 | → | Mark_ joins (uid14803@user/mark/x-9597255) |
| 2021-05-28 18:35:06 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-05-28 18:35:35 | → | shiraeeshi joins (~shiraeesh@109.166.58.65) |
| 2021-05-28 18:37:02 | × | dunham quits (~dunham@97-113-35-16.tukw.qwest.net) (Ping timeout: 248 seconds) |
| 2021-05-28 18:38:26 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Remote host closed the connection) |
| 2021-05-28 18:40:14 | × | wagle quits (~wagle@quassel.wagle.io) (Ping timeout: 248 seconds) |
| 2021-05-28 18:42:23 | → | geekosaur joins (~geekosaur@069-135-003-034.biz.spectrum.com) |
| 2021-05-28 18:42:52 | → | isovector1 joins (~isovector@172.103.216.166) |
| 2021-05-28 18:43:17 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-05-28 18:44:45 | → | tose joins (~tose@ip-85-160-8-1.eurotel.cz) |
| 2021-05-28 18:45:00 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-05-28 18:46:15 | → | wagle joins (~wagle@quassel.wagle.io) |
| 2021-05-28 18:47:10 | × | werneta quits (~werneta@mobile-166-176-57-62.mycingular.net) (Ping timeout: 248 seconds) |
| 2021-05-28 18:47:57 | <monochrom> | Quiet Friday when there is no drama. |
All times are in UTC.