Logs on 2024-06-13 (liberachat/#haskell)
| 00:10:54 | → | vizimajac joins (vizimajac@shell.xshellz.com) |
| 00:12:08 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 00:12:51 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 00:13:29 | Lord_of_Life_ | is now known as Lord_of_Life |
| 00:14:13 | → | dcoutts joins (~duncan@212.140.138.201) |
| 00:14:17 | × | dcoutts quits (~duncan@212.140.138.201) (Remote host closed the connection) |
| 00:17:07 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 00:19:45 | → | emmanuelux_ joins (~emmanuelu@user/emmanuelux) |
| 00:19:51 | → | tabemann joins (~tabemann@2600:1700:7990:24e0:f01:e94f:2e5:5d5d) |
| 00:20:42 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Ping timeout: 255 seconds) |
| 00:23:03 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 00:28:32 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 00:38:23 | × | Square2 quits (~Square4@user/square) (Ping timeout: 264 seconds) |
| 00:56:18 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 00:57:25 | → | califax joins (~califax@user/califx) |
| 01:11:23 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 01:13:36 | → | joeyadams joins (~joeyadams@2603:6010:5100:2ed:909:ef37:664d:c6a7) |
| 01:21:19 | × | dev2 quits (~dev@2405:201:c062:801d:4d6f:d1e8:5a8c:26e3) (Quit: WeeChat 4.3.2) |
| 01:44:25 | × | xff0x quits (~xff0x@2405:6580:b080:900:611b:282b:7bc2:c44f) (Ping timeout: 255 seconds) |
| 01:55:11 | × | krei-se quits (~krei-se@p57af2529.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 01:55:11 | → | krei-se- joins (~krei-se@p5085de1f.dip0.t-ipconnect.de) |
| 01:59:39 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 02:07:26 | × | y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 02:21:11 | × | dysthesis quits (~dysthesis@user/dysthesis) (Quit: dysthesis) |
| 02:30:27 | × | wagle quits (~wagle@quassel.wagle.io) (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.) |
| 02:31:23 | → | wagle joins (~wagle@quassel.wagle.io) |
| 02:33:02 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:55:27 | × | td_ quits (~td@i5387092E.versanet.de) (Ping timeout: 264 seconds) |
| 02:56:46 | → | td_ joins (~td@i53870929.versanet.de) |
| 02:57:49 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 268 seconds) |
| 03:00:54 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 03:14:50 | × | joeyadams quits (~joeyadams@2603:6010:5100:2ed:909:ef37:664d:c6a7) (Quit: Leaving) |
| 03:16:37 | × | tabemann quits (~tabemann@2600:1700:7990:24e0:f01:e94f:2e5:5d5d) (Ping timeout: 268 seconds) |
| 03:18:15 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 03:25:14 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 03:25:30 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 03:33:17 | → | whatsupdoc joins (uid509081@id-509081.hampstead.irccloud.com) |
| 03:38:18 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Read error: Connection reset by peer) |
| 03:40:22 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 03:40:58 | → | michalz joins (~michalz@185.246.207.203) |
| 03:40:59 | → | euleritian joins (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) |
| 03:42:48 | × | michalz quits (~michalz@185.246.207.203) (Client Quit) |
| 03:45:36 | → | michalz joins (~michalz@185.246.207.201) |
| 03:45:41 | → | aforemny_ joins (~aforemny@i59F516D7.versanet.de) |
| 03:46:48 | × | aforemny quits (~aforemny@2001:9e8:6cf6:d100:13b7:91e0:122d:7bf6) (Ping timeout: 255 seconds) |
| 03:48:57 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 03:51:23 | → | danse-nr3 joins (~danse-nr3@151.37.247.23) |
| 03:57:43 | <haskellbridge> | <James> Hello |
| 04:04:35 | <Axman6> | Hello! |
| 04:09:06 | <Axman6> | rustisafungus: What is jax? |
| 04:09:34 | <Axman6> | rustisafungus: There's quite a few talks out there on implementing differentiation in Haskell, maybe they would be helpful? |
| 04:19:18 | → | andrei_n joins (~andrei_n@user/andrei-n:62396) |
| 04:35:36 | → | y04nn joins (~username@2a03:1b20:8:f011::e10d) |
| 04:38:53 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 04:39:44 | × | euleritian quits (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 04:40:01 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 04:40:53 | × | danse-nr3 quits (~danse-nr3@151.37.247.23) (Ping timeout: 240 seconds) |
| 04:50:43 | × | andrei_n quits (~andrei_n@user/andrei-n:62396) (Ping timeout: 255 seconds) |
| 04:54:03 | → | danse-nr3 joins (~danse-nr3@151.37.247.23) |
| 04:54:39 | → | andrei_n joins (~andrei_n@2a02:a03f:c091:a800:2023:eb80:7e75:618b) |
| 04:54:39 | × | andrei_n quits (~andrei_n@2a02:a03f:c091:a800:2023:eb80:7e75:618b) (Changing host) |
| 04:54:39 | → | andrei_n joins (~andrei_n@user/andrei-n:62396) |
| 04:54:57 | × | danse-nr3 quits (~danse-nr3@151.37.247.23) (Remote host closed the connection) |
| 04:55:21 | → | danse-nr3 joins (~danse-nr3@151.37.247.23) |
| 05:05:15 | → | alexherbo2 joins (~alexherbo@2a02-8440-3301-9f46-013f-12cf-5855-af6b.rev.sfr.net) |
| 05:05:56 | <rustisafungus> | Axman6: jax is google's machine learning framework, like pytorch... although jax is python based it demands that you write pure functions |
| 05:08:12 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 05:11:11 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 252 seconds) |
| 05:30:02 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:33:54 | × | TheCoffeMaker_ quits (~TheCoffeM@200.114.213.75) (Ping timeout: 255 seconds) |
| 05:42:33 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 05:44:19 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 05:45:08 | → | euleritian joins (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) |
| 05:46:31 | → | acidjnk joins (~acidjnk@p200300d6e714dc24101446769eacf81f.dip0.t-ipconnect.de) |
| 05:53:23 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 05:58:19 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 05:58:52 | → | rvalue joins (~rvalue@user/rvalue) |
| 06:20:42 | <[exa]> | Axman6: kinda like accelerate, but in python |
| 06:21:00 | × | jcarpenter2 quits (~lol@96.78.87.198) (Ping timeout: 268 seconds) |
| 06:25:19 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 260 seconds) |
| 06:26:20 | × | echoreply quits (~echoreply@2001:19f0:9002:1f3b:5400:ff:fe6f:8b8d) (Quit: WeeChat 2.8) |
| 06:27:39 | → | echoreply joins (~echoreply@45.32.163.16) |
| 06:35:23 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:37:04 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 06:41:45 | → | poscat joins (~poscat@user/poscat) |
| 06:42:26 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:44:18 | → | jcarpenter2 joins (~lol@96.78.87.198) |
| 06:46:26 | × | causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.3.1) |
| 06:49:02 | <danse-nr3> | kinda like pytorch, without side effects? |
| 06:50:32 | × | ft quits (~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:54:40 | → | robobub joins (uid248673@id-248673.uxbridge.irccloud.com) |
| 06:56:26 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 256 seconds) |
| 07:10:58 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 07:12:27 | × | euleritian quits (~euleritia@dynamic-176-001-135-088.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:12:44 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:15:45 | → | oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 07:16:15 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 07:16:27 | × | danse-nr3 quits (~danse-nr3@151.37.247.23) (Ping timeout: 264 seconds) |
| 07:17:07 | → | danse-nr3 joins (~danse-nr3@151.35.245.71) |
| 07:17:26 | → | califax joins (~califax@user/califx) |
| 07:17:41 | × | mjacob quits (~mjacob@adrastea.uberspace.de) (Read error: Connection reset by peer) |
| 07:22:47 | → | mjacob joins (~mjacob@adrastea.uberspace.de) |
| 07:31:52 | → | CiaoSen joins (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) |
| 07:31:52 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 07:33:28 | → | califax joins (~califax@user/califx) |
| 07:48:00 | → | tomku joins (~tomku@syn-141-126-184-057.res.spectrum.com) |
| 07:48:11 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 07:53:09 | → | gmg joins (~user@user/gehmehgeh) |
| 07:54:12 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 07:58:22 | × | danse-nr3 quits (~danse-nr3@151.35.245.71) (Ping timeout: 246 seconds) |
| 07:58:22 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 07:59:29 | × | notzmv quits (~daniel@user/notzmv) (Ping timeout: 272 seconds) |
| 08:00:06 | × | tomku quits (~tomku@syn-141-126-184-057.res.spectrum.com) (Remote host closed the connection) |
| 08:00:17 | → | danse-nr3 joins (~danse-nr3@151.35.245.71) |
| 08:00:20 | → | tomku joins (~tomku@syn-141-126-184-057.res.spectrum.com) |
| 08:02:00 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 08:04:27 | × | CiaoSen quits (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) (Ping timeout: 264 seconds) |
| 08:05:03 | × | danse-nr3 quits (~danse-nr3@151.35.245.71) (Ping timeout: 264 seconds) |
| 08:08:54 | sprout_ | is now known as sprout |
| 08:10:28 | → | danza joins (~francesco@151.35.245.71) |
| 08:12:53 | × | y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 08:20:00 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 08:20:32 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 08:25:34 | × | danza quits (~francesco@151.35.245.71) (Ping timeout: 268 seconds) |
| 08:27:27 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 08:37:11 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:37:53 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 08:43:53 | → | Guest19 joins (~Guest76@49.245.75.147) |
| 08:45:53 | → | danse-nr3 joins (~danse-nr3@151.35.245.71) |
| 08:51:46 | × | danse-nr3 quits (~danse-nr3@151.35.245.71) (Remote host closed the connection) |
| 08:52:07 | → | danse-nr3 joins (~danse-nr3@151.35.245.71) |
| 08:54:13 | × | danse-nr3 quits (~danse-nr3@151.35.245.71) (Remote host closed the connection) |
| 08:54:38 | → | danse-nr3 joins (~danse-nr3@151.35.245.71) |
| 08:56:04 | → | nickiminjaj joins (~nickiminj@188.146.127.82) |
| 08:56:04 | × | nickiminjaj quits (~nickiminj@188.146.127.82) (Changing host) |
| 08:56:04 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 09:02:49 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 09:04:41 | → | chele joins (~chele@user/chele) |
| 09:08:58 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 09:11:17 | × | destituion quits (~destituio@77.18.53.84.tmi.telenormobil.no) (Read error: Connection reset by peer) |
| 09:12:17 | → | destituion joins (~destituio@85.221.111.174) |
| 09:17:22 | × | seeg123456 quits (~seeg12345@64.176.64.83) (Ping timeout: 268 seconds) |
| 09:18:06 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:21:56 | → | CiaoSen joins (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) |
| 09:31:31 | × | andrei_n quits (~andrei_n@user/andrei-n:62396) (Ping timeout: 255 seconds) |
| 09:31:53 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 09:41:40 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:44:33 | → | andrei_n joins (~andrei_n@2a02:a03f:c091:a800:4cc9:832b:d3d8:de1c) |
| 09:44:33 | × | andrei_n quits (~andrei_n@2a02:a03f:c091:a800:4cc9:832b:d3d8:de1c) (Changing host) |
| 09:44:33 | → | andrei_n joins (~andrei_n@user/andrei-n:62396) |
| 09:44:44 | → | akegalj joins (~akegalj@141-138-29-155.dsl.iskon.hr) |
| 09:49:38 | × | MironZ3 quits (~MironZ@nat-infra.ehlab.uk) (Quit: The Lounge - https://thelounge.chat) |
| 09:50:13 | → | MironZ3 joins (~MironZ@nat-infra.ehlab.uk) |
| 09:55:29 | → | __monty__ joins (~toonn@user/toonn) |
| 09:59:54 | × | akegalj quits (~akegalj@141-138-29-155.dsl.iskon.hr) (Quit: leaving) |
| 10:00:03 | → | nickiminjaj joins (~nickiminj@188.146.127.82) |
| 10:00:03 | × | nickiminjaj quits (~nickiminj@188.146.127.82) (Changing host) |
| 10:00:03 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 10:02:37 | × | Guest19 quits (~Guest76@49.245.75.147) (Quit: Client closed) |
| 10:04:00 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:05:40 | <kuribas> | With types it's easy to verify that a field is used but doesn't exist. |
| 10:06:04 | <kuribas> | What about the opposite? For example you want to verify that a field that is passed to a REST api is actually used somewhere. |
| 10:09:48 | → | notzmv joins (~daniel@user/notzmv) |
| 10:15:51 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds) |
| 10:16:49 | → | absence joins (torgeihe@hildring.pvv.ntnu.no) |
| 10:17:43 | <tomsmeding> | kuribas: bind the individual fields to individual variables, and rely on an unused variable warning? |
| 10:18:35 | × | xdminsy quits (~xdminsy@117.147.70.212) (Quit: Konversation terminated!) |
| 10:18:55 | <kuribas> | tomsmeding: but you are not forced to put all fields in the record, no? |
| 10:20:13 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 10:21:21 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 272 seconds) |
| 10:22:58 | <tomsmeding> | ok I guess this depends on how you get the fields from the API |
| 10:23:20 | <tomsmeding> | at some point, in the beginning, there is a parser that gets all fields from the wire format |
| 10:23:40 | <absence> | I want to apply "f :: a -> m b" to an "a :: Maybe a" in a MaybeT context. Are there other options than "MaybeT (traverse f a)" or "lift . f =<< hoistMaybe a"? Both feel a bit finnicky, but maybe that can't be helped. |
| 10:24:57 | <tomsmeding> | absence: the "natural" thing would be 'f <$> a', of course, but that gives you a Maybe (m b) instead of an m (Maybe b) |
| 10:25:10 | <tomsmeding> | and monads cannot be commuted in general |
| 10:25:27 | × | alexherbo2 quits (~alexherbo@2a02-8440-3301-9f46-013f-12cf-5855-af6b.rev.sfr.net) (Remote host closed the connection) |
| 10:25:32 | <tomsmeding> | specifically in the case of Maybe you can, but you have to use something Maybe-specific |
| 10:25:55 | <tomsmeding> | with your 'traverse' alternative, the Maybe-specific thing you're using is that Maybe is not only a Monad, but also Traversable |
| 10:26:03 | <tomsmeding> | with the second alternative, well, you're using hoistMaybe |
| 10:26:18 | <tomsmeding> | there will always be something |
| 10:28:52 | <ncf> | what's an "MaybeT context"? |
| 10:29:33 | <absence> | tomsmeding: Right. Since MaybeT is also Maybe specific, I was hoping there were other clever options, but possibly they would have to amount to something similar. |
| 10:30:20 | <absence> | ncf: The result of applying the function should be of type "MaybeT m b". |
| 10:30:38 | <tomsmeding> | ncf: presumably they're in a do-block in the 'MaybeT m' monad |
| 10:32:22 | <ncf> | hmm |
| 10:33:13 | <ncf> | i'd go with the hoistMaybe thing probably |
| 10:33:16 | <tomsmeding> | this also has the right type: MaybeT (return a) >>= MaybeT . fmap Just . f |
| 10:33:22 | <tomsmeding> | more verbose than all the other alternatives |
| 10:33:25 | <tomsmeding> | but I guess more principled? |
| 10:33:36 | <ncf> | meh, you've just inlined lift and hoistMaybe |
| 10:33:40 | <tomsmeding> | maybe :p |
| 10:44:29 | → | Square2 joins (~Square4@user/square) |
| 10:50:03 | × | andrei_n quits (~andrei_n@user/andrei-n:62396) (Ping timeout: 264 seconds) |
| 10:59:50 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:01:18 | <lortabac> | kuribas: import the fields explicitly instead of using the (..) syntax, so you get unused warnings |
| 11:05:34 | <kuribas> | lortabac: If I do Foo{bar}, I don't get a warning if I add "baz", no? |
| 11:06:12 | <lortabac> | ah I was thinking in the opposite sense |
| 11:07:15 | <lortabac> | I mean you already know all the fields, you just want to ensure that they are used in that module |
| 11:07:45 | <tomsmeding> | kuribas: don't use record syntax in the pattern match |
| 11:07:59 | <tomsmeding> | you lose labels but you get a name resolution error if the number of fields changes |
| 11:08:02 | <kuribas> | tomsmeding: positional? That sucks. |
| 11:08:06 | <tomsmeding> | fair |
| 11:08:13 | <tomsmeding> | haskell records suck :p |
| 11:08:17 | <kuribas> | true |
| 11:08:47 | <lortabac> | to be honest this looks like a simple warning to add |
| 11:09:39 | <kuribas> | like a pragma CompleteRecordFields? |
| 11:09:49 | <lortabac> | yes |
| 11:10:21 | <tomsmeding> | where would the pragma be added? On the record or on the match |
| 11:10:23 | <tomsmeding> | ? |
| 11:10:28 | <kuribas> | On the module? |
| 11:10:30 | <lortabac> | it's probably only useful in rare specific cases, so I wouldn't enable it in -Wall |
| 11:10:30 | <tomsmeding> | bad |
| 11:10:38 | <kuribas> | ok :) |
| 11:10:55 | <tomsmeding> | we need less of these things that apply gratuitously to everything once you want them for one particular case :p |
| 11:11:15 | <tomsmeding> | -Worphans, RebindableSyntax, Overloaded* |
| 11:11:29 | <lortabac> | tomsmeding: +1 |
| 11:11:37 | <Rembane> | Worphans is the best word. |
| 11:11:46 | <tomsmeding> | :D |
| 11:11:51 | → | andrei_n joins (~andrei_n@user/andrei-n:62396) |
| 11:12:06 | <tomsmeding> | I cannot read that as anything else than -W orphans, I guess I learned C before I learned English |
| 11:13:18 | × | danse-nr3 quits (~danse-nr3@151.35.245.71) (Read error: Connection reset by peer) |
| 11:13:38 | → | danse-nr3 joins (~danse-nr3@151.43.251.36) |
| 11:20:12 | → | xff0x joins (~xff0x@2405:6580:b080:900:1910:1409:8fe6:7f05) |
| 11:20:46 | <Rembane> | tomsmeding: There's a joke here involving &humor in C, but I can't spell it out. |
| 11:24:26 | <int-e> | I don't get the reference. |
| 11:24:58 | <Rembane> | It's probably not initialized. UB! :O |
| 11:25:18 | <int-e> | (C doesn't have references :-P) |
| 11:26:51 | <Rembane> | This is true, but isn't it possible to reference something using the ampersand? |
| 11:27:41 | <int-e> | You'd get a pointer. |
| 11:28:37 | <Rembane> | That's true, my joke totally failed. :D |
| 11:29:04 | <Rembane> | It's "dereferencing", so uh... yeah... |
| 11:42:10 | <mauke> | C lets you dereference without having references; Java can throw a NullPointerException without having pointers |
| 11:44:39 | × | danse-nr3 quits (~danse-nr3@151.43.251.36) (Ping timeout: 264 seconds) |
| 11:46:01 | <ncf> | pointers are an implementation of references |
| 11:51:37 | <Rembane> | mauke: Programming languages are weird. It's the Saphire Worphan hypothesis all over again! |
| 11:54:32 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:01:48 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 255 seconds) |
| 12:04:42 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 12:09:22 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 12:13:28 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:14:18 | → | danse-nr3 joins (~danse-nr3@151.43.251.36) |
| 12:15:16 | × | danse-nr3 quits (~danse-nr3@151.43.251.36) (Remote host closed the connection) |
| 12:15:40 | → | danse-nr3 joins (~danse-nr3@151.43.251.36) |
| 12:23:42 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 12:23:50 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 12:28:41 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 12:34:19 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 12:45:03 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 12:47:41 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 12:48:07 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 12:50:07 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 268 seconds) |
| 12:58:38 | → | rosco joins (~rosco@175.136.155.137) |
| 13:00:15 | → | nickiminjaj_ joins (~nickiminj@user-5-173-188-100.play-internet.pl) |
| 13:00:15 | × | nickiminjaj_ quits (~nickiminj@user-5-173-188-100.play-internet.pl) (Changing host) |
| 13:00:15 | → | nickiminjaj_ joins (~nickiminj@user/laxhh) |
| 13:04:27 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Ping timeout: 264 seconds) |
| 13:08:37 | → | someone235 joins (uid419897@id-419897.ilkley.irccloud.com) |
| 13:09:50 | × | nickiminjaj_ quits (~nickiminj@user/laxhh) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 13:11:50 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 13:22:40 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 13:24:35 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit) |
| 13:25:42 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal) |
| 13:25:48 | → | ystael joins (~ystael@user/ystael) |
| 13:27:33 | × | andrei_n quits (~andrei_n@user/andrei-n:62396) (Quit: Leaving) |
| 13:32:05 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 13:35:59 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit) |
| 13:38:03 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 13:42:25 | <danse-nr3> | @hoogle Maybe (a -> Maybe b) -> a -> Maybe b |
| 13:42:26 | <lambdabot> | Util apMA :: Monad m => m (a -> m b) -> a -> m b |
| 13:43:44 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 13:44:06 | <danse-nr3> | doesn't seem to be a thing at https://hoogle.haskell.org/?hoogle=Maybe%20(a%20-%3E%20Maybe%20b)%20-%3E%20a%20-%3E%20Maybe%20b |
| 13:45:49 | → | TactfulCitrus joins (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) |
| 13:47:19 | → | brett48 joins (~brett48@cpc91312-watf11-2-0-cust1213.15-2.cable.virginm.net) |
| 13:48:58 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 13:49:40 | <danse-nr3> | so i am not sure from which package does that Util come |
| 13:50:50 | → | euleritian joins (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) |
| 13:50:55 | <tomsmeding> | danse-nr3: https://hackage.haskell.org/package/util-0.1.17.1/docs/Util.html |
| 13:51:08 | <tomsmeding> | the description of that package is "Deprecated" |
| 13:51:41 | <danse-nr3> | thanks tomsmeding! |
| 13:52:43 | <danse-nr3> | this signature is too weird anyways i hope to get to something simpler eventually |
| 13:53:55 | <tomsmeding> | :t (join .) . fmap . flip id |
| 13:53:56 | <lambdabot> | Monad m => b -> m (b -> m a) -> m a |
| 13:55:00 | → | gdl_ joins (~gdl__@mob-5-91-23-178.net.vodafone.it) |
| 13:55:08 | <danse-nr3> | ^^; a bit of type-fu. Kind of spoiled the fun but still appreciated |
| 13:55:21 | <gdl_> | Hi all! Just updated to vscode 1.90 and HLS seems not to be working at all :( |
| 13:59:54 | × | euleritian quits (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 14:00:13 | → | euleritian joins (~euleritia@77.22.252.56) |
| 14:04:09 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 14:04:19 | <danse-nr3> | not sure gdl_ not using neither vscode nor HLS |
| 14:04:27 | <gdl_> | manually downgrading to vscode 1.89 works as a quick fix... Any hint on where to report this? |
| 14:05:39 | × | Square2 quits (~Square4@user/square) (Ping timeout: 264 seconds) |
| 14:05:39 | <EvanR> | maybe there is an HLS channel here |
| 14:05:56 | <EvanR> | yay breakage |
| 14:06:13 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 14:06:35 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Client Quit) |
| 14:07:12 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 14:07:49 | <ncf> | :t (=<<) . (&) |
| 14:07:51 | <lambdabot> | Monad m => a -> m (a -> m b) -> m b |
| 14:08:13 | × | TactfulCitrus quits (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection) |
| 14:09:24 | → | TactfulCitrus joins (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) |
| 14:09:37 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 255 seconds) |
| 14:09:57 | → | califax joins (~califax@user/califx) |
| 14:10:32 | → | euleritian joins (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) |
| 14:10:54 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 14:11:07 | <tomsmeding> | #haskell-language-server |
| 14:11:25 | <tomsmeding> | gdl_: try there, but they may redirect you elsewhere again |
| 14:14:13 | <gdl_> | thank you :) |
| 14:17:14 | <danse-nr3> | ooh, the (=<<) . (&) solution looks more meaningful to me |
| 14:17:59 | <danse-nr3> | in fact it's kind of explaining the uncanny-valley feeling i had about that type |
| 14:18:33 | × | TactfulCitrus quits (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection) |
| 14:21:26 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 14:22:18 | → | TactfulCitrus joins (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) |
| 14:23:38 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 14:26:44 | → | eron joins (~eron@179.98.163.50) |
| 14:30:38 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 14:38:13 | × | eron quits (~eron@179.98.163.50) (Ping timeout: 250 seconds) |
| 14:38:31 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 14:44:39 | × | destituion quits (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 14:49:22 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 14:51:14 | × | TactfulCitrus quits (~al@2a02:8012:87a6:0:fbe0:6116:6e30:e047) (Remote host closed the connection) |
| 14:53:00 | → | destituion joins (~destituio@2a02:2121:306:89fe:6583:236:fa09:18d5) |
| 14:55:11 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 14:55:29 | → | k_hachig joins (~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca) |
| 14:57:56 | × | nickiminjaj quits (~nickiminj@user/laxhh) (Quit: Textual IRC Client: www.textualapp.com) |
| 14:58:09 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 15:03:45 | → | nickiminjaj joins (~nickiminj@user/laxhh) |
| 15:06:46 | × | picnoir quits (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Ping timeout: 255 seconds) |
| 15:07:10 | × | noctux quits (~noctux@user/noctux) (Read error: Connection reset by peer) |
| 15:11:03 | × | dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 264 seconds) |
| 15:11:56 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 15:13:50 | weechat | is now known as dminuoso |
| 15:15:21 | × | danse-nr3 quits (~danse-nr3@151.43.251.36) (Read error: Connection reset by peer) |
| 15:15:39 | → | danse-nr3 joins (~danse-nr3@151.47.241.29) |
| 15:17:16 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 15:24:05 | → | noctux joins (~noctux@user/noctux) |
| 15:26:46 | × | mauke quits (~mauke@user/mauke) (Read error: Connection reset by peer) |
| 15:29:19 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 15:32:25 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Client Quit) |
| 15:32:33 | → | mauke joins (~mauke@user/mauke) |
| 15:32:34 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 15:33:54 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Client Quit) |
| 15:35:39 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 15:42:38 | → | puke joins (~puke@user/puke) |
| 15:42:42 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:42:57 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 15:48:11 | × | euleritian quits (~euleritia@dynamic-176-001-010-018.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:48:28 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:51:13 | × | cyphase quits (~cyphase@user/cyphase) (Ping timeout: 246 seconds) |
| 15:51:56 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:52:12 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 255 seconds) |
| 15:52:45 | → | picnoir joins (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) |
| 15:58:59 | × | someone235 quits (uid419897@id-419897.ilkley.irccloud.com) (Quit: Connection closed for inactivity) |
| 16:01:54 | × | CiaoSen quits (~Jura@2a05:5800:2cb:b00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 16:03:02 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 16:03:15 | × | danse-nr3 quits (~danse-nr3@151.47.241.29) (Ping timeout: 264 seconds) |
| 16:11:55 | → | yin joins (~yin@user/zero) |
| 16:12:01 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 16:12:33 | × | haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection) |
| 16:14:26 | × | gdl_ quits (~gdl__@mob-5-91-23-178.net.vodafone.it) (Remote host closed the connection) |
| 16:18:38 | → | haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com) |
| 16:18:38 | ChanServ | sets mode +v haskellbridge |
| 16:19:50 | → | danse-nr3 joins (~danse-nr3@151.47.241.29) |
| 16:22:43 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 16:23:26 | × | danse-nr3 quits (~danse-nr3@151.47.241.29) (Remote host closed the connection) |
| 16:34:22 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 16:40:54 | → | califax joins (~califax@user/califx) |
| 16:47:07 | × | hueso quits (~root@user/hueso) (Ping timeout: 255 seconds) |
| 16:49:17 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 16:53:39 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 16:54:59 | → | euleritian joins (~euleritia@dynamic-176-003-011-033.176.3.pool.telefonica.de) |
| 16:58:27 | × | rdcdr quits (~rdcdr@user/rdcdr) (Ping timeout: 264 seconds) |
| 16:58:54 | × | Me-me quits (~me-me@user/me-me) (Remote host closed the connection) |
| 16:59:21 | → | hueso joins (~root@user/hueso) |
| 16:59:28 | → | Me-me joins (~me-me@kc.randomserver.name) |
| 17:01:14 | × | euleritian quits (~euleritia@dynamic-176-003-011-033.176.3.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:01:31 | → | euleritian joins (~euleritia@77.22.252.56) |
| 17:01:47 | → | henry40408 joins (~henry4040@175.182.111.183) |
| 17:04:07 | → | rdcdr joins (~rdcdr@user/rdcdr) |
| 17:14:36 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:15:14 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 17:16:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:17:50 | → | osogyian joins (~osogyian@2804:1b3:6603:6f0b:4dd2:8d4e:c6db:c6b7) |
| 17:19:53 | ← | osogyian parts (~osogyian@2804:1b3:6603:6f0b:4dd2:8d4e:c6db:c6b7) () |
| 17:22:27 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 17:28:17 | × | rosco quits (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 17:39:17 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:42:51 | <lxsameer> | would it be possible to define a dependent type using type families? |
| 17:44:57 | <EvanR> | by promoting then reimplementing all the value level code for e.g. numbers, that is how you can go about getting dependentish types with type families |
| 17:45:02 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 17:45:39 | <lxsameer> | EvanR: got it. Thank you |
| 17:48:56 | × | ocra8 quits (~ocra8@user/ocra8) (Read error: Connection reset by peer) |
| 17:53:47 | → | ocra8 joins (~ocra8@user/ocra8) |
| 17:54:03 | <haskellbridge> | <sm> yikes, thanks for the heads up. Checking my VS Code updates are manual |
| 17:54:22 | → | ft joins (~ft@p3e9bcb39.dip0.t-ipconnect.de) |
| 17:59:41 | × | ocra8 quits (~ocra8@user/ocra8) (Ping timeout: 240 seconds) |
| 18:00:59 | → | ocra8 joins (~ocra8@user/ocra8) |
| 18:03:36 | × | brett48 quits (~brett48@cpc91312-watf11-2-0-cust1213.15-2.cable.virginm.net) (Quit: brett48) |
| 18:05:35 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 18:08:26 | → | califax_ joins (~califax@user/califx) |
| 18:08:59 | → | Chai-T-Rex joins (~ChaiTRex@user/chaitrex) |
| 18:09:24 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 18:10:34 | × | califax quits (~califax@user/califx) (Ping timeout: 260 seconds) |
| 18:10:34 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 18:10:35 | califax_ | is now known as califax |
| 18:11:02 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 18:11:02 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
| 18:12:29 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 18:12:53 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 18:15:32 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 18:17:41 | <tomsmeding> | lxsameer: aren't GADTs more the thing that you can get limited dependencies with? |
| 18:18:07 | <tomsmeding> | type families are restricted to the type level, and the "dependencies" of "dependent types" refer to types depending on terms |
| 18:18:58 | <tomsmeding> | with GADTs you can have types depend on GADT constructors, thus you do get actual _dependent_ types -- albeit limited to GADT constructors, not arbitrary values |
| 18:22:07 | <lxsameer> | got it. but in my understanding you can use type families that "depend" (loosly) on terms. right? |
| 18:22:50 | gehmehgeh | is now known as gmg |
| 18:22:54 | <dolio> | GADTs correspond to inductive families/indexed inductive types. But the indices are entirely at the type level for GADTs. |
| 18:23:46 | <dolio> | So they're not really like dependent types, still. You have to manually establish a correspondence between values and types. |
| 18:24:21 | <EvanR> | type families map types to types, but using DataKinds you can more conveniently clone value constructors to the type level to use for that |
| 18:24:42 | <yin> | what are the advantages of dependent types, performance-wise? |
| 18:24:49 | <yin> | if there are any |
| 18:24:58 | <EvanR> | at runtime there are no types, so none xD |
| 18:25:20 | <dolio> | In principle you have more detailed information for static analysis, but that is rarely actually realized. |
| 18:25:46 | <yin> | well, by using them the runtime will likely be different from when you don't use them, right? |
| 18:26:11 | <EvanR> | data families could have different runtime implementation at different indices |
| 18:26:12 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:26:23 | × | hueso quits (~root@user/hueso) (Ping timeout: 264 seconds) |
| 18:27:25 | <EvanR> | the main thing I've seen dependent types used for is guaranteeing properties and invariants before it all gets compiled away |
| 18:27:39 | <yin> | knowing your Int can only be < x must open the door to some memory management optimizations, i imagine |
| 18:28:09 | → | hueso joins (~root@user/hueso) |
| 18:28:20 | <EvanR> | using Fin X for numbers less than X (and greater than or equal to zero) likely performs WORSE, due to more naive implementation |
| 18:28:46 | <EvanR> | Int that is known to be within some range sounds more like liquid types |
| 18:29:02 | <yin> | well yeah bad example |
| 18:29:23 | <dolio> | I mean, you could detect and optimize. |
| 18:30:08 | <dolio> | Like, Agda's ℕ is in principle defined in unary, but it gets handled specially to use Haskell's Integer behind the scenes. |
| 18:31:17 | <dolio> | But, most dependently typed languages aren't in the business of doing stuff like that right now. |
| 18:33:24 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 18:40:47 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 18:47:23 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 18:48:34 | × | rvalue quits (~rvalue@user/rvalue) (Remote host closed the connection) |
| 18:49:02 | → | rvalue joins (~rvalue@user/rvalue) |
| 18:52:02 | → | Square joins (~Square@user/square) |
| 19:03:00 | → | cyphase joins (~cyphase@user/cyphase) |
| 19:09:58 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 19:10:18 | → | Guest13 joins (~Guest13@220.67.223.22) |
| 19:10:39 | × | foul_owl quits (~kerry@185.216.231.181) (Ping timeout: 255 seconds) |
| 19:10:50 | → | foul_owl joins (~kerry@174-21-146-130.tukw.qwest.net) |
| 19:11:02 | × | Guest13 quits (~Guest13@220.67.223.22) (Client Quit) |
| 19:16:54 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 19:21:36 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds) |
| 19:23:51 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 19:25:01 | <probie> | Depending on your dependently typed language and how you "run" code, `Σ ℕ (λn → n < X)` may perform no worse than `ℕ` (e.g. in Coq with "run" meaning running code extracted to OCaml or Haskell), although I don't know of any where it performs better |
| 19:25:50 | → | noumenon joins (~noumenon@113.51-175-156.customer.lyse.net) |
| 19:29:44 | × | dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 252 seconds) |
| 19:30:01 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 19:30:45 | <probie> | I think it'd be completely unexpected if a function with type `∀ {x y : ℕ} → x < y → Σ ℕ (λn → n < x) → Σ ℕ (λn → n < y)` were to change the representation of the first part of the pair if `y` was much bigger than `x` |
| 19:34:28 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:35:27 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 19:38:44 | <tomsmeding> | if one has evidence of the maximum value of a natural number, one might be able to eliminate bounds checks when using them as an index into arrays, for example |
| 19:38:51 | <tomsmeding> | thus they can improve performance in some cases |
| 19:39:33 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 19:39:40 | <tomsmeding> | but that typically requires a careful setup, plus care that the proofs of those bounds (to satisfy the type checker that the bounds are indeed valid) do not require additional runtime code that more than negates the wins from eliminated bounds checks |
| 19:40:28 | <dolio> | I don't think it's that hard to see how it could effectively change the representation. Integer in GHC is either a word-sized thing or an arbitrary precision thing. So for small enough x, you can know that you will actually never have the arbitrary-precision thing. |
| 19:40:32 | <tomsmeding> | this can, I guess, be seen as a type theory implementation of what compiler writers (of languages with bounds checks) already do |
| 19:40:50 | <dolio> | Then you optimize everything with that type to only operate on word-sized things. |
| 19:42:34 | × | henry40408 quits (~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds)) |
| 19:42:59 | → | henry40408 joins (~henry4040@175.182.111.183) |
| 19:43:04 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 19:45:18 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:53:39 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 19:59:22 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:06:26 | → | andrei_n joins (~andrei_n@user/andrei-n:62396) |
| 20:08:03 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:18:40 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 20:19:02 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 20:20:20 | × | hueso quits (~root@user/hueso) (Ping timeout: 252 seconds) |
| 20:20:47 | → | hueso joins (~root@user/hueso) |
| 20:21:28 | → | mei joins (~mei@user/mei) |
| 20:26:39 | × | andrei_n quits (~andrei_n@user/andrei-n:62396) (Ping timeout: 264 seconds) |
| 20:26:46 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds) |
| 20:38:10 | × | yin quits (~yin@user/zero) (Ping timeout: 268 seconds) |
| 20:38:55 | → | yin joins (~yin@user/zero) |
| 20:38:58 | → | causal joins (~eric@50.35.88.207) |
| 20:40:22 | × | k_hachig quits (~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca) (Ping timeout: 256 seconds) |
| 20:43:26 | × | yin quits (~yin@user/zero) (Ping timeout: 252 seconds) |
| 20:43:42 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 20:44:17 | → | yin joins (~yin@user/zero) |
| 20:44:39 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 20:49:50 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 20:54:11 | → | k_hachig joins (~k_hachig@65.94.221.127) |
| 21:03:52 | × | michalz quits (~michalz@185.246.207.201) (Quit: ZNC 1.9.0 - https://znc.in) |
| 21:08:33 | × | opqdonut quits (opqdonut@pseudo.fixme.fi) (Ping timeout: 255 seconds) |
| 21:08:47 | × | Me-me quits (~me-me@kc.randomserver.name) (Changing host) |
| 21:08:47 | → | Me-me joins (~me-me@user/me-me) |
| 21:15:11 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:18:22 | × | sp1ff quits (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 21:21:18 | → | rvalue- joins (~rvalue@user/rvalue) |
| 21:22:01 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 21:22:34 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 268 seconds) |
| 21:25:17 | rvalue- | is now known as rvalue |
| 21:28:26 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:35:32 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 21:37:54 | → | mei joins (~mei@user/mei) |
| 21:39:52 | → | sp1ff joins (~user@c-24-21-45-157.hsd1.wa.comcast.net) |
| 21:41:04 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 21:41:29 | → | euleritian joins (~euleritia@dynamic-176-003-011-016.176.3.pool.telefonica.de) |
| 21:43:05 | × | k_hachig quits (~k_hachig@65.94.221.127) (Quit: WeeChat 4.3.2) |
| 21:44:13 | → | k_hachig joins (~k_hachig@bras-base-mtrlpq42zf4-grc-08-65-94-221-127.dsl.bell.ca) |
| 21:44:46 | × | AlexZenon quits (~alzenon@178.34.163.204) (Ping timeout: 268 seconds) |
| 21:44:54 | → | pavonia joins (~user@user/siracusa) |
| 21:53:37 | → | AlexZenon joins (~alzenon@178.34.163.204) |
| 21:55:09 | → | gabiruh_ joins (~gabiruh@vps19177.publiccloud.com.br) |
| 21:56:02 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 252 seconds) |
| 22:03:53 | × | yin quits (~yin@user/zero) (Remote host closed the connection) |
| 22:10:53 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 22:18:32 | × | acidjnk quits (~acidjnk@p200300d6e714dc24101446769eacf81f.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 22:21:15 | × | Square quits (~Square@user/square) (Ping timeout: 264 seconds) |
| 22:22:27 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 264 seconds) |
| 22:23:09 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 22:27:29 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 22:33:15 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 264 seconds) |
| 22:35:12 | × | barrucadu quits (~barrucadu@carcosa.barrucadu.co.uk) (Remote host closed the connection) |
| 22:37:51 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 22:42:06 | → | iqubic joins (~sophia@2601:602:9502:c70:e652:d0e0:e8d1:62b3) |
| 22:43:29 | <iqubic> | How are poeple today? |
| 22:50:23 | <pavonia> | Indeterminate |
| 22:52:29 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 272 seconds) |
| 22:53:17 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 22:53:25 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 22:54:50 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:57:04 | → | barrucadu joins (~barrucadu@carcosa.barrucadu.co.uk) |
| 22:58:54 | × | danso quits (~danso@user/danso) (Quit: quittin time) |
| 22:59:03 | × | dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 264 seconds) |
| 23:00:11 | → | danso joins (~danso@user/danso) |
| 23:00:43 | → | dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 23:05:34 | <EvanR> | ⊥ |
| 23:06:51 | × | iqubic quits (~sophia@2601:602:9502:c70:e652:d0e0:e8d1:62b3) (Ping timeout: 264 seconds) |
| 23:06:51 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 23:08:58 | → | iqubic joins (~sophia@2601:602:9502:c70:686a:4fef:cd21:89a7) |
| 23:09:48 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:19:27 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 264 seconds) |
| 23:21:17 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 23:28:37 | × | rustisafungus quits (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Ping timeout: 256 seconds) |
| 23:29:21 | → | rustisafungus joins (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) |
| 23:39:13 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Read error: Connection reset by peer) |
| 23:39:47 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 23:40:02 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 23:41:10 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 23:53:15 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
| 23:55:40 | → | mei joins (~mei@user/mei) |
| 23:56:14 | × | mei quits (~mei@user/mei) (Remote host closed the connection) |
All times are in UTC on 2024-06-13.