Logs on 2023-12-12 (liberachat/#haskell)
| 00:04:01 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 00:06:04 | × | mosul quits (~mosul@user/mosul) (Quit: leaving) |
| 00:13:18 | → | mosul joins (mosul@user/mosul) |
| 00:15:07 | johnw_ | is now known as johnw |
| 00:16:12 | → | RedFlamingos joins (~RedFlamin@user/RedFlamingos) |
| 00:27:27 | <monochrom> | Here may be a clearer example. You have a correspondence between "data Foo a = Unit a | Foo Req (Rsp -> Foo a)" (so Foo :: (Rsp -> Foo a) -> (Req -> Foo a)) and "class MonadFoo f where foo :: Req -> f Rsp". |
| 00:35:45 | <monochrom> | Joao003: You may like: https://link.springer.com/chapter/10.1007/978-3-662-54434-1_21 "APLicative Programming with Naperian Functors" (it explains APL by (->)r and Traversable). It also has a PDF version. |
| 00:37:03 | <Joao003> | i was just contemplating the usefulness of (->)r as a monad |
| 00:37:15 | → | juri__ joins (~juri@79.140.117.100) |
| 00:39:10 | <monochrom> | Well yeah, APL is the epitome of pointfree programming, so it is quite deep that APL can be explained by (->)r and a Traversable assumption. That will cover your pointfree interest for a long way. |
| 00:40:18 | <Joao003> | (->) r is the function type, right? |
| 00:40:30 | <monochrom> | Yes. |
| 00:40:41 | <glguy> | If you're in the market for a current language in this space I came upon someone solving AoC in Uiua https://aoc2023.jonathanperret.net/ |
| 00:40:50 | × | juri_ quits (~juri@79.140.117.38) (Ping timeout: 268 seconds) |
| 00:42:14 | <monochrom> | Ugh that's Egyptian :D |
| 00:43:05 | <monochrom> | One might say: Ra himself writes like this for functional programming :) |
| 00:43:49 | → | mud joins (~mud@user/kadoban) |
| 00:44:28 | <Joao003> | CURSE OF RA *hieroglyph spam* |
| 00:47:07 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 00:55:12 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-39e5-e6a4-25fc-cb4b.rev.sfr.net) (Remote host closed the connection) |
| 00:56:59 | → | alexherbo2 joins (~alexherbo@2a02-8440-3341-aec3-bd61-c6f5-4a7d-43f0.rev.sfr.net) |
| 01:01:11 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 01:05:29 | × | mud quits (~mud@user/kadoban) (Quit: quit) |
| 01:08:36 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 01:16:06 | × | not_reserved quits (~not_reser@185.202.220.251) (Quit: Client closed) |
| 01:19:35 | → | emmanuelux_ joins (~emmanuelu@user/emmanuelux) |
| 01:21:14 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Ping timeout: 256 seconds) |
| 01:30:22 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds) |
| 01:36:35 | → | leungbk joins (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) |
| 01:37:46 | × | alexherbo2 quits (~alexherbo@2a02-8440-3341-aec3-bd61-c6f5-4a7d-43f0.rev.sfr.net) (Remote host closed the connection) |
| 01:42:12 | × | machinedgod quits (~machinedg@93-136-135-211.adsl.net.t-com.hr) (Ping timeout: 256 seconds) |
| 01:47:13 | → | trev joins (~trev@user/trev) |
| 01:51:49 | × | trev quits (~trev@user/trev) (Client Quit) |
| 01:52:04 | × | xff0x quits (~xff0x@ai085147.d.east.v6connect.net) (Ping timeout: 255 seconds) |
| 01:55:24 | × | leungbk quits (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) (Quit: ERC 5.6-git (IRC client for GNU Emacs 30.0.50)) |
| 01:55:48 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 02:00:21 | × | Joao003 quits (~Joao003@190.108.99.230) (Quit: Bye!) |
| 02:03:02 | → | not_reserved joins (~not_reser@185.202.220.251) |
| 02:12:23 | → | tornato joins (uid197568@id-197568.tinside.irccloud.com) |
| 02:21:43 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 240 seconds) |
| 02:22:20 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 02:23:23 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 264 seconds) |
| 02:26:37 | <EvanR> | monochrom, (->) r, aka the dependency injection functor! |
| 02:27:44 | → | leungbk joins (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) |
| 02:27:47 | → | jespada joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 02:33:15 | × | not_reserved quits (~not_reser@185.202.220.251) (Quit: Client closed) |
| 02:33:56 | → | not_reserved joins (~not_reser@185.202.220.251) |
| 02:37:21 | × | fryguybob quits (~fryguybob@cpe-24-94-50-22.stny.res.rr.com) (Quit: leaving) |
| 02:39:34 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 02:40:58 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 02:41:29 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:41:39 | × | leungbk quits (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) (Quit: ERC 5.6-git (IRC client for GNU Emacs 30.0.50)) |
| 02:41:41 | <brettgilio> | :) |
| 02:42:01 | <brettgilio> | test |
| 02:42:39 | <brettgilio> | test |
| 02:42:58 | <geekosaur> | hello |
| 02:43:01 | <brettgilio> | sorry |
| 02:43:07 | <brettgilio> | my irssi client frame was being unusual |
| 02:43:39 | → | leungbk joins (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) |
| 02:44:12 | × | leungbk quits (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) (Remote host closed the connection) |
| 02:45:36 | × | tabemann quits (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Quit: Leaving) |
| 02:45:55 | <monochrom> | EvanR: Haha that's a great name |
| 02:46:37 | → | leungbk joins (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) |
| 02:46:47 | → | trev joins (~trev@user/trev) |
| 02:47:43 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 240 seconds) |
| 02:48:07 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 02:50:37 | <albet70> | rrtype :: !TYPE what this ! mean? |
| 02:52:47 | <monochrom> | Strict fields in a record. https://www.vex.net/~trebla/haskell/strict-field.xhtml |
| 02:53:12 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 02:56:59 | → | tabemann joins (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 02:57:36 | <albet70> | rrtype :: ResourceRecord -> !TYPE from Network.DNS.Types, how I can construct a TYPE? since 'pattern' isn't defined |
| 02:58:00 | <monochrom> | Oh that, then sorry, I don't know. |
| 02:58:47 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 264 seconds) |
| 02:59:43 | <int-e> | EvanR: would that make Const the dependency rejection functor? |
| 03:00:08 | <geekosaur> | albet70, "pattern" there means it's a pattern synonym |
| 03:01:26 | <albet70> | this one https://hackage.haskell.org/package/dns-4.2.0/docs/Network-DNS-Types.html#t:TYPE |
| 03:01:28 | <geekosaur> | so there are pattern synonyms for the most common RR types, and toTYPE can be used to construct others given the RR number |
| 03:01:30 | <geekosaur> | yes |
| 03:02:45 | <albet70> | geekosaur , I want to use ‘rrtype’ to get the record type, like CNAME, A, AAAA, how I can filter AAAA? |
| 03:04:13 | <geekosaur> | presumably a field pattern match (foo ResourceRecord{rrtype = AAAA} = …) |
| 03:05:27 | <albet70> | AAAA is normal vaule in haskell? |
| 03:05:41 | <geekosaur> | the patterns act as values, so you can refer to AAAA in your code instead of having to use 28 |
| 03:05:50 | <geekosaur> | it's a pattern synonym |
| 03:06:05 | <geekosaur> | so it behaves as a normal value |
| 03:07:09 | <geekosaur> | (bidirectional pattern synonym) |
| 03:08:21 | <monochrom> | You read find pattern synonyms in the GHC User's Guide. It has examples. |
| 03:08:32 | <geekosaur> | https://downloads.haskell.org/ghc/9.6.1/docs/users_guide/exts/pattern_synonyms.html |
| 03:09:40 | → | dwt__ joins (~dwt_@2601:2c6:8381:e5c:186c:2b2e:4114:8cc0) |
| 03:11:11 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 245 seconds) |
| 03:12:37 | × | dwt_ quits (~dwt_@2601:2c6:8381:e5c:c917:e876:d8ba:f05f) (Ping timeout: 246 seconds) |
| 03:13:08 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 03:24:11 | <albet70> | difference with ‘type’? |
| 03:24:26 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 03:28:38 | <albet70> | sorry, I still don’t get it, why it doesn’t use a number? like 1 for CNAME, 2 for A, 3 for AAAA etc |
| 03:29:14 | <albet70> | so I know it’s a Int, so I can use == to check it’s a A or AAAA |
| 03:29:23 | × | td_ quits (~td@i5387090E.versanet.de) (Ping timeout: 264 seconds) |
| 03:30:42 | → | td_ joins (~td@i53870905.versanet.de) |
| 03:35:55 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 03:36:02 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 03:36:48 | <geekosaur> | it's not a number, it's a `data` with a smart constructor (toTYPE) for numbers and pattern synonyms for the most common rrtypes |
| 03:37:12 | × | edr quits (~edr@user/edr) (Quit: Leaving) |
| 03:38:21 | <geekosaur> | (in fact the haddock says it's a GADT: "data TYPE where") |
| 03:38:33 | <geekosaur> | sadly it doesn't have links to the source |
| 03:38:55 | <albet70> | yes,no links on the hackage |
| 03:39:15 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
| 03:39:30 | → | eggplantade joins (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) |
| 03:40:01 | <geekosaur> | and the reason it doesn't simply use a number is you can't have uppercase variables for the common ones like A |
| 03:40:18 | <geekosaur> | it'd have to be something like `rr_A = 1` |
| 03:41:22 | <geekosaur> | pattern synonyms let you make custom "constructors" |
| 03:41:46 | <EvanR> | pattern matching is cooler than if number ==... else if... else if ... |
| 03:41:50 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 03:42:16 | <geekosaur> | and who wants to use 28 instead of AAAA? |
| 03:42:47 | <EvanR> | even C avoids it by using defined constants and switch |
| 03:43:04 | <geekosaur> | or enums |
| 03:43:38 | <geekosaur> | but with C enums you can specify values and skip them when needed; Haskell Enum isn't quite that flexible |
| 03:44:38 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 03:44:40 | <geekosaur> | also you can add your own patterns (note "Bundled Patterns") for rrtypes they don't provide; you can't extend either a C or Haskell enum that way |
| 03:45:36 | <EvanR> | you can customize the numeric mapping with Enum but it's a pain in the ass |
| 03:46:01 | <albet70> | can I think “pattern synonym “ as “data alias”? |
| 03:46:40 | <geekosaur> | sort of |
| 03:46:46 | <c_wraith> | they can be, but they can be a lot more sophisticated. |
| 03:47:20 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 03:52:18 | → | rosco joins (~rosco@175.136.152.56) |
| 03:57:28 | <albet70> | pattern synonym is like C’s macro? |
| 03:58:22 | <geekosaur> | mm, I wouldn't really say that, since (a) it is typesafe (b) it can do more than a macro can |
| 03:58:31 | <geekosaur> | not that its power is really being used here |
| 03:59:09 | <albet70> | geekosaur , do more than lisp’s macro can? |
| 03:59:17 | <c_wraith> | Pattern synonyms can be used *as patterns* |
| 03:59:51 | <geekosaur> | but they can be used to execute arbitrary code (with type safety) |
| 04:00:03 | <c_wraith> | They aren't, as they don't correspond to constructors for the type |
| 04:00:14 | <int-e> | Lisp macros are an entirely different beast. Template Haskell ventures into that territory. |
| 04:00:27 | <c_wraith> | But you can use them to construct values of the type or to pattern-match and extract arguments from a value |
| 04:00:33 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 04:00:33 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 04:00:33 | finn_elija | is now known as FinnElija |
| 04:01:04 | <c_wraith> | I have made some very silly pattern synonyms just to stretch the system out. |
| 04:03:48 | <c_wraith> | https://paste.tomsmeding.com/D9pR2DBP Very silly. Don't do this. |
| 04:03:55 | × | cods quits (~fred@tuxee.net) (Ping timeout: 255 seconds) |
| 04:04:38 | × | analoq quits (~yashi@user/dies) (Ping timeout: 268 seconds) |
| 04:04:54 | <c_wraith> | also, this TypeAbstractions thing is new to me... |
| 04:08:26 | <c_wraith> | Ok, I read the docs and that's great, but... couldn't we just shoehorn a few more things into ScopedTypeVariables instead? |
| 04:18:43 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 04:18:52 | <albet70> | back to the question, how I can filter AAAA in TYPE? |
| 04:19:24 | → | euleritian joins (~euleritia@dynamic-046-114-202-232.46.114.pool.telefonica.de) |
| 04:20:23 | <albet70> | data TYPE where pattern A :: TYPE, there’s no pattern A =? |
| 04:21:03 | → | cods joins (~fred@tuxee.net) |
| 04:21:05 | → | analoq joins (~yashi@user/dies) |
| 04:26:42 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:36:06 | × | SanchayanMaity quits (sid478177@id-478177.hampstead.irccloud.com) () |
| 04:36:23 | → | SanchayanMaity joins (sid478177@id-478177.hampstead.irccloud.com) |
| 04:39:14 | × | aforemny_ quits (~aforemny@2001:9e8:6cdd:be00:6f70:eeee:fde4:e2c7) (Ping timeout: 260 seconds) |
| 04:39:14 | → | aforemny joins (~aforemny@2001:9e8:6cc3:3a00:a23:6c46:4b53:30b) |
| 04:39:25 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 04:41:57 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Read error: Connection reset by peer) |
| 04:47:37 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 04:47:57 | → | trev joins (~trev@user/trev) |
| 04:52:51 | × | euleritian quits (~euleritia@dynamic-046-114-202-232.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 04:53:09 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 05:00:10 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 05:00:52 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 05:02:09 | × | tornato quits (uid197568@id-197568.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 05:02:48 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 05:03:53 | × | [_] quits (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 256 seconds) |
| 05:06:36 | → | tri_ joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 05:09:32 | <tri_> | testing from limechat |
| 05:10:49 | → | thegeekinside joins (~thegeekin@189.217.90.224) |
| 05:10:53 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 05:11:23 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 05:13:29 | × | phma quits (~phma@host-67-44-208-181.hnremote.net) (Read error: Connection reset by peer) |
| 05:14:31 | → | phma joins (~phma@2001:5b0:215d:e438:647:90bc:42bc:c98) |
| 05:19:05 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 05:32:13 | × | arkoinad quits (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) (Ping timeout: 256 seconds) |
| 05:40:11 | × | rosco quits (~rosco@175.136.152.56) (Quit: Lost terminal) |
| 05:43:38 | × | thegeekinside quits (~thegeekin@189.217.90.224) (Remote host closed the connection) |
| 05:44:12 | → | alp_ joins (~alp@2001:861:e3d6:8f80:873a:e9b8:5ec5:8a14) |
| 05:47:01 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 05:47:44 | × | mikess quits (~sam@user/mikess) (Quit: leaving) |
| 05:47:58 | → | euleritian joins (~euleritia@dynamic-089-015-236-089.89.15.236.pool.telefonica.de) |
| 05:48:01 | → | mikess joins (~sam@user/mikess) |
| 05:50:24 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 05:54:20 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 05:59:13 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 05:59:13 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 05:59:13 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 05:59:13 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 05:59:13 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Remote host closed the connection) |
| 05:59:13 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 05:59:38 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 05:59:40 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 05:59:41 | → | califax joins (~califax@user/califx) |
| 05:59:49 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 05:59:52 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 06:00:16 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 06:01:15 | × | stiell quits (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 06:01:40 | → | stiell joins (~stiell@gateway/tor-sasl/stiell) |
| 06:02:04 | × | td_ quits (~td@i53870905.versanet.de) (Ping timeout: 276 seconds) |
| 06:03:03 | × | echoreply quits (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
| 06:03:20 | → | td_ joins (~td@i53870924.versanet.de) |
| 06:03:51 | → | zetef joins (~quassel@95.77.17.251) |
| 06:03:55 | × | zetef quits (~quassel@95.77.17.251) (Remote host closed the connection) |
| 06:03:56 | → | echoreply joins (~echoreply@45.32.163.16) |
| 06:04:36 | → | zetef joins (~quassel@95.77.17.251) |
| 06:05:31 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 06:05:36 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:07:03 | → | igemnace joins (~ian@user/igemnace) |
| 06:08:00 | <iqubic> | tri_: I can see that message. |
| 06:09:52 | → | rosco joins (~rosco@175.136.152.56) |
| 06:11:03 | → | johnw joins (~johnw@69.62.242.138) |
| 06:16:33 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 06:17:44 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:34:34 | × | bilegeek quits (~bilegeek@2600:1008:b08b:7355:7869:26c7:cf9e:bac4) (Quit: Leaving) |
| 06:36:32 | → | Maeda joins (~Maeda@91-161-10-149.subs.proxad.net) |
| 06:36:47 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 06:37:20 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 06:38:44 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 06:44:59 | → | araujo joins (~araujo@45.146.54.110) |
| 06:48:47 | × | iqubic quits (~avi@2601:602:9502:c70:5de0:aac0:2bec:3df) (Read error: Connection reset by peer) |
| 06:54:58 | → | arkoinad joins (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) |
| 06:56:03 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 06:56:40 | × | analoq quits (~yashi@user/dies) (Ping timeout: 276 seconds) |
| 06:57:48 | → | analoq joins (~yashi@user/dies) |
| 06:59:37 | × | tri_ quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 07:00:47 | → | tri_ joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 07:01:06 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 07:02:07 | × | tri_ quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 07:02:19 | → | tri_ joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 07:03:16 | → | iqubic joins (~avi@2601:602:9502:c70:589:c039:227d:3881) |
| 07:04:31 | × | bliminse quits (~bliminse@user/bliminse) (Quit: leaving) |
| 07:15:30 | × | tri_ quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 07:16:14 | <ski> | @remember EvanR <EvanR> (->) r, aka the dependency injection functor! <int-e> EvanR: would that make Const the dependency rejection functor? |
| 07:16:14 | <lambdabot> | Nice! |
| 07:16:22 | <ski> | c_wraith : hah ! |
| 07:16:24 | <ski> | c_wraith : "couldn't we just shoehorn a few more things into ScopedTypeVariables instead?" -- how ? |
| 07:16:51 | <ski> | albet70 : filter how ? from a list of `TYPE's ? |
| 07:17:23 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:18:21 | → | bliminse joins (~bliminse@user/bliminse) |
| 07:20:04 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 276 seconds) |
| 07:21:15 | × | skyres_ quits (~skyres@176.254.244.83) (Ping timeout: 252 seconds) |
| 07:25:22 | × | farn_ quits (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505) (Ping timeout: 268 seconds) |
| 07:34:47 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 264 seconds) |
| 07:36:04 | → | hsw_ joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 07:36:27 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 07:37:44 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:37:45 | × | hsw quits (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) (Read error: Connection reset by peer) |
| 07:38:04 | → | farn_ joins (~farn@2a03:4000:7:3cd:d4ab:85ff:feeb:f505) |
| 07:42:05 | × | arkoinad quits (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 07:43:40 | → | yeiskomp joins (~yeiskomp@176.254.244.83) |
| 07:47:15 | → | acidjnk_new joins (~acidjnk@p200300d6e72b9347b4dc018a2c6658c2.dip0.t-ipconnect.de) |
| 07:48:18 | × | euleritian quits (~euleritia@dynamic-089-015-236-089.89.15.236.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:48:36 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:50:53 | → | akegalj joins (~akegalj@78-0-45-228.adsl.net.t-com.hr) |
| 07:51:33 | → | falafel joins (~falafel@76.red-79-153-68.dynamicip.rima-tde.net) |
| 07:51:52 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:57:07 | × | falafel quits (~falafel@76.red-79-153-68.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 08:01:02 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 08:04:57 | → | zetef joins (~quassel@95.77.17.251) |
| 08:08:04 | → | fendor joins (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) |
| 08:10:28 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Remote host closed the connection) |
| 08:10:44 | → | adanwan joins (~adanwan@gateway/tor-sasl/adanwan) |
| 08:20:31 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 240 seconds) |
| 08:22:02 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 08:24:12 | → | zetef_ joins (~quassel@95.77.17.251) |
| 08:26:23 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 08:26:51 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 08:26:53 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 256 seconds) |
| 08:30:37 | → | chele joins (~chele@user/chele) |
| 08:31:13 | × | Square2 quits (~Square4@user/square) (Ping timeout: 255 seconds) |
| 08:35:08 | → | danza joins (~danza@151.43.125.100) |
| 08:36:10 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 08:37:34 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 08:41:16 | × | rosco quits (~rosco@175.136.152.56) (Quit: Lost terminal) |
| 08:45:24 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 08:49:51 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 08:56:34 | × | mc47 quits (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 08:58:42 | × | akegalj quits (~akegalj@78-0-45-228.adsl.net.t-com.hr) (Ping timeout: 260 seconds) |
| 09:00:01 | × | danza quits (~danza@151.43.125.100) (Ping timeout: 268 seconds) |
| 09:11:52 | × | not_reserved quits (~not_reser@185.202.220.251) (Quit: Client closed) |
| 09:12:42 | × | shriekingnoise quits (~shrieking@186.137.175.87) (Ping timeout: 260 seconds) |
| 09:13:48 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:14:58 | → | dhil joins (~dhil@2001:8e0:2014:3100:a3e7:9e7e:94ec:9684) |
| 09:16:44 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 09:19:01 | × | eggplantade quits (~Eggplanta@104-55-37-220.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 09:20:06 | × | Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:20:11 | <albet70> | ski , I use fromTYPE turn TYPE into word16 and filter it |
| 09:21:11 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 245 seconds) |
| 09:21:18 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:22:58 | <ski> | filter, how ? |
| 09:24:14 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:25:05 | × | jargon quits (~jargon@32.sub-174-238-226.myvzw.com) (Remote host closed the connection) |
| 09:25:07 | <albet70> | let rrtn = fmap (\a -> fromTYPE $ rrtype a) $ answer (_r :: DNSMessage) |
| 09:25:14 | <albet70> | if elem (28 :: Word16) rrtn then |
| 09:28:06 | <ski> | what about AAAA `elem` rrtn if you skip the `fromTYPE' part ? |
| 09:29:55 | <albet70> | AAAA isn't defined? I haven't tried that, but in ghci, AAAA is not defined |
| 09:33:21 | → | danse-nr3 joins (~danse@an-19-163-233.service.infuturo.it) |
| 09:33:47 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 09:35:04 | → | CiaoSen joins (~Jura@2a05:5800:283:9300:ca4b:d6ff:fec1:99da) |
| 09:35:04 | <albet70> | ski , yes, you're right, A can be A elem rrtn |
| 09:38:03 | × | tzh quits (~tzh@c-71-193-181-0.hsd1.or.comcast.net) (Quit: zzz) |
| 09:38:09 | × | qqq quits (~qqq@92.43.167.61) (Ping timeout: 256 seconds) |
| 09:42:06 | × | ft quits (~ft@p3e9bc784.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:45:06 | → | coot joins (~coot@89-69-206-216.dynamic.chello.pl) |
| 09:47:35 | <ski> | albet70 : surround with backticks, to use it as an infix operator |
| 09:50:34 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
| 09:50:40 | → | qqq joins (~qqq@92.43.167.61) |
| 09:51:05 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 09:52:03 | → | cfricke joins (~cfricke@user/cfricke) |
| 09:55:03 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Ping timeout: 260 seconds) |
| 10:00:14 | × | phma quits (~phma@2001:5b0:215d:e438:647:90bc:42bc:c98) (Read error: Connection reset by peer) |
| 10:01:07 | → | phma joins (phma@2001:5b0:211c:d228:5342:e754:aa9:bcd5) |
| 10:01:23 | × | td_ quits (~td@i53870924.versanet.de) (Ping timeout: 256 seconds) |
| 10:01:27 | <ski> | "AAAA isn't defined? I haven't tried that, but in ghci, AAAA is not defined" -- oh, missed this. i guess you didn't import `Network.DNS.Types' in the interactor ? |
| 10:03:13 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 10:03:23 | → | td_ joins (~td@i5387090E.versanet.de) |
| 10:03:47 | × | alp_ quits (~alp@2001:861:e3d6:8f80:873a:e9b8:5ec5:8a14) (Remote host closed the connection) |
| 10:04:34 | × | zetef_ quits (~quassel@95.77.17.251) (Ping timeout: 260 seconds) |
| 10:06:21 | → | alp_ joins (~alp@2001:861:e3d6:8f80:b08a:7a72:bc6f:b2a9) |
| 10:12:17 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 10:13:55 | → | califax joins (~califax@user/califx) |
| 10:14:07 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Client Quit) |
| 10:19:14 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 10:19:56 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds) |
| 10:20:17 | → | zetef joins (~quassel@95.77.17.251) |
| 10:22:11 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:27:36 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 10:33:10 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 255 seconds) |
| 10:35:16 | <albet70> | yes, I didn't |
| 10:38:31 | → | califax joins (~califax@user/califx) |
| 10:40:08 | → | __monty__ joins (~toonn@user/toonn) |
| 10:40:26 | → | akegalj joins (~akegalj@89-164-125-9.dsl.iskon.hr) |
| 10:40:28 | <ski> | (you could always reexport that module from your module, i guess) |
| 10:44:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:45:03 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 10:45:34 | × | CiaoSen quits (~Jura@2a05:5800:283:9300:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 10:46:11 | → | califax joins (~califax@user/califx) |
| 10:47:13 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:6831:b374:3227:de58) |
| 10:51:21 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) |
| 10:54:47 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 10:55:50 | → | califax joins (~califax@user/califx) |
| 10:57:18 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:57:35 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 10:58:01 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 11:03:01 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 276 seconds) |
| 11:05:10 | <ski> | @botslack |
| 11:05:11 | <lambdabot> | :) |
| 11:05:26 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 11:05:38 | ski | looks at tri |
| 11:06:12 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 252 seconds) |
| 11:09:17 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 11:10:03 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 11:10:49 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 276 seconds) |
| 11:18:16 | × | mikess quits (~sam@user/mikess) (Ping timeout: 245 seconds) |
| 11:36:30 | × | alp_ quits (~alp@2001:861:e3d6:8f80:b08a:7a72:bc6f:b2a9) (Ping timeout: 260 seconds) |
| 11:36:31 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 240 seconds) |
| 11:37:27 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 11:39:09 | × | mzg quits (mzg@lazy.unconscious.biz) (Quit: leaving) |
| 11:41:22 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 11:50:54 | × | dhil quits (~dhil@2001:8e0:2014:3100:a3e7:9e7e:94ec:9684) (Ping timeout: 260 seconds) |
| 11:52:14 | → | arahael_ joins (~arahael@103.246.103.99) |
| 11:52:18 | → | euleritian joins (~euleritia@dynamic-046-114-192-005.46.114.pool.telefonica.de) |
| 11:54:01 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 12:01:08 | × | euleritian quits (~euleritia@dynamic-046-114-192-005.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 12:01:26 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 12:06:43 | → | mzg joins (mzg@lazy.unconscious.biz) |
| 12:08:43 | → | Joao003 joins (~Joao003@190.108.99.230) |
| 12:16:35 | × | danse-nr3 quits (~danse@an-19-163-233.service.infuturo.it) (Read error: Connection reset by peer) |
| 12:19:53 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 12:21:46 | × | sawilagar quits (~sawilagar@user/sawilagar) (Read error: Connection reset by peer) |
| 12:23:02 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 12:25:52 | → | machinedgod joins (~machinedg@93-138-57-84.adsl.net.t-com.hr) |
| 12:25:55 | × | sawilagar quits (~sawilagar@user/sawilagar) (Client Quit) |
| 12:30:46 | × | arahael_ quits (~arahael@103.246.103.99) (Ping timeout: 245 seconds) |
| 12:33:02 | → | danse-nr3 joins (~danse@151.57.235.147) |
| 12:42:54 | → | alp_ joins (~alp@2001:861:e3d6:8f80:5f2a:e7a9:cfa0:1d79) |
| 12:48:01 | → | CiaoSen joins (~Jura@2a05:5800:283:9300:ca4b:d6ff:fec1:99da) |
| 12:48:26 | → | abrantesasf joins (~abrantesa@177.154.20.2) |
| 12:49:19 | × | abrantesasf quits (~abrantesa@177.154.20.2) (Remote host closed the connection) |
| 12:51:39 | → | abrantesasf joins (~abrantesa@177.154.20.2) |
| 12:54:37 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 12:56:16 | × | machinedgod quits (~machinedg@93-138-57-84.adsl.net.t-com.hr) (Ping timeout: 255 seconds) |
| 12:57:19 | × | trev quits (~trev@user/trev) (Read error: Connection reset by peer) |
| 12:57:26 | → | tr_ev joins (~trev@user/trev) |
| 13:02:47 | tr_ev | is now known as trev |
| 13:07:47 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Ping timeout: 264 seconds) |
| 13:10:11 | <albet70> | ski , I saw that about pattern synonym link, but I still don't get it, what's the benefit? |
| 13:11:11 | <ski> | benefit is that you don't have to remember magic numbers (and you can't use an incorrect one by mistake/intent) |
| 13:11:46 | <albet70> | ski , but that C's macro do the same thing |
| 13:12:07 | → | edr joins (~edr@user/edr) |
| 13:12:28 | <albet70> | like #define PI 3.1415 |
| 13:14:03 | → | zetef joins (~quassel@95.77.17.251) |
| 13:15:02 | <ski> | yes, but that's not an abstract data type |
| 13:17:31 | <ski> | (not even a separate data type at all, as `enum TYPE {A = 1,NS,MD,...};' would be) |
| 13:18:35 | <albet70> | do you have a good example? |
| 13:18:36 | ski | idly imagines a pragma for setting individual constructors values for `deriving Enum' |
| 13:21:15 | → | alexherbo2 joins (~alexherbo@2a02-8440-3240-ce99-dd22-abb7-bd07-cd6f.rev.sfr.net) |
| 13:21:31 | <ski> | well, e.g. <https://en.wikipedia.org/wiki/List_of_DNS_record_types#Obsolete_record_types> says `MD' is obsolete. and <https://hackage.haskell.org/package/dns-4.2.0/docs/Network-DNS-Types.html#t:TYPE> does not list it. so you can't use `3' in your code (for `MD'), because `TYPE' is not a synonym for a numeric type (nor is it an instance of `Num', so no implicit `fromInteger' being used) |
| 13:25:31 | → | xff0x joins (~xff0x@ai085147.d.east.v6connect.net) |
| 13:27:53 | <albet70> | ski , data TYPE where pattern A :: TYPE; f :: TYPE -> TYPE f A is ok? |
| 13:29:00 | <ski> | (hm, come to think of it, i guess a numeric literal like `0' acts more or less as if `pattern 0 :: (Num a,Eq a) => a; pattern 0 <- ((fromInteger 0 ==) -> True) where 0 = fromInteger 0' .. except when used as an expression, there's no `Eq a' constraint .. i sometimes would like to be able to specify some extra constraints for the pattern form of a pattern synonym, without having them on the expression form. |
| 13:29:06 | <ski> | probably would be nice to also be able to have some on the expression form that're not in the pattern form) |
| 13:29:32 | <ski> | albet70 : where did this `f' come from ? |
| 13:29:52 | <ski> | is it just any function on `TYPE's ? |
| 13:30:22 | <ski> | if so, then yes (but you'd not write `pattern' there, in a GADT-style (`GADGTSyntax') `data' type definition) |
| 13:30:51 | <albet70> | I like ADT, |
| 13:31:00 | <albet70> | GADT make me confused sometimes |
| 13:31:07 | <ski> | (Algebraic Data Types or Abstract Data Types ?) |
| 13:31:21 | <albet70> | Algebraic Data Types |
| 13:31:22 | <ski> | well, in this case, it's not really using any actual extra GADT powers |
| 13:31:36 | <albet70> | it uses "where" |
| 13:31:46 | <ski> | (well, perhaps the implementation in the library is .. haven't seen the source) |
| 13:31:57 | <albet70> | yes, no source |
| 13:32:00 | <ski> | maybe that's just an artefact of the Haddock |
| 13:34:35 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:37:01 | × | darchitect quits (~darchitec@2a00:23c6:3584:df01:4cbc:8ff2:73ae:d845) (Ping timeout: 246 seconds) |
| 13:39:12 | → | darchitect joins (~darchitec@2a00:23c6:3584:df01:fea4:c282:f8d:5ecc) |
| 13:40:33 | <albet70> | ski , where I can find the data TYPE's source code since it's not on hackage? |
| 13:40:55 | <albet70> | I install that package on cabal, where cabal install it? |
| 13:41:18 | <ski> | <https://hackage.haskell.org/package/dns-4.2.0/dns-4.2.0.tar.gz>, linked from <https://hackage.haskell.org/package/dns>, i suppose |
| 13:41:45 | <albet70> | do you know where cabal install the package on ? I mean local path on linux |
| 13:41:51 | <ski> | oh, it has <https://hackage.haskell.org/package/dns-4.2.0/src/>, too |
| 13:42:34 | <ski> | <https://hackage.haskell.org/package/dns-4.2.0/src/internal/Network/DNS/Types/Internal.hs> has `TYPE', and it's implemented as a `newtype' (not GADT) |
| 13:43:21 | <albet70> | newtype TYPE = TYPE { -- | From type to number.fromTYPE :: Word16 } deriving (E |
| 13:43:22 | <ski> | .. and i notice the `Show TYPE' instance is (slightly) incorrect |
| 13:44:15 | <ski> | (it doesn't matter for the first cases, but the last case ought to be defined using `showsPrec', which would force the previous ones to use that as well) |
| 13:44:20 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 13:45:09 | <albet70> | newtype TYPE = TYPE { fromTYPE :: Word16 } |
| 13:45:19 | <albet70> | pattern A :: TYPE |
| 13:45:22 | <ski> | (because it ought to say `showsPrec p x = showParen (p > 10) $ showString "TYPE " . showsPrec 11 (fromTYPE x)') |
| 13:45:30 | <albet70> | pattern A = TYPE 1 |
| 13:45:34 | <ski> | (.. also missing a space, apparently) |
| 13:46:13 | <albet70> | where you use A , actually it's TYPE 1, still C's macro to me |
| 13:46:34 | <ski> | yes, but `TYPE' is exported abstractly, so you can't reach into the innards from outside |
| 13:48:09 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 13:48:10 | × | araujo quits (~araujo@45.146.54.110) (Read error: Connection reset by peer) |
| 13:48:37 | × | darchitect quits (~darchitec@2a00:23c6:3584:df01:fea4:c282:f8d:5ecc) (Ping timeout: 256 seconds) |
| 13:48:51 | <ski> | well, i guess `fromType' and `toType' are exported |
| 13:49:22 | <ski> | albet70 : still, you get additional type safety, by not being able to screw up the magic numbers by mistake |
| 13:49:25 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 276 seconds) |
| 13:49:39 | → | araujo joins (~araujo@216.73.163.162) |
| 13:49:56 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 13:50:17 | → | euleritian joins (~euleritia@dynamic-046-114-192-005.46.114.pool.telefonica.de) |
| 13:50:25 | <albet70> | how "define PI 3.1415" would screw up the magic numbers by mistake? |
| 13:50:25 | <ski> | (so, i guess that `showsPrec' defining equation ought to say `toTYPE' instead of `TYPE' in that `String's, then) |
| 13:50:33 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 13:51:03 | → | califax joins (~califax@user/califx) |
| 13:51:14 | <ski> | albet70 : because now wherever you could type `PI', you could just as well type `3.1415' or `3.1415926' or `3.1416' or `2.718281828' or `496' or .. |
| 13:51:52 | <ski> | with a `newtype', that doesn't happen (since there is no `Num' instance) |
| 13:52:50 | → | darchitect joins (~darchitec@host86-191-124-92.range86-191.btcentralplus.com) |
| 14:03:41 | × | abrantesasf quits (~abrantesa@177.154.20.2) (Remote host closed the connection) |
| 14:03:43 | × | CiaoSen quits (~Jura@2a05:5800:283:9300:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 14:04:55 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 14:05:24 | → | igemnace joins (~ian@user/igemnace) |
| 14:07:13 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 14:08:00 | → | shriekingnoise joins (~shrieking@186.137.175.87) |
| 14:20:23 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 264 seconds) |
| 14:25:56 | → | rosco_ joins (~rosco@175.136.152.56) |
| 14:26:50 | × | rosco_ quits (~rosco@175.136.152.56) (Client Quit) |
| 14:27:53 | → | rosco_ joins (~rosco@175.136.152.56) |
| 14:32:07 | × | danse-nr3 quits (~danse@151.57.235.147) (Ping timeout: 255 seconds) |
| 14:34:52 | × | rosco_ quits (~rosco@175.136.152.56) (Quit: Lost terminal) |
| 14:36:04 | → | rosco_ joins (~rosco@175.136.152.56) |
| 14:36:14 | × | rosco_ quits (~rosco@175.136.152.56) (Client Quit) |
| 14:40:45 | → | rosco joins (~rosco@2001:e68:5411:21b:709e:ff04:8b05:a76c) |
| 14:42:29 | → | danza joins (~danza@151.57.235.147) |
| 14:51:03 | × | rosco quits (~rosco@2001:e68:5411:21b:709e:ff04:8b05:a76c) (Remote host closed the connection) |
| 14:51:40 | × | koolazer quits (~koo@user/koolazer) (Read error: Connection reset by peer) |
| 14:54:58 | × | danza quits (~danza@151.57.235.147) (Ping timeout: 256 seconds) |
| 14:59:10 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 15:03:27 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 15:03:28 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 15:03:51 | × | araujo quits (~araujo@216.73.163.162) (Quit: Leaving) |
| 15:04:04 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 255 seconds) |
| 15:05:16 | → | araujo joins (~araujo@216.73.163.162) |
| 15:10:55 | → | danse-nr3 joins (~danse@151.57.235.147) |
| 15:12:39 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 15:19:22 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 15:19:42 | × | euleritian quits (~euleritia@dynamic-046-114-192-005.46.114.pool.telefonica.de) (Read error: Connection reset by peer) |
| 15:19:59 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:24:35 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 15:24:58 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 276 seconds) |
| 15:26:22 | <mosul> | 7 |
| 15:28:57 | <danse-nr3> | 6 |
| 15:29:22 | × | leungbk quits (~user@2603-8000-1201-2dd2-4813-9b76-6ca8-e97f.res6.spectrum.com) (Ping timeout: 246 seconds) |
| 15:29:48 | <mauke> | /3 |
| 15:31:58 | × | akegalj quits (~akegalj@89-164-125-9.dsl.iskon.hr) (Quit: leaving) |
| 15:32:13 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 15:32:31 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:32:47 | → | Tuplanolla joins (~Tuplanoll@91-159-68-236.elisa-laajakaista.fi) |
| 15:36:06 | × | Joao003 quits (~Joao003@190.108.99.230) (Quit: Bye!) |
| 15:36:06 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 15:37:18 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 15:40:41 | × | dwt__ quits (~dwt_@2601:2c6:8381:e5c:186c:2b2e:4114:8cc0) (Read error: Connection reset by peer) |
| 15:41:05 | → | dwt__ joins (~dwt_@2601:2c6:8381:e5c:186c:2b2e:4114:8cc0) |
| 15:42:26 | → | Pixi__ joins (~Pixi@user/pixi) |
| 15:43:21 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 15:45:38 | × | Pixi` quits (~Pixi@user/pixi) (Ping timeout: 260 seconds) |
| 15:45:50 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 15:50:48 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 15:52:51 | × | danse-nr3 quits (~danse@151.57.235.147) (Ping timeout: 245 seconds) |
| 15:55:27 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.0.5) |
| 15:55:31 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 276 seconds) |
| 15:56:24 | → | leungbk joins (~user@142-129-149-172.res.spectrum.com) |
| 15:56:42 | × | alexherbo2 quits (~alexherbo@2a02-8440-3240-ce99-dd22-abb7-bd07-cd6f.rev.sfr.net) (Remote host closed the connection) |
| 16:01:17 | × | qqq quits (~qqq@92.43.167.61) (Remote host closed the connection) |
| 16:01:52 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.1.1) |
| 16:03:36 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 16:06:20 | → | Joao003 joins (~Joao003@190.108.99.230) |
| 16:08:23 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 16:20:17 | × | zetef quits (~quassel@95.77.17.251) (Remote host closed the connection) |
| 16:20:49 | × | alp_ quits (~alp@2001:861:e3d6:8f80:5f2a:e7a9:cfa0:1d79) (Ping timeout: 246 seconds) |
| 16:27:11 | → | Square2 joins (~Square4@user/square) |
| 16:27:13 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 16:27:23 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 16:29:14 | <kaol> | I know more about JWA now than I ever wanted. JOSE is missing JWE support and I'm implementing that. |
| 16:29:28 | → | tri53 joins (~tri@4133220a.cst.lightpath.net) |
| 16:29:37 | tri53 | is now known as _tri |
| 16:34:20 | <_tri> | Hi folks, im looking into rewriting an OOP logic that keeps track of the rate of events going into a system into functional in F# (I know this is Haskell group, but the fundamental is the same). The logic is, say, maximum 3 events per 10 seconds, and will alert if the rule is breached. |
| 16:34:54 | <_tri> | my problem is, this logic inherent has internal state, that is it must know at any given time the number of events for the last 10 seconds |
| 16:35:08 | <_tri> | (a sliding window) |
| 16:35:23 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 16:35:44 | <_tri> | i can think natively in OOP because object can maintain state |
| 16:35:44 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 16:36:30 | <_tri> | but im not sure how to achieve this in FP paradigm, because the state is only changed at the edges, i.e. input and output, not kept track in the internal system, if that makes any sense |
| 16:38:39 | × | ystael quits (~ystael@user/ystael) (Read error: Connection reset by peer) |
| 16:39:15 | <Rembane> | _tri: Hi! That's an interesting problem. I think I would solve it by storing a list of timestamps, and every time another timestamp is added, the ones that are too old are removed. This makes it possible to test this subsystem without having to take time into account. |
| 16:39:47 | <kaol> | https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/values/ mutable variables are a thing in F# (and in Haskell too). |
| 16:39:52 | <Franciman> | Seems like a foldl' over a stream where the accumulator keeps the last timestamp as Rembane suggests |
| 16:40:38 | <Franciman> | wait, a question |
| 16:40:55 | <_tri> | kaol: Im kinda hesitant to dip into mutating state, that's the reason im trying to rewrite from OOP to FP :\ |
| 16:40:55 | <Franciman> | do you want to alert in real time? Or at the end of the analysis? |
| 16:41:17 | <_tri> | Franciman: yes, in realtime, this is to make sure thing doesn't spin out of control |
| 16:42:20 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 16:42:38 | <_tri> | Rembane: do you mean something similar to fold and scan? I thought about it, because these are the only constructs that can maintain state in FP, but im asking to see if there is any other |
| 16:42:53 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 16:43:03 | <Franciman> | imho a fold can do it |
| 16:43:12 | <Franciman> | and internally you print stuff, which is not pure but he |
| 16:43:15 | <Rembane> | _tri: To be totally honest, I'm thinking in terms of a GenServer that has a list of timestamps as internal state, because I've done Elixir for too long. :) |
| 16:43:51 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:444f:4a45:c596:a200) (Remote host closed the connection) |
| 16:44:07 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) |
| 16:44:18 | <kaol> | FRP is one option. Something like https://fsharpforfunandprofit.com/posts/concurrency-reactive/ (old and I have no way of telling if it's still relevant to current F#). |
| 16:44:29 | <Franciman> | i would do it with conduit or pipes |
| 16:44:31 | <Franciman> | in haskell |
| 16:44:38 | <Rembane> | _tri: So I'm having an actor that single threadedly handles the state, and the rest of the system communicates with that actor. |
| 16:45:35 | <_tri> | kaol: yes that's the route im going into too, but again, that FRP only has fold and scan to keep track of the internal state, as far as i know, so that's why im picking your brain |
| 16:45:46 | <kaol> | Or maybe something like https://medium.com/@dzoukr/event-sourcing-step-by-step-in-f-be808aa0ca18 |
| 16:46:00 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 16:46:14 | × | kimiamania46 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 16:47:35 | → | kimiamania464 joins (~65804703@user/kimiamania) |
| 16:48:39 | <_tri> | kaol: that's interesting, event sourcing never occur to me. I will take a read of that. But before I read, can you check if this statement is correct? (because i only know vaguely about event sourcing). The statement is: I would use ES to write all the events coming into my system, and read them out, separately, to check the rate? If so, then it's |
| 16:48:39 | <_tri> | not really real-time due to read/write IO right? a few seconds or a minute delay is not a problem to me btw |
| 16:49:30 | <kaol> | Pure FP pretty much takes one or more values and gives you a value and it has no concept of time. You'll pretty much need to use something else to cover the 10 seconds of events part. |
| 16:49:34 | → | zetef joins (~quassel@95.77.17.251) |
| 16:50:07 | <_tri> | Franciman: conduit and pipes sound like Reactive programming right |
| 16:50:28 | <Joao003> | % System.Cmd.system "sleep 10" |
| 16:50:30 | <yahb2> | <timeout> |
| 16:50:31 | × | slideshow6052 quits (uid629799@id-629799.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 16:50:41 | <Franciman> | in a way yes |
| 16:50:42 | <Joao003> | at least for linux |
| 16:51:12 | <_tri> | Rembane: yea, I totally admire the actor model, just that it's not native in FP to have something keep track of the state, and so i can't do it easily in F# |
| 16:51:25 | <Rembane> | _tri: Got it! |
| 16:51:52 | → | Square joins (~Square@user/square) |
| 16:52:35 | <_tri> | alright thank you everyone. You are very helpful |
| 16:52:38 | <Joao003> | _tri: yeah, like in fp you don't have variables and stuff so you need a workaround |
| 16:52:40 | × | leungbk quits (~user@142-129-149-172.res.spectrum.com) (Ping timeout: 246 seconds) |
| 16:52:50 | <_tri> | Joao003: gotcha |
| 16:54:34 | × | zetef quits (~quassel@95.77.17.251) (Remote host closed the connection) |
| 16:55:00 | <Joao003> | _tri: like, every function which wants to update that variable has to return it and then get it used later, or just use multi-threading |
| 16:55:38 | <telser> | Surely F# has something similar to a TVar? |
| 16:56:05 | × | Square2 quits (~Square4@user/square) (Ping timeout: 268 seconds) |
| 16:57:10 | <[exa]> | telser: does F# have threads or so |
| 16:57:36 | <Joao003> | telser: you just got me into f# |
| 16:58:07 | <telser> | Just as an alternate to something like conduit/pipes. |
| 16:59:11 | <_tri> | F# have mutable variable (which i guess is tvar) and threads |
| 16:59:57 | <int-e> | The "T" is for "transactional" |
| 16:59:59 | → | ystael joins (~ystael@user/ystael) |
| 17:00:10 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) (Remote host closed the connection) |
| 17:00:46 | <int-e> | There is https://fsprojects.github.io/FSharpx.Extras/reference/fsharpx-stm-core.html (which may or may not have poor performance... there's an old blog post that found it to be slow at the time: https://vaskir.blogspot.com/2013/09/stm-f-vs-haskell.html ) |
| 17:03:19 | × | pastly quits (~pastly@gateway/tor-sasl/pastly) (Ping timeout: 240 seconds) |
| 17:06:53 | → | pastly joins (~pastly@gateway/tor-sasl/pastly) |
| 17:07:42 | × | szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:10:13 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) |
| 17:11:00 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:6831:b374:3227:de58) (Quit: ubert) |
| 17:16:14 | → | dhil joins (~dhil@2001:8e0:2014:3100:fe62:84ae:2b90:5200) |
| 17:16:40 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:26:58 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 17:27:38 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:29:02 | × | igemnace quits (~ian@user/igemnace) (Remote host closed the connection) |
| 17:39:10 | → | tzh joins (~tzh@c-71-193-181-0.hsd1.or.comcast.net) |
| 17:39:37 | → | Guest16 joins (~Guest16@ec2-13-232-74-226.ap-south-1.compute.amazonaws.com) |
| 17:39:49 | × | son0p quits (~ff@181.136.122.143) (Ping timeout: 256 seconds) |
| 17:40:12 | × | Guest16 quits (~Guest16@ec2-13-232-74-226.ap-south-1.compute.amazonaws.com) (Client Quit) |
| 17:46:10 | × | fendor quits (~fendor@2a02:8388:1605:d100:267b:1353:13d7:4f0c) (Remote host closed the connection) |
| 17:46:38 | × | _tri quits (~tri@4133220a.cst.lightpath.net) (Quit: Client closed) |
| 17:47:11 | → | alp_ joins (~alp@2001:861:e3d6:8f80:afc2:f59:afac:cc18) |
| 17:55:09 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) (Remote host closed the connection) |
| 18:09:43 | → | idgaen joins (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) |
| 18:11:15 | → | machinedgod joins (~machinedg@93-138-57-84.adsl.net.t-com.hr) |
| 18:11:23 | → | danse-nr3 joins (~danse@151.37.238.206) |
| 18:11:38 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 18:12:10 | → | euleritian joins (~euleritia@dynamic-089-204-154-086.89.204.154.pool.telefonica.de) |
| 18:17:54 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 18:19:21 | → | aruns joins (~aruns@user/aruns) |
| 18:20:35 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:20:42 | × | Natch quits (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) (Remote host closed the connection) |
| 18:20:46 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 18:22:46 | × | euleritian quits (~euleritia@dynamic-089-204-154-086.89.204.154.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:23:05 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:25:04 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:26:56 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) |
| 18:26:57 | × | alp_ quits (~alp@2001:861:e3d6:8f80:afc2:f59:afac:cc18) (Remote host closed the connection) |
| 18:27:42 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 18:28:59 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 18:31:02 | → | ft joins (~ft@p3e9bc784.dip0.t-ipconnect.de) |
| 18:32:49 | → | mikess joins (~sam@user/mikess) |
| 18:33:13 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 18:33:42 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 18:33:53 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 18:34:00 | → | euleritian joins (~euleritia@dynamic-089-204-154-086.89.204.154.pool.telefonica.de) |
| 18:38:31 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 240 seconds) |
| 18:38:58 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) (Remote host closed the connection) |
| 18:48:29 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 18:49:15 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) |
| 18:51:25 | × | td_ quits (~td@i5387090E.versanet.de) (Ping timeout: 260 seconds) |
| 18:53:03 | → | alexherbo2 joins (~alexherbo@2a02-8440-3240-ce99-a4f7-9aab-90ab-68ff.rev.sfr.net) |
| 18:53:12 | → | td_ joins (~td@i53870913.versanet.de) |
| 18:53:22 | × | euleritian quits (~euleritia@dynamic-089-204-154-086.89.204.154.pool.telefonica.de) (Read error: Connection reset by peer) |
| 18:53:40 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:54:22 | → | __monty__ joins (~toonn@user/toonn) |
| 18:55:06 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 19:00:41 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 19:02:49 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:03:23 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:05:58 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 276 seconds) |
| 19:06:29 | × | danse-nr3 quits (~danse@151.37.238.206) (Ping timeout: 240 seconds) |
| 19:06:35 | × | RedFlamingos quits (~RedFlamin@user/RedFlamingos) (Quit: RedFlamingos) |
| 19:07:14 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) (Remote host closed the connection) |
| 19:07:26 | × | analoq quits (~yashi@user/dies) (Ping timeout: 268 seconds) |
| 19:09:18 | → | danza joins (~danza@151.47.233.72) |
| 19:14:24 | → | danse-nr3 joins (~danse@151.47.233.72) |
| 19:17:36 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) |
| 19:17:54 | × | danza quits (~danza@151.47.233.72) (Ping timeout: 252 seconds) |
| 19:20:08 | → | Natch joins (~natch@c-9e07225c.038-60-73746f7.bbcust.telenor.se) |
| 19:21:43 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 19:21:55 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:25:36 | × | alexherbo2 quits (~alexherbo@2a02-8440-3240-ce99-a4f7-9aab-90ab-68ff.rev.sfr.net) (Ping timeout: 250 seconds) |
| 19:28:33 | → | alexherbo2 joins (~alexherbo@2a02-8440-3240-ce99-a4f7-9aab-90ab-68ff.rev.sfr.net) |
| 19:29:19 | → | taupiqueur joins (~taupiqueu@2a02:8440:3240:ce99:a4f7:9aab:90ab:68ff) |
| 19:38:51 | × | bradparker quits (sid262931@id-262931.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 19:38:51 | × | edm quits (sid147314@id-147314.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 19:39:00 | → | bradparker joins (sid262931@id-262931.uxbridge.irccloud.com) |
| 19:39:19 | × | iqubic quits (~avi@2601:602:9502:c70:589:c039:227d:3881) (Ping timeout: 260 seconds) |
| 19:39:19 | × | haasn quits (sid579015@id-579015.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 19:39:19 | × | flukiluke quits (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Ping timeout: 260 seconds) |
| 19:39:23 | → | glguy_ joins (g@libera/staff/glguy) |
| 19:39:28 | → | berberman_ joins (~berberman@user/berberman) |
| 19:39:35 | → | iqubic joins (~avi@2601:602:9502:c70:589:c039:227d:3881) |
| 19:39:38 | → | flukiluke joins (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 19:39:47 | × | b20n quits (sid115913@id-115913.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 19:39:47 | × | joel135 quits (sid136450@id-136450.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 19:39:55 | × | Reinhilde quits (~Ellenor@callbox.trd.is) (Remote host closed the connection) |
| 19:40:15 | × | gmc quits (sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 19:40:15 | × | berberman quits (~berberman@user/berberman) (Ping timeout: 260 seconds) |
| 19:40:15 | × | liyang quits (sid322268@id-322268.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 19:40:44 | × | glguy quits (glguy@libera/staff/glguy) (Read error: Connection reset by peer) |
| 19:42:51 | → | joel135 joins (sid136450@id-136450.hampstead.irccloud.com) |
| 19:42:52 | → | liyang joins (sid322268@id-322268.uxbridge.irccloud.com) |
| 19:42:56 | → | haasn joins (sid579015@id-579015.hampstead.irccloud.com) |
| 19:43:04 | → | edm joins (sid147314@id-147314.hampstead.irccloud.com) |
| 19:43:14 | → | gmc joins (sid58314@id-58314.ilkley.irccloud.com) |
| 19:46:01 | × | danse-nr3 quits (~danse@151.47.233.72) (Remote host closed the connection) |
| 19:46:25 | → | danse-nr3 joins (~danse@151.47.233.72) |
| 19:48:38 | × | iqubic quits (~avi@2601:602:9502:c70:589:c039:227d:3881) (Remote host closed the connection) |
| 19:48:54 | → | iqubic joins (~avi@2601:602:9502:c70:589:c039:227d:3881) |
| 19:51:19 | × | alexherbo2 quits (~alexherbo@2a02-8440-3240-ce99-a4f7-9aab-90ab-68ff.rev.sfr.net) (Remote host closed the connection) |
| 19:52:40 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 19:53:16 | × | eggplantade quits (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) (Remote host closed the connection) |
| 19:53:40 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 19:56:28 | → | b20n joins (sid115913@id-115913.uxbridge.irccloud.com) |
| 20:02:31 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 276 seconds) |
| 20:03:07 | <EvanR> | tri, by using forkIO threads or async you can pretty easily set up "the actor model" |
| 20:03:30 | <EvanR> | also you might want to fix your connection / client somehow |
| 20:04:10 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 20:04:11 | × | danse-nr3 quits (~danse@151.47.233.72) (Ping timeout: 264 seconds) |
| 20:04:47 | × | mikess quits (~sam@user/mikess) (Ping timeout: 268 seconds) |
| 20:05:34 | → | Ellenor joins (ellenor@callbox.trd.is) |
| 20:05:36 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 20:05:52 | <Joao003> | If `Integer's have infinite range, then how are they stored? |
| 20:06:05 | <monochrom> | One byte at a time? |
| 20:06:26 | <Joao003> | You need a length variable for that. |
| 20:06:33 | <monochrom> | Sure. |
| 20:06:36 | <int-e> | ...maybe revisit your premise |
| 20:07:01 | <c_wraith> | they don't have infinite range, fwiw |
| 20:07:07 | <dminuoso_> | Joao003: https://hackage.haskell.org/package/ghc-bignum-1.3/docs/src/GHC.Num.Integer.html#Integer |
| 20:07:15 | <c_wraith> | they have a maximum of 2^64 limbs, IIRC |
| 20:07:20 | <int-e> | "arbitrary precision" is subject to available memory. |
| 20:07:22 | <dminuoso_> | https://hackage.haskell.org/package/ghc-bignum-1.3/docs/GHC-Num-BigNat.html#t:BigNat-35- |
| 20:08:17 | <exarkun> | Joao003: Supposing they really did have infinite range, are you sure you need a length variable? |
| 20:08:23 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 20:08:23 | <int-e> | And yeah that limb thing puts a hard bound of 2^(2^70) on things on a 64 bit architecture. |
| 20:08:39 | <Joao003> | Hackage's documentation of Prelude documents them as infinite range, which under my assumption, is dependent on implementation |
| 20:08:52 | <dminuoso_> | Well, infinite range by specification, limited by reality. |
| 20:08:59 | <Joao003> | Yes |
| 20:09:26 | <dminuoso_> | Our observable universe has a finite number of atoms/energy, which means there is a physical limit to how much information you could physically store. |
| 20:09:32 | <dminuoso_> | Regardless of how large you scale your implementation. |
| 20:09:39 | <Joao003> | dminuoso_: The Haskell world almost never cares about reality |
| 20:09:53 | <int-e> | If you wonder about a theoretical answer, https://en.wikipedia.org/wiki/Elias_omega_coding encodes natural numbers as self-delimiting bit strings (so it's a prefix code). |
| 20:10:01 | <monochrom> | Well that escalated quickly. |
| 20:10:23 | <int-e> | There is an encoding of length in their but the length of the length is itself variable. |
| 20:10:51 | <dminuoso_> | Joao003: See https://iohk.io/en/blog/posts/2020/07/28/improving-haskells-big-numbers-support/ for some details on how ghc-bignum works. |
| 20:11:06 | <Joao003> | If `Integer's are precise, then `Float's are the opposite, right? |
| 20:11:17 | → | mikess joins (~sam@user/mikess) |
| 20:11:24 | <dminuoso_> | Joao003: Well they are also precise, depending on what you mean by it. |
| 20:11:28 | <monochrom> | I don't think anyone knows what that means. |
| 20:11:29 | <dminuoso_> | That is, we dont store them analog. |
| 20:11:39 | <dminuoso_> | We use IEEE 754. |
| 20:11:45 | <monochrom> | Anyone. Including the author. Perhaps especially the author. |
| 20:11:45 | × | juri__ quits (~juri@79.140.117.100) (Read error: Connection reset by peer) |
| 20:12:05 | <Joao003> | dminuoso_: If we mean accuracy, then IEEE 754 is imprecise |
| 20:12:07 | → | tri25 joins (~tri@4133220a.cst.lightpath.net) |
| 20:12:11 | tri25 | is now known as _tri |
| 20:12:12 | <dminuoso_> | Define accuracy. |
| 20:12:15 | <exarkun> | does the Haskell report require IEEE 754? Or could I build a computer with analog an Float representation and make a conforming Haskell implementation for it? |
| 20:12:22 | <int-e> | Floats aren't inexact by themselves. Arithmetic on floats tends to round a lot. |
| 20:12:24 | <dminuoso_> | Conforming IEEE 754 implementations will agree in their answers, Joao003. |
| 20:12:37 | <Joao003> | > 0.1 + 0.2 --dminuoso_ |
| 20:12:39 | <lambdabot> | 0.30000000000000004 |
| 20:12:48 | <dminuoso_> | Joao003: Yes, and any IEEE 754 conforming implementation will agree with that result. |
| 20:12:55 | <dminuoso_> | Is that imprecise? It depends on your perspective and expectation. |
| 20:12:55 | <exarkun> | Joao003: This is a 100% accurate IEEE 754 result. |
| 20:13:01 | <Joao003> | Yes. |
| 20:13:23 | <Joao003> | But it quickly becomes inaccurate when we do this: |
| 20:13:29 | <Joao003> | > (0.1 + 0.2) == 0.3 |
| 20:13:31 | <lambdabot> | False |
| 20:13:34 | <dminuoso_> | IEEE 754 is an imprecise approximation of rational arithmatic, if thats what you mean. |
| 20:13:39 | <Joao003> | Yes |
| 20:13:42 | <dminuoso_> | Then sure. |
| 20:14:00 | <dminuoso_> | Joao003: The primary fault here is programmers tend to think of 0.1 as a rational number. |
| 20:14:08 | <dminuoso_> | (In this context) its not. |
| 20:14:12 | <Joao003> | This discussion escalated quickly from discussing `Integer's to discussing IEEE 754 |
| 20:14:17 | <int-e> | > toRational 0.1 |
| 20:14:19 | <lambdabot> | 3602879701896397 % 36028797018963968 |
| 20:14:21 | <int-e> | :-) |
| 20:14:25 | <Joao003> | XD |
| 20:14:46 | <Joao003> | int-e: Goddammit, I hate emoticons with noses |
| 20:15:05 | <dminuoso_> | Joao003: So really, dont think of literals (monomorphized to Float/Double) as rational numbers. If you dont, you dont have any expectations with regards to their "accuracy" or "precision" |
| 20:15:06 | <int-e> | > toRational 0.1 + toRational 0.2 == toRational (0.1 + 0.2) -- I wonder |
| 20:15:08 | <lambdabot> | False |
| 20:15:12 | <dminuoso_> | It then all boils down to IEEE 754 semantics. |
| 20:15:26 | <Joao003> | dminuoso_: I don't. |
| 20:15:39 | <int-e> | Joao003: :-/ |
| 20:16:04 | <Joao003> | int-e: THAT NOSE EMOTICON :( |
| 20:16:27 | <yushyin> | :-) |
| 20:16:33 | <Joao003> | ò_ó |
| 20:16:42 | <int-e> | Joao003: Let me just say that you did this to yourself. |
| 20:16:44 | <int-e> | :-P |
| 20:16:51 | <exarkun> | Have some tolerance for differences. It's a good thing. |
| 20:17:06 | <Joao003> | ♂️ |
| 20:17:09 | <Joao003> | lol |
| 20:17:34 | <monochrom> | I wonder if that is a pun on floating point arithmetic. |
| 20:17:46 | <Joao003> | If :-D is a smiley, then tell me what's this: 8=D |
| 20:17:46 | → | juri_ joins (~juri@implicitcad.org) |
| 20:18:01 | <exarkun> | More escalation. Why? |
| 20:18:05 | <int-e> | dminuoso_: I honestly didn't know whether that would round or not. |
| 20:18:18 | <dminuoso_> | :t toRational |
| 20:18:19 | <lambdabot> | Real a => a -> Rational |
| 20:18:26 | <Joao003> | :t (%) |
| 20:18:27 | <lambdabot> | Integral a => a -> a -> Ratio a |
| 20:18:35 | <Joao003> | haha get ratio'd |
| 20:18:48 | <dminuoso_> | int-e: Luckily we have a strongly typed system where implicit coercion using magical hidden rules dont occur! |
| 20:18:50 | <int-e> | > map toRational [1/0, 0/0] |
| 20:18:51 | <lambdabot> | [179769313486231590772930519078902473361797697894230657273430081157732675805... |
| 20:18:58 | <Joao003> | lol |
| 20:19:06 | <int-e> | oh right, it would be too long for that. |
| 20:19:15 | <Joao003> | > map toRational [0.01] |
| 20:19:16 | <lambdabot> | [5764607523034235 % 576460752303423488] |
| 20:19:26 | <Joao003> | > map toRational [0.00000000001] |
| 20:19:27 | <lambdabot> | [6189700196426901 % 618970019642690137449562112] |
| 20:19:39 | <int-e> | (try that in ghci, "proof" that infinity is an integer, but so is NaN) |
| 20:19:42 | <[exa]> | ieee floats never disappoint |
| 20:19:44 | <dminuoso_> | Also I really like that Real typeclass. |
| 20:19:46 | <dminuoso_> | "Real numbers. The Haskell report defines no laws for Real" |
| 20:19:53 | <Joao003> | [exa]: To me they do |
| 20:19:54 | × | taupiqueur quits (~taupiqueu@2a02:8440:3240:ce99:a4f7:9aab:90ab:68ff) (Quit: WeeChat 4.1.2) |
| 20:20:04 | <Joao003> | dminuoso_: LOL |
| 20:20:08 | <int-e> | The Real world is a cruel and unforgiving place. |
| 20:20:16 | <Joao003> | XD |
| 20:20:37 | <dminuoso_> | > toRational (0.1 :: _) |
| 20:20:37 | <[exa]> | even if you look into actual GHC.Prim.RealWorld..........it's empty!!!11 |
| 20:20:38 | <lambdabot> | 3602879701896397 % 36028797018963968 |
| 20:20:41 | <Joao003> | I also like how `Integer's have the typeclass `Fractional' |
| 20:20:45 | <dminuoso_> | Huh, why doesnt lambdabot error out here? |
| 20:20:55 | <dminuoso_> | % () :: _ |
| 20:20:55 | <yahb2> | <interactive>:5:7: error: ; • Found type wildcard ‘_’ standing for ‘()’ ; To use the inferred type, enable PartialTypeSignatures ; • In an expression type signature: _ ; In the ... |
| 20:21:01 | <dminuoso_> | % toRational (0.1 :: _) |
| 20:21:01 | <yahb2> | <interactive>:7:20: error: ; • Found type wildcard ‘_’ standing for ‘Double’ ; To use the inferred type, enable PartialTypeSignatures ; • In an expression type signature: _ ; In... |
| 20:21:14 | <dminuoso_> | Okay, so Real a defaults to Double? |
| 20:21:23 | <Joao003> | lol |
| 20:21:31 | <Maxdamantus> | in the case of `0.1 + 0.2`, the arithmetic is precise. the problem is that binary floats can't represent 0.1, 0.2 or 0.3. |
| 20:21:39 | <Joao003> | Yes |
| 20:21:40 | <monochrom> | I think Haskell 2010 defaults Real to Double. |
| 20:21:54 | <geekosaur> | `default (Integer, Double)` |
| 20:22:06 | <Joao003> | % iterate (/10) 1 |
| 20:22:06 | <yahb2> | [1.0,0.1,1.0e-2,1.0e-3,1.0e-4,1.0e-5,1.0000000000000002e-6,1.0000000000000002e-7,1.0000000000000002e-8,1.0000000000000003e-9,1.0000000000000003e-10,1.0000000000000003e-11,1.0000000000000002e-12,1.0... |
| 20:22:07 | <dminuoso_> | monochrom: Like I said, good think we have a strongly typed system without implicit coercions using magical hidden and unknown rules. |
| 20:22:07 | <geekosaur> | since 0.1 can't be Integer, it becomes Double |
| 20:22:09 | <dminuoso_> | :-) |
| 20:22:28 | <Joao003> | > (1 % 10) % 10 |
| 20:22:29 | <lambdabot> | error: |
| 20:22:29 | <lambdabot> | • No instance for (Integral (Ratio Integer)) |
| 20:22:29 | <lambdabot> | arising from a use of ‘e_111010’ |
| 20:22:31 | <Maxdamantus> | in particular, because there's no solution for integers `m` and `e` where `m*2^e = 0.1` |
| 20:22:37 | <Joao003> | yes |
| 20:22:53 | <monochrom> | I may weasel out from that with "defaulting is not implicit coercions"... :) |
| 20:23:11 | <dminuoso_> | What does `0.3 :: Double` even mean? Does IEEE 754 give some definition on how to map rationals to IEEE 754? |
| 20:23:22 | <Joao003> | Lesson: Do not use floats unless the inaccuracies do not bother you |
| 20:23:29 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 20:24:04 | <int-e> | Maxdamantus: No, I tested above: If you take the Double representation of 0.1 and 0.2 and add them, the result isn't exact but gets rounded. |
| 20:24:54 | <monochrom> | I have not read IEEE 754. I go out on a limb to guess that it specifies relations with decimal notation. |
| 20:25:00 | <Maxdamantus> | int-e: the result is exactly the sum of the IEEE-754 values corresponding to the strings 0.1 and 0.2. |
| 20:25:05 | <Joao003> | > (2147483647 :: Int) + 1 |
| 20:25:06 | <lambdabot> | 2147483648 |
| 20:25:19 | <Maxdamantus> | dminuoso_: yes. it defines the relationship with decimal notation. |
| 20:25:26 | <int-e> | > 0.1 + 0.2 - 0.2 == 0.1 |
| 20:25:27 | <lambdabot> | False |
| 20:25:30 | <Joao003> | > (2147483647+ 1) :: Int |
| 20:25:31 | <lambdabot> | 2147483648 |
| 20:25:46 | <geekosaur> | > maxBound :: Int |
| 20:25:47 | <lambdabot> | 9223372036854775807 |
| 20:25:50 | <Joao003> | Oh ok |
| 20:25:56 | <Joao003> | x_x |
| 20:25:59 | → | eggplantade joins (~Eggplanta@2600:1700:38c5:d800:21a7:e3e2:1963:5573) |
| 20:26:13 | <int-e> | (0.1 + 0.2 get rounded; the subtraction is actually exact) |
| 20:26:17 | <int-e> | > let a = 0.1 + 0.2; b = 0.2 in toRational a - toRational b == toRational (a-b) |
| 20:26:19 | <lambdabot> | True |
| 20:26:26 | <Joao003> | > ((maxBound :: Int) + 1) :: Int |
| 20:26:28 | <lambdabot> | -9223372036854775808 |
| 20:26:31 | <int-e> | > let a = 0.1; b = 0.2 in toRational a + toRational b == toRational (a + b) |
| 20:26:32 | <lambdabot> | False |
| 20:26:33 | <Joao003> | Overflow |
| 20:26:33 | <Maxdamantus> | dminuoso_: it defines it in both directions too, such that the value of computing 1/10 has "0.1" as its "canonical representation", even though that value is not exactly 0.1 |
| 20:27:52 | <int-e> | > toRational 0.1 - 1/10 |
| 20:27:53 | <lambdabot> | 1 % 180143985094819840 |
| 20:28:25 | <int-e> | toRational is a pretty good tool for working out examples for this |
| 20:28:49 | <int-e> | > toRational 0.1 - 0.1 -- not sure why I didn't write it like this |
| 20:28:50 | <lambdabot> | 1 % 180143985094819840 |
| 20:28:52 | <monochrom> | This is why "define 'precise'", "define 'accurate'" are right on. "precise" "accurate" under whose prejudice? |
| 20:29:04 | <Maxdamantus> | int-e: ah right, I guess in this case the arithmetic is indeed imprecise, because it has to increase the exponent. |
| 20:29:11 | <monochrom> | And that's right, it's always someone's prejudice. It's always personal. |
| 20:29:28 | <Joao003> | > 0.999999999999999999999999999999999999999999999999999999999999 == 1 |
| 20:29:30 | <lambdabot> | True |
| 20:31:03 | <Joao003> | TIL: Complex exists |
| 20:31:07 | <Joao003> | > 0 +: 1 |
| 20:31:09 | <lambdabot> | error: |
| 20:31:09 | <lambdabot> | • Variable not in scope: (+:) :: t0 -> t1 -> t |
| 20:31:09 | <lambdabot> | • Perhaps you meant one of these: |
| 20:31:12 | <Joao003> | > 0 :+ 1 |
| 20:31:14 | <lambdabot> | 0 :+ 1 |
| 20:31:22 | <Joao003> | :t 0 :+ 1 |
| 20:31:23 | <lambdabot> | Num a => Complex a |
| 20:31:30 | <monochrom> | Did you know: Complex is a Monad too. |
| 20:31:39 | <Joao003> | Nice |
| 20:31:43 | <Joao003> | @src Complex |
| 20:31:43 | <lambdabot> | data (RealFloat a) => Complex a = !a :+ !a |
| 20:32:14 | <geekosaur> | someone should update that to Haskell2010 someday |
| 20:32:38 | <monochrom> | It's also Traversable haha. |
| 20:32:47 | <monochrom> | "My life is complete." |
| 20:33:25 | × | todi quits (~todi@p5dca55c4.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in) |
| 20:33:28 | <monochrom> | It is also a representable functor. OK I'll stop. (Really complete now.) |
| 20:35:36 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 20:41:07 | × | araujo quits (~araujo@216.73.163.162) (Ping timeout: 255 seconds) |
| 20:42:55 | × | gehmehgeh quits (~user@user/gehmehgeh) (Ping timeout: 240 seconds) |
| 20:45:19 | → | gmg joins (~user@user/gehmehgeh) |
| 20:45:43 | <juri_> | using floats can be done right. |
| 20:46:18 | <juri_> | but unless you have an idea of "what is close enough" in your algebra, you're probably in a cursed land. |
| 20:46:51 | <int-e> | monochrom: most people's understanding of floating point numbers is pretty vague, or should I say imprecise? |
| 20:48:40 | <EvanR> | many people believe that floats don't have a definite value. They are confused. But you can impose an interval arithmetic on them as an additional protocol, interpreting their value to be an interval |
| 20:48:58 | <EvanR> | but the fact remains they have only 1 value at a time |
| 20:49:27 | <EvanR> | an exact known value |
| 20:49:35 | <int-e> | . o O ( NaN ) |
| 20:50:01 | <EvanR> | Nan = not a number, not Not A Value xD |
| 20:50:19 | <EvanR> | bottom is not a value |
| 20:50:42 | <int-e> | EvanR: you're not wrong |
| 20:52:14 | <juri_> | units of least precision, and more importantly, how to interpret the accumulated error... these are important in floating point systems. |
| 20:52:45 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 20:53:03 | <EvanR> | unfortunately accumulated error isn't tracked anywhere, it's up to your application |
| 20:53:28 | <EvanR> | and in a given application it might not even be necessary because you only do exact math |
| 20:53:36 | × | malte quits (~malte@mal.tc) (Remote host closed the connection) |
| 20:54:53 | → | malte joins (~malte@mal.tc) |
| 20:56:43 | <EvanR> | > 0.999999999999999999999999999999999999999999999999999999999999 :: CReal == 1 |
| 20:56:45 | <lambdabot> | error: |
| 20:56:45 | <lambdabot> | Not in scope: type constructor or class ‘==’ |
| 20:56:53 | <EvanR> | > (0.999999999999999999999999999999999999999999999999999999999999 :: CReal) == 1 |
| 20:56:54 | <lambdabot> | True |
| 20:57:00 | × | trev quits (~trev@user/trev) (Quit: trev) |
| 20:57:06 | × | _tri quits (~tri@4133220a.cst.lightpath.net) (Quit: Client closed) |
| 20:58:23 | <EvanR> | the same high school student who would object to that also has a good chance of saying 0.9999... forever doesn't equal 1 either xD |
| 20:59:35 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 20:59:54 | × | aruns quits (~aruns@user/aruns) (Ping timeout: 256 seconds) |
| 21:01:48 | glguy_ | is now known as glguy |
| 21:07:25 | <int-e> | EvanR: there's a valid question in there... because high school students never see a definition of a real number either |
| 21:09:45 | <EvanR> | teacher who is trying to be clever "ok what would you say is 1 minus 0.999 repeating" |
| 21:09:57 | <EvanR> | student "zero point zero zero zero forever with 1 at the end" |
| 21:10:36 | <EvanR> | xD |
| 21:10:48 | <int-e> | and you can kind of construct numbers that work that way |
| 21:10:58 | <EvanR> | yeah I was thinking about that earlier |
| 21:11:06 | <int-e> | (surreal numbers are an appealing example) |
| 21:11:42 | <EvanR> | it might work if the posed question was, what is 1 minute 0.999... forever with 9 at the end xD |
| 21:11:45 | <int-e> | so the right answer to 0.999... = 1 is that it's a property of the real numbers and that's the only thing high school students are going to see. |
| 21:12:10 | <int-e> | and you should probably make 0.999... formal as a limit somewhere while explaining all that |
| 21:12:16 | <int-e> | you'll be there for a while |
| 21:12:49 | <probie> | I think "high school" students is a much too vague category |
| 21:13:19 | <int-e> | probie: average, not best of the best |
| 21:13:25 | → | infinity0_ joins (~infinity0@pwned.gg) |
| 21:13:25 | infinity0 | is now known as Guest6319 |
| 21:13:25 | infinity0_ | is now known as infinity0 |
| 21:14:38 | × | Guest6319 quits (~infinity0@pwned.gg) (Ping timeout: 260 seconds) |
| 21:15:11 | × | DigitalKiwi quits (~kiwi@137.184.156.191) (Quit: quite.) |
| 21:15:16 | <EvanR> | high "school students" |
| 21:15:32 | <EvanR> | very different category |
| 21:15:44 | → | DigitalKiwi joins (~kiwi@137.184.156.191) |
| 21:18:16 | Ellenor | is now known as Reinhilde |
| 21:18:37 | <probie> | Quite a few of the mathematically inclined high school students in my city also start doing the first year university maths courses whilst still in high school. They get the course credit for it (assuming they go to a university that recognises it), and it improves their university entrance score |
| 21:22:38 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Remote host closed the connection) |
| 21:23:15 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:28:10 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 21:28:19 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 276 seconds) |
| 21:35:02 | × | ft quits (~ft@p3e9bc784.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 21:36:42 | → | ft joins (~ft@p508db0fa.dip0.t-ipconnect.de) |
| 21:40:22 | <jjhoo> | 1 / 9 = 0.111... high school, arithmetic series |
| 21:40:56 | <int-e> | geometric series |
| 21:41:10 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:44:47 | × | wryish quits (~wryish@216.246.119.62) (Read error: Connection reset by peer) |
| 21:45:55 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 21:47:00 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:47:02 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 21:48:03 | → | wryish joins (~wryish@216.246.119.62) |
| 21:49:53 | <EvanR> | 0.1 + 1 + 1 + 1 + 1 + ... xD |
| 21:50:06 | <EvanR> | 0.11111... |
| 21:51:54 | × | Eoco quits (~ian@128.101.131.218) (Quit: WeeChat 4.1.1) |
| 21:52:07 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 256 seconds) |
| 21:52:33 | → | Eoco joins (~ian@128.101.131.218) |
| 21:52:36 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 21:53:56 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 21:56:54 | → | __monty__ joins (~toonn@user/toonn) |
| 21:58:47 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:01:03 | × | dhil quits (~dhil@2001:8e0:2014:3100:fe62:84ae:2b90:5200) (Ping timeout: 256 seconds) |
| 22:01:06 | <ncf> | edwardk: is there any reason that `divide` and `choose` are not yoneda-ified to get rid of the first argument? |
| 22:01:12 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:01:20 | <ncf> | and lose |
| 22:05:46 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 245 seconds) |
| 22:14:58 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 22:16:56 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:17:13 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:19:40 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 22:20:31 | × | machinedgod quits (~machinedg@93-138-57-84.adsl.net.t-com.hr) (Remote host closed the connection) |
| 22:23:08 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 22:25:23 | → | pavonia joins (~user@user/siracusa) |
| 22:25:47 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 22:26:23 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 22:32:20 | × | wryish quits (~wryish@216.246.119.62) (Quit: %blank%) |
| 22:32:37 | → | wryish joins (~wryish@216.246.119.62) |
| 22:35:21 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:35:42 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:42:28 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 22:43:11 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 22:47:07 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:48:11 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 22:50:13 | × | ft quits (~ft@p508db0fa.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 22:50:43 | × | johnw quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in) |
| 22:51:34 | → | ft joins (~ft@p4fc2ae2b.dip0.t-ipconnect.de) |
| 22:53:06 | × | emmanuelux_ quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 23:00:32 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 23:00:51 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 23:02:12 | → | nate4 joins (~nate@c-98-45-158-125.hsd1.ca.comcast.net) |
| 23:04:40 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 23:04:47 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 264 seconds) |
| 23:07:46 | × | nate4 quits (~nate@c-98-45-158-125.hsd1.ca.comcast.net) (Ping timeout: 276 seconds) |
| 23:10:38 | <Axman6> | probie: yeah but we're all nerds in this city, hardly average |
| 23:13:56 | <jjhoo> | int-e: yes, geometric. I was on the wikipedia about geometric series... got confused when writing |
| 23:15:36 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 23:17:01 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 23:17:56 | → | tri_ joins (~tri@ool-18bbef1a.static.optonline.net) |
| 23:23:36 | → | alexherbo2 joins (~alexherbo@2a02-8440-3241-6fde-605e-bbc1-347b-4f81.rev.sfr.net) |
| 23:23:51 | → | taupiqueur joins (~taupiqueu@2a02-8440-3241-6fde-605e-bbc1-347b-4f81.rev.sfr.net) |
| 23:24:43 | × | tri_ quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 23:25:12 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 23:25:29 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 23:29:14 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:34:34 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 23:34:56 | → | tri joins (~tri@ool-18bbef1a.static.optonline.net) |
| 23:35:06 | × | acidjnk_new quits (~acidjnk@p200300d6e72b9347b4dc018a2c6658c2.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 23:36:43 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 23:38:50 | × | idgaen quits (~idgaen@2a01:e0a:498:fd50:fcc6:bb5d:489a:ce8c) (Quit: WeeChat 4.1.1) |
| 23:39:07 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 23:39:39 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 23:40:21 | × | tri quits (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 245 seconds) |
| 23:46:56 | × | coot quits (~coot@89-69-206-216.dynamic.chello.pl) (Quit: coot) |
| 23:54:16 | → | johnw joins (~johnw@69.62.242.138) |
| 23:55:44 | → | sebagutiem joins (~sebagutie@2800:300:62e1:7fa1:80a7:2aab:4b46:cdd5) |
All times are in UTC on 2023-12-12.