Logs: freenode/#haskell
| 2021-03-29 15:45:37 | × | SrPx quits (sid108780@gateway/web/irccloud.com/x-bbnjzembhmbnppsc) (Ping timeout: 276 seconds) |
| 2021-03-29 15:46:16 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-edqceocpkulqhglr) (Ping timeout: 276 seconds) |
| 2021-03-29 15:46:19 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-29 15:46:55 | × | mudri quits (sid317655@gateway/web/irccloud.com/x-mxbgcmszbbzcrnwx) (Ping timeout: 276 seconds) |
| 2021-03-29 15:47:08 | → | gaze__ joins (sid387101@gateway/web/irccloud.com/x-jyfzdgulluqjzdzf) |
| 2021-03-29 15:47:33 | → | SrPx joins (sid108780@gateway/web/irccloud.com/x-mmboofbtgdacydlo) |
| 2021-03-29 15:47:38 | → | kiweun joins (~kiweun@2607:fea8:2a62:9600:30e4:9f38:5ce5:23cb) |
| 2021-03-29 15:48:06 | → | mudri joins (sid317655@gateway/web/irccloud.com/x-bcigdzdisjxobsht) |
| 2021-03-29 15:48:21 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-kcdtjlkqhzglspxx) |
| 2021-03-29 15:49:07 | → | ep1ctetus joins (~epictetus@ip72-194-215-136.sb.sd.cox.net) |
| 2021-03-29 15:49:51 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 2021-03-29 15:50:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-03-29 15:50:30 | → | Sorny joins (~Sornaensi@077213203030.dynamic.telenor.dk) |
| 2021-03-29 15:51:08 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-29 15:51:11 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-29 15:51:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 15:53:41 | × | Sorna quits (~Sornaensi@79.142.232.102.static.router4.bolignet.dk) (Ping timeout: 240 seconds) |
| 2021-03-29 15:54:17 | × | enoq quits (~textual@194-208-146-143.lampert.tv) (Quit: Textual IRC Client: www.textualapp.com) |
| 2021-03-29 15:54:18 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-29 15:55:31 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 250 seconds) |
| 2021-03-29 15:57:22 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:cca4:232:630d:d55c) |
| 2021-03-29 15:57:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-03-29 15:57:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 15:58:05 | → | ezrakilty joins (~ezrakilty@97-113-58-224.tukw.qwest.net) |
| 2021-03-29 15:59:41 | → | vicfred joins (vicfred@gateway/vpn/mullvad/vicfred) |
| 2021-03-29 16:00:05 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 2021-03-29 16:00:27 | → | Rudd0 joins (~Rudd0@185.189.115.103) |
| 2021-03-29 16:00:37 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Remote host closed the connection) |
| 2021-03-29 16:01:03 | → | idhugo__ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-29 16:02:46 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-03-29 16:03:27 | → | codygman__ joins (~user@47.186.207.161) |
| 2021-03-29 16:03:44 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 16:04:12 | × | xff0x quits (~xff0x@2001:1a81:5268:4b00:6095:39e:f552:2f81) (Ping timeout: 246 seconds) |
| 2021-03-29 16:04:13 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-29 16:05:13 | → | xff0x joins (~xff0x@2001:1a81:5268:4b00:52c4:a3b3:40c7:ac40) |
| 2021-03-29 16:05:46 | <Gurkenglas> | What language or language extension do I want to model types like "real numbers where a less defined than b <=> a at most b" and "1-lipschitz functions on the previous type"? |
| 2021-03-29 16:05:48 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Remote host closed the connection) |
| 2021-03-29 16:05:54 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2021-03-29 16:08:12 | <xerox_> | am I completely off track wanting this? deriving instance Enum a => Enum (Maybe a |
| 2021-03-29 16:08:26 | <xerox_> | (using StandaloneDeriving and friends) |
| 2021-03-29 16:08:28 | → | geekosaur joins (82650c7a@130.101.12.122) |
| 2021-03-29 16:08:37 | × | ezrakilty quits (~ezrakilty@97-113-58-224.tukw.qwest.net) (Remote host closed the connection) |
| 2021-03-29 16:08:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-03-29 16:09:23 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 16:11:37 | <[exa]> | xerox_: it's been discussed already for sure, but I don't remember the result |
| 2021-03-29 16:12:15 | <[exa]> | uh what, hackage down? |
| 2021-03-29 16:12:40 | <[exa]> | anyway, xerox_: Data.Enum.Deriving wouldn't work? |
| 2021-03-29 16:13:38 | × | codygman__ quits (~user@47.186.207.161) (Ping timeout: 240 seconds) |
| 2021-03-29 16:13:59 | <xerox_> | first time delving into (non-haskell-2010-)deriving, didn't know about that package, just trying to figure out what ghc allows me to do as is for starters |
| 2021-03-29 16:14:41 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-03-29 16:15:38 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-29 16:16:38 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-29 16:17:09 | × | andreas31 quits (~andreas@gateway/tor-sasl/andreas303) (Ping timeout: 240 seconds) |
| 2021-03-29 16:17:40 | <xerox_> | open to other ideas as well, trying to go from a newtype Foo = .. with deriving Enum to data Bar = Other | Foo and get that extra "Other" snuck in there into Enum |
| 2021-03-29 16:18:00 | <dexterfoo> | hello when will hackage docs be back online? |
| 2021-03-29 16:18:36 | <xerox_> | I guess in the meanwhile one can use stackage.org |
| 2021-03-29 16:18:41 | <xerox_> | I often default to that one anyway |
| 2021-03-29 16:18:48 | → | andreas31 joins (~andreas@gateway/tor-sasl/andreas303) |
| 2021-03-29 16:19:48 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:30e4:9f38:5ce5:23cb) (Remote host closed the connection) |
| 2021-03-29 16:20:16 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-29 16:20:18 | × | zjp quits (~zjp@66-45-138-104-dynamic.midco.net) (Remote host closed the connection) |
| 2021-03-29 16:20:52 | → | kiweun joins (~kiweun@2607:fea8:2a62:9600:bd23:b03d:cd6e:b210) |
| 2021-03-29 16:20:54 | → | dbmikus joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2021-03-29 16:21:51 | → | cake_eater joins (~kiweun@2607:fea8:2a62:9600:b1d8:81d4:b440:7736) |
| 2021-03-29 16:23:19 | → | blackriversoftwa joins (sid364914@gateway/web/irccloud.com/x-elfvrucbyuzljosj) |
| 2021-03-29 16:23:21 | × | conal quits (~conal@107.181.166.205) (Quit: Computer has gone to sleep.) |
| 2021-03-29 16:24:00 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2021-03-29 16:25:25 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:bd23:b03d:cd6e:b210) (Ping timeout: 252 seconds) |
| 2021-03-29 16:25:49 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-29 16:26:03 | × | [exa] quits (exa@srv3.blesmrt.net) (Changing host) |
| 2021-03-29 16:26:03 | → | [exa] joins (exa@unaffiliated/exa/x-5381537) |
| 2021-03-29 16:26:14 | × | cake_eater quits (~kiweun@2607:fea8:2a62:9600:b1d8:81d4:b440:7736) (Ping timeout: 245 seconds) |
| 2021-03-29 16:26:24 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-03-29 16:27:35 | → | codygman__ joins (~user@209.251.131.98) |
| 2021-03-29 16:28:23 | <slack1256> | Gurkenglas: you probably want agda by then |
| 2021-03-29 16:28:33 | <slack1256> | Computable real numbers and all that jazz |
| 2021-03-29 16:29:36 | × | haritz quits (~hrtz@unaffiliated/haritz) (Quit: ZNC 1.7.2+deb3 - https://znc.in) |
| 2021-03-29 16:30:26 | <slack1256> | dexterfoo: If you have a local copy of the libraries you want documentation of, you can see where those html are with the command `ghc-pkg field <package> haddock-html`. |
| 2021-03-29 16:31:28 | <statusbot> | Status update: Due to a disk space issue the hackage web interface is down for a storage upgrade. -- http://status.haskell.org/pages/incident/537c07b0cf1fad5830000093/606200df2a84ed05341dcbf1 |
| 2021-03-29 16:32:09 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-29 16:32:54 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-29 16:33:00 | × | jonathanx_ quits (~jonathan@94.234.49.69) (Read error: Connection reset by peer) |
| 2021-03-29 16:33:11 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-29 16:35:24 | <Gurkenglas> | slack1256, not quite computable real numbers. I mean a type where each element corresponds to a real number and the definedness relation (in the sense that undefined is less defined than "asd") corresponds to the usual order on real numbers |
| 2021-03-29 16:35:30 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 2021-03-29 16:36:05 | <Gurkenglas> | (i mean, i can kinda make one: newtype Real = UnsafeReal {greaterThan :: Double -> ()}; embedDouble :: Double -> Real; embedDouble d = UnsafeReal (\d' -> if d>d' then () else error ("embedDouble" + show d + show d')) -- but it's not type safe) |
| 2021-03-29 16:36:39 | × | borne quits (~fritjof@200116b864978000f7ed9fd86a2491f0.dip.versatel-1u1.de) (Ping timeout: 245 seconds) |
| 2021-03-29 16:39:24 | × | codygman__ quits (~user@209.251.131.98) (Remote host closed the connection) |
| 2021-03-29 16:39:46 | → | codygman__ joins (~user@209.251.131.98) |
| 2021-03-29 16:40:52 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Disconnected: Replaced by new connection") |
| 2021-03-29 16:40:52 | × | ph88^ quits (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2021-03-29 16:40:57 | <dolio> | That description isn't real numbers, just like the other description wasn't natural numbers. |
| 2021-03-29 16:41:02 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-03-29 16:41:14 | × | z0k quits (~user@115.186.169.1) (Quit: WeeChat 3.0) |
| 2021-03-29 16:41:15 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-03-29 16:41:21 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-29 16:41:57 | <dolio> | Also the usual ordering on the reals doesn't have a bottom to be a domain. |
| 2021-03-29 16:42:20 | → | ubert joins (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de) |
| 2021-03-29 16:42:58 | <dolio> | It's also not directed complete, I think. |
| 2021-03-29 16:43:18 | <Gurkenglas> | dolio, yeah add -inf and inf |
All times are in UTC.