Logs: freenode/#haskell
| 2021-03-29 16:43:24 | × | Tene quits (~tene@poipu/supporter/slacker/tene) (Ping timeout: 246 seconds) |
| 2021-03-29 16:44:06 | × | ByronJohnson quits (~bairyn@unaffiliated/bob0) (Ping timeout: 246 seconds) |
| 2021-03-29 16:44:17 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 2021-03-29 16:45:56 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 2021-03-29 16:46:10 | <sclv> | psa btw, hackage web interface is down while we fix disk storage issues |
| 2021-03-29 16:46:18 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 260 seconds) |
| 2021-03-29 16:46:21 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Client Quit) |
| 2021-03-29 16:46:32 | <Gurkenglas> | do dependent types get me "that subtype of A defined by the property f : A -> Bool"? (or perhaps A -> ()) |
| 2021-03-29 16:47:23 | × | zaquest quits (~notzaques@5.128.210.178) (Read error: Connection reset by peer) |
| 2021-03-29 16:47:45 | → | LKoen joins (~LKoen@65.250.88.92.rev.sfr.net) |
| 2021-03-29 16:47:49 | → | zaquest joins (~notzaques@5.128.210.178) |
| 2021-03-29 16:47:52 | → | CrazyPython joins (~crazypyth@98.122.164.118) |
| 2021-03-29 16:50:25 | <dolio> | A -> () is isomorphic to () in most dependently typed languages. |
| 2021-03-29 16:50:57 | → | jonathanx_ joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 2021-03-29 16:52:26 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Remote host closed the connection) |
| 2021-03-29 16:52:44 | <dolio> | The Sierpinski type would need to be defined instead. |
| 2021-03-29 16:52:55 | × | jonathanx_ quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Remote host closed the connection) |
| 2021-03-29 16:53:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 16:53:49 | ← | justsomeguy parts (~justsomeg@unaffiliated/--/x-3805311) ("WeeChat 3.0.1") |
| 2021-03-29 16:53:52 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 2021-03-29 16:54:13 | → | jonathanx joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 2021-03-29 16:54:30 | <dolio> | Or a Sierpinski type, since there wouldn't be a unique choice in a lot of cases. |
| 2021-03-29 16:55:08 | → | ByronJohnson joins (~bairyn@unaffiliated/bob0) |
| 2021-03-29 16:55:25 | → | Tene joins (~tene@mail.digitalkingdom.org) |
| 2021-03-29 16:55:25 | × | Tene quits (~tene@mail.digitalkingdom.org) (Changing host) |
| 2021-03-29 16:55:25 | → | Tene joins (~tene@poipu/supporter/slacker/tene) |
| 2021-03-29 16:56:38 | × | ukari quits (~ukari@unaffiliated/ukari) (Ping timeout: 240 seconds) |
| 2021-03-29 16:58:27 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2021-03-29 16:58:36 | × | evanjs quits (~evanjs@075-129-098-007.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2021-03-29 16:58:38 | → | pupuupup joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 2021-03-29 17:03:02 | → | average joins (uid473595@gateway/web/irccloud.com/x-tblkdtktwteghrni) |
| 2021-03-29 17:03:24 | × | codygman__ quits (~user@209.251.131.98) (Remote host closed the connection) |
| 2021-03-29 17:03:28 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-29 17:03:35 | ski | . o O ( "First Steps in Synthetic Computability Theory" by Andrej Bauer in 2004 at <http://math.andrej.com/2005/05/08/first-steps-in-synthetic-computability-theory/> ) |
| 2021-03-29 17:03:51 | → | gitgood joins (~gitgood@80-44-12-39.dynamic.dsl.as9105.com) |
| 2021-03-29 17:03:57 | → | codygman__ joins (~user@209.251.131.98) |
| 2021-03-29 17:06:52 | <monochrom> | I think when you wrote "A -> ()" you had "relation between A and ()" in mind. |
| 2021-03-29 17:06:56 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 2021-03-29 17:07:32 | <monochrom> | Because I recently used that in parametricity theorems to obtain induction/elimination principles. :) |
| 2021-03-29 17:08:06 | × | pupuupup quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 240 seconds) |
| 2021-03-29 17:09:29 | → | DTZUZU joins (~DTZUZO@205.ip-149-56-132.net) |
| 2021-03-29 17:10:10 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-29 17:12:10 | → | Erutuon_ joins (~Erutuon@97-116-16-233.mpls.qwest.net) |
| 2021-03-29 17:12:39 | × | DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 268 seconds) |
| 2021-03-29 17:12:54 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-29 17:12:56 | × | chele quits (~chele@ip5b40237d.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2021-03-29 17:13:32 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 2021-03-29 17:14:52 | → | pupuupup_ joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 2021-03-29 17:14:59 | × | knupfer quits (~Thunderbi@200116b82b0bfe00e407e369ad43ca6f.dip.versatel-1u1.de) (Ping timeout: 245 seconds) |
| 2021-03-29 17:17:13 | <dolio> | Well, you don't just want any relation. |
| 2021-03-29 17:17:31 | <dolio> | Because that is A -> Ω. |
| 2021-03-29 17:17:36 | <dolio> | Not A -> Σ |
| 2021-03-29 17:17:37 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 258 seconds) |
| 2021-03-29 17:19:57 | <dolio> | You can kind of pretend that () is Σ in some ways in something like Haskell, although there is no good encoding of the other truth value types. |
| 2021-03-29 17:20:29 | <dolio> | At least, I think. |
| 2021-03-29 17:21:27 | × | lawid quits (~quassel@dslb-090-186-122-181.090.186.pools.vodafone-ip.de) (Quit: lawid) |
| 2021-03-29 17:22:19 | × | astronavt quits (~astronavt@unaffiliated/astronavt) (Remote host closed the connection) |
| 2021-03-29 17:23:21 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 2021-03-29 17:25:39 | × | Jesin quits (~Jesin@pool-72-66-101-18.washdc.fios.verizon.net) (Quit: Leaving) |
| 2021-03-29 17:26:31 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-03-29 17:26:46 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-03-29 17:27:55 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-03-29 17:29:11 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 2021-03-29 17:30:38 | × | __minoru__shirae quits (~shiraeesh@109.166.57.99) (Ping timeout: 240 seconds) |
| 2021-03-29 17:30:49 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 245 seconds) |
| 2021-03-29 17:31:21 | × | gentauro quits (~gentauro@unaffiliated/gentauro) (Read error: Connection reset by peer) |
| 2021-03-29 17:31:43 | → | gentauro joins (~gentauro@unaffiliated/gentauro) |
| 2021-03-29 17:33:09 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 240 seconds) |
| 2021-03-29 17:34:19 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-29 17:37:18 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 2021-03-29 17:38:06 | × | pupuupup_ quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 260 seconds) |
| 2021-03-29 17:39:22 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 276 seconds) |
| 2021-03-29 17:39:43 | → | nuncanada joins (~dude@179.235.160.168) |
| 2021-03-29 17:40:12 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 17:44:28 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-29 17:44:38 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-29 17:44:54 | → | pupuupup_ joins (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) |
| 2021-03-29 17:46:00 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 2021-03-29 17:47:11 | × | ixlun quits (~matthew@109.249.184.133) (Ping timeout: 240 seconds) |
| 2021-03-29 17:49:12 | × | pupuupup_ quits (~pupuupup@node-1p6.pool-125-24.dynamic.totinternet.net) (Ping timeout: 246 seconds) |
| 2021-03-29 17:49:23 | × | ubert quits (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2021-03-29 17:49:30 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-03-29 17:49:35 | → | dandart joins (~Thunderbi@home.dandart.co.uk) |
| 2021-03-29 17:49:49 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-29 17:50:02 | × | geekosaur quits (82650c7a@130.101.12.122) (Ping timeout: 240 seconds) |
| 2021-03-29 17:51:46 | × | dandart quits (~Thunderbi@home.dandart.co.uk) (Client Quit) |
| 2021-03-29 17:52:23 | × | vicfred quits (vicfred@gateway/vpn/mullvad/vicfred) (Quit: Leaving) |
| 2021-03-29 17:52:27 | → | dmoerner joins (~dmoerner@fedora/dmoerner) |
| 2021-03-29 17:52:58 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Ping timeout: 240 seconds) |
| 2021-03-29 17:53:24 | <dmoerner> | hackage is down, I guess |
| 2021-03-29 17:53:45 | <tomsmeding> | dmoerner: disk space issues, it's being worked on |
| 2021-03-29 17:53:58 | <tdammers> | talk about spofs... |
| 2021-03-29 17:54:23 | <dmoerner> | tomsmeding: no problem. |
| 2021-03-29 17:54:26 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 260 seconds) |
| 2021-03-29 17:54:26 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 240 seconds) |
| 2021-03-29 17:54:47 | <tomsmeding> | Does haskell have some kind of "injective type classes"? In particular, given 'instance C b => C (a, b)' and the information 'C (a, b)', I'd like to be able to infer 'C b', but GHC can't |
| 2021-03-29 17:55:01 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-29 17:55:14 | <Gurkenglas> | monochrom, by A -> () I mean the monotonic functions from A to (), not necessarily strict, one-to-one with the Scott-open sets in A |
| 2021-03-29 17:55:34 | <tomsmeding> | (my actual use case has 'a -> b' instead of '(a, b)', but I can't imagine that to make a difference) |
| 2021-03-29 17:55:38 | → | sgibber2018 joins (d055ed90@208.85.237.144) |
All times are in UTC.