Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→
Page 1 .. 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 .. 18041
— 1,804,036 events total
2021-08-09 19:03:37 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-08-09 19:08:17 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 248 seconds)
2021-08-09 19:08:26 × curiousgay quits (~curiousga@77-120-186-48.kha.volia.net) (Ping timeout: 272 seconds)
2021-08-09 19:09:52 → jneira_ joins (~jneira_@28.red-80-28-169.staticip.rima-tde.net)
2021-08-09 19:09:57 <Gurkenglas> Is there a programming language that lets you implement ((a -> Void) -> Void) -> a? It would have to go "it must somewhere apply the (a -> Void) to an a, so lets take that a and return it instead."
2021-08-09 19:10:39 × mattil quits (~mattilinn@87-92-142-109.rev.dnainternet.fi) (Quit: Leaving)
2021-08-09 19:11:35 <davean> Gurkenglas: but thats not true? With a forall it might be
2021-08-09 19:12:24 <tomsmeding> Gurkenglas: why must it apply that particular function?
2021-08-09 19:12:25 <Gurkenglas> davean, it would be true in that language, hopefully. how would it be false?
2021-08-09 19:12:58 <Gurkenglas> tomsmeding, because that language does not allow one to actually have a Void
2021-08-09 19:13:16 <Gurkenglas> so the only place to get one is to use the given (a -> Void)
2021-08-09 19:13:33 <tomsmeding> because it has no knowledge of what 'a' is?
2021-08-09 19:13:56 <Gurkenglas> wut? no this works for String to
2021-08-09 19:14:02 <tomsmeding> then davean's suggestion is correct, I think: it should at least be (forall a. (a -> Void) -> Void) -> a
2021-08-09 19:14:06 <Gurkenglas> *too
2021-08-09 19:14:17 <tomsmeding> oh right
2021-08-09 19:14:29 <tomsmeding> but there might be another function in the environment with type Int -> Void
2021-08-09 19:14:33 <Gurkenglas> ((String -> Void) -> Void) -> Void, by inspecting the argument for what string it feeds into the (String -> Void)
2021-08-09 19:14:38 <tomsmeding> and then for a ~ Int it could just call that
2021-08-09 19:15:04 <tomsmeding> yeah my forall remark was incorrect
2021-08-09 19:15:37 <tomsmeding> heh this is double-negation elimination, which implies law of the excluded middle if I remember correctly
2021-08-09 19:15:45 <Gurkenglas> indeed, thats the point :)
2021-08-09 19:15:48 <tomsmeding> so this won't work in any language based on pure type theory
2021-08-09 19:17:23 <Gurkenglas> tomsmeding, if the environment contains another source of Void you'd only get a Maybe String
2021-08-09 19:17:46 <davean> I'd meant (forall b . (a -> b) -> b) -> a
2021-08-09 19:18:03 <davean> because it knows what Void is, but with forall it doesn't, and we can inject whatever b we want
2021-08-09 19:18:24 <tomsmeding> in which case, ($ id) suffices
2021-08-09 19:18:34 × pricly_yellow quits (~pricly_ye@2a01:620:c06f:6300::339) (Remote host closed the connection)
2021-08-09 19:20:01 × yoctocell quits (~user@h87-96-130-155.cust.a3fiber.se) (Ping timeout: 248 seconds)
2021-08-09 19:20:08 <tomsmeding> I wonder, given that 'a -> Void' is the usual encoding of "NOT a" in type theory, would 'forall b. a -> b' also be a valid encoding?
2021-08-09 19:20:35 <tomsmeding> it's at least as powerful, by substituting b = Void
2021-08-09 19:21:14 × Guest60 quits (~Guest60@2a01cb0589202e0024fe769e33dfd141.ipv6.abo.wanadoo.fr) (Quit: Client closed)
2021-08-09 19:21:54 × gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer)
2021-08-09 19:21:58 <tomsmeding> i.e. is it true that for all propositions that you can curry-howard implement using the 'a -> Void' convention, you can also implement them using the 'forall b. a -> b' convention?
2021-08-09 19:22:17 <tomsmeding> yes, by post-composing with 'absurd'
2021-08-09 19:22:47 → gentauro joins (~gentauro@user/gentauro)
2021-08-09 19:23:09 <tomsmeding> so with that alternative encoding of "NOT a", the encoding of "NOT (NOT a) => a" in a type would be (forall b. (forall c. a -> c) -> b) -> a)
2021-08-09 19:23:18 × Natch quits (~natch@c-e070e255.014-297-73746f25.bbcust.telenor.se) (Remote host closed the connection)
2021-08-09 19:23:53 × lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 268 seconds)
2021-08-09 19:23:56 → Natch joins (~natch@c-e070e255.014-297-73746f25.bbcust.telenor.se)
2021-08-09 19:24:16 <tomsmeding> heh and then ($ id) doesn't work anymore
2021-08-09 19:24:18 → pricly_yellow joins (~pricly_ye@2a01:620:c06f:6300::339)
2021-08-09 19:25:36 × talismanick quits (~user@2601:644:8502:d700::8fb8) (Ping timeout: 272 seconds)
2021-08-09 19:25:57 × ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds)
2021-08-09 19:26:42 <tomsmeding> of course it doesn't because that would be a proof that ~~a => a in type theory, and that's impossible
2021-08-09 19:30:58 × eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-08-09 19:31:21 → eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-08-09 19:31:34 × markpythonicbitc quits (~markpytho@2601:647:5a00:35:112f:f355:ed76:9e65) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-08-09 19:33:04 → ec joins (~ec@gateway/tor-sasl/ec)
2021-08-09 19:33:18 → Guest662 joins (~Guest66@2a01cb0589202e0024fe769e33dfd141.ipv6.abo.wanadoo.fr)
2021-08-09 19:33:19 × Guest662 quits (~Guest66@2a01cb0589202e0024fe769e33dfd141.ipv6.abo.wanadoo.fr) (Client Quit)
2021-08-09 19:35:02 × pricly_yellow quits (~pricly_ye@2a01:620:c06f:6300::339) (Remote host closed the connection)
2021-08-09 19:38:19 SIben_ is now known as SIben
2021-08-09 19:38:36 → burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-08-09 19:39:22 → _73 joins (~user@pool-96-252-123-136.bstnma.fios.verizon.net)
2021-08-09 19:39:49 → burnside_ joins (~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-08-09 19:40:02 ← _73 parts (~user@pool-96-252-123-136.bstnma.fios.verizon.net) ()
2021-08-09 19:40:05 × burnside_ quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Read error: Connection reset by peer)
2021-08-09 19:40:13 → burnside_ joins (~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-08-09 19:40:19 × burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Read error: Connection reset by peer)
2021-08-09 19:43:22 → MoC joins (~moc@user/moc)
2021-08-09 19:43:44 → zebrag joins (~chris@user/zebrag)
2021-08-09 19:44:33 × Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Ping timeout: 248 seconds)
2021-08-09 19:44:36 → Pickchea joins (~private@user/pickchea)
2021-08-09 19:44:59 → Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es)
2021-08-09 19:47:07 → segfaultfizzbuzz joins (~segfaultf@157-131-253-1.fiber.dynamic.sonic.net)
2021-08-09 19:47:17 × Atum_ quits (~IRC@user/atum/x-2392232) (Quit: Atum_)
2021-08-09 19:48:49 ← segfaultfizzbuzz parts (~segfaultf@157-131-253-1.fiber.dynamic.sonic.net) ()
2021-08-09 19:50:02 → markpythonicbitc joins (~markpytho@c-24-6-12-87.hsd1.ca.comcast.net)
2021-08-09 19:50:06 × zebrag quits (~chris@user/zebrag) (Remote host closed the connection)
2021-08-09 19:52:38 × cheater quits (~Username@user/cheater) (Ping timeout: 258 seconds)
2021-08-09 19:53:10 → cheater joins (~Username@user/cheater)
2021-08-09 19:54:07 → pschorf` joins (~user@c-73-77-28-188.hsd1.tx.comcast.net)
2021-08-09 19:54:53 × pschorf` quits (~user@c-73-77-28-188.hsd1.tx.comcast.net) (Remote host closed the connection)
2021-08-09 19:57:40 → jgeerds joins (~jgeerds@55d45555.access.ecotel.net)
2021-08-09 19:58:03 → merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2021-08-09 19:58:46 → pgib joins (~textual@173.38.117.78)
2021-08-09 19:59:55 × _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection)
2021-08-09 20:00:17 panda_man is now known as koala_man
2021-08-09 20:02:41 × Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Ping timeout: 248 seconds)
2021-08-09 20:02:47 ← nova parts (novasenco@user/nova) (♥☺)
2021-08-09 20:03:07 × burnside_ quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection)
2021-08-09 20:03:58 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds)
2021-08-09 20:05:07 × juhp quits (~juhp@128.106.188.220) (Ping timeout: 245 seconds)
2021-08-09 20:08:04 → juhp joins (~juhp@128.106.188.220)
2021-08-09 20:10:00 × emliunix quits (~emliunix@103.138.75.119) (Remote host closed the connection)
2021-08-09 20:10:23 → emliunix joins (~emliunix@2a09:bac0:23::815:bca)
2021-08-09 20:11:25 × ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds)
2021-08-09 20:11:48 → gehmehgeh joins (~user@user/gehmehgeh)
2021-08-09 20:12:57 → Sadeq joins (~Sadeq@93.110.31.186)
2021-08-09 20:13:55 × Sadeq quits (~Sadeq@93.110.31.186) (Client Quit)
2021-08-09 20:14:13 → Sadeq joins (~Sadeq@93.110.31.186)
2021-08-09 20:15:26 × qbt quits (~edun@user/edun) (Quit: Leaving)
2021-08-09 20:15:39 × Sadeq quits (~Sadeq@93.110.31.186) (Client Quit)
2021-08-09 20:20:34 → pricly_yellow joins (~pricly_ye@2a01:620:c06f:6300::339)
2021-08-09 20:20:58 × eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-08-09 20:21:26 <myShoggoth> Gil Mizrahi has posted the Haskell performance tuning book proposal, please check it out, give feedback, and volunteer your expertise!
2021-08-09 20:21:26 <myShoggoth> https://github.com/haskellfoundation/tech-proposals/pull/9
2021-08-09 20:22:49 → ec joins (~ec@gateway/tor-sasl/ec)
2021-08-09 20:29:48 → acidjnk joins (~acidjnk@p200300d0c72b9517f81283fc8b5e04b5.dip0.t-ipconnect.de)
←Prev  Next→
Page 1 .. 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 .. 18041

All times are in UTC.