Logs on 2020-09-20 (freenode/#haskell)
| 00:00:01 | × | MasterGruntR75 quits (~MasterGru@185.163.110.116) () |
| 00:04:28 | hackage | string-interpolate 0.3.0.1 - Haskell string/text/bytestring interpolation that just works https://hackage.haskell.org/package/string-interpolate-0.3.0.1 (williamyaoh) |
| 00:06:27 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 00:07:02 | × | alx741 quits (~alx741@186.178.110.2) (Ping timeout: 272 seconds) |
| 00:10:57 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Read error: Connection reset by peer) |
| 00:14:36 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 00:14:46 | ← | Plazma parts (~Plazma@freenode/staff-emeritus/plazma) () |
| 00:20:38 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 00:22:52 | × | __Joker_ quits (~Joker@180.151.105.65) (Ping timeout: 272 seconds) |
| 00:23:45 | → | machinedgod joins (~machinedg@24.51.251.11) |
| 00:25:52 | → | __Joker joins (~Joker@180.151.105.65) |
| 00:26:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 00:26:43 | × | cantstanya quits (~chatting@gateway/tor-sasl/cantstanya) (Ping timeout: 240 seconds) |
| 00:26:57 | → | wavemode joins (~wavemode@097-070-075-143.res.spectrum.com) |
| 00:28:12 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 260 seconds) |
| 00:30:05 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 240 seconds) |
| 00:30:58 | → | cantstanya joins (~chatting@gateway/tor-sasl/cantstanya) |
| 00:35:34 | → | gmt joins (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) |
| 00:38:01 | × | machinedgod quits (~machinedg@24.51.251.11) (Ping timeout: 260 seconds) |
| 00:44:28 | → | maroloccio joins (~marolocci@2a02:8084:601d:7f80:164f:8aff:fed8:411d) |
| 00:47:25 | × | aenesidemus quits (~aenesidem@c-73-53-247-25.hsd1.fl.comcast.net) (Quit: Leaving) |
| 00:48:26 | × | cantstanya quits (~chatting@gateway/tor-sasl/cantstanya) (Remote host closed the connection) |
| 00:50:43 | → | cantstanya joins (~chatting@gateway/tor-sasl/cantstanya) |
| 00:51:22 | × | solonarv quits (~solonarv@astrasbourg-653-1-186-165.w90-13.abo.wanadoo.fr) (Ping timeout: 272 seconds) |
| 00:51:23 | → | alx741 joins (~alx741@186.178.110.2) |
| 00:54:35 | → | toony1 joins (~toony@s91904426.blix.com) |
| 00:54:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 00:58:34 | × | MorrowM quits (~max@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 265 seconds) |
| 00:58:43 | → | polyrain joins (~polyrain@2001:8003:e501:6901:a8a8:546d:e1e3:2f7b) |
| 00:59:13 | → | MrZe joins (~root@140.213.56.183) |
| 00:59:27 | <MrZe> | hi |
| 00:59:54 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 01:00:40 | <MrZe> | anybody online ? |
| 01:00:48 | <MrZe> | 2 |
| 01:01:08 | <yushyin> | maybe |
| 01:01:56 | → | __Joker joins (~Joker@180.151.105.65) |
| 01:02:04 | → | OmegaDoug joins (6ca87592@dhcp-108-168-117-146.cable.user.start.ca) |
| 01:02:29 | <yushyin> | over 1000 users are online |
| 01:03:25 | × | ryansmccoy quits (~ryansmcco@156.96.151.132) (Ping timeout: 240 seconds) |
| 01:03:37 | → | ryansmccoy joins (~ryansmcco@68.235.48.108) |
| 01:04:22 | → | pera joins (~pera@unaffiliated/pera) |
| 01:04:24 | → | root_ joins (~root@140.213.56.183) |
| 01:04:28 | <sim590> | I have this function http://sprunge.us/3by4Qf which maps a function on some field of a type LBSNode in order to increment it. I'm getting "Pattern match(es) are non-exhaustive" error with "Patterns not matched: (LBSInternalNode _ _)". Why am I getting this error even though I did write `incIndex _` on the next line to cover every other cases? |
| 01:04:59 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 240 seconds) |
| 01:05:18 | × | MrZe quits (~root@140.213.56.183) (Ping timeout: 256 seconds) |
| 01:05:25 | <root_> | exit |
| 01:05:31 | <root_> | exit |
| 01:06:24 | <sim590> | Seems like this https://gitlab.haskell.org/ghc/ghc/-/issues/5728 is related? |
| 01:06:26 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 256 seconds) |
| 01:06:31 | <MarcelineVQ> | sim590: is mapML perhaps not exhaustive? |
| 01:06:42 | × | xff0x_ quits (~fox@2001:1a81:5373:6a00:4ccb:e51f:bb16:7d67) (Ping timeout: 260 seconds) |
| 01:06:58 | → | nbloomf joins (~nbloomf@104-183-67-6.lightspeed.fyvlar.sbcglobal.net) |
| 01:07:17 | <lechner> | Hi, what's a good way to print a string without double quotes, please? Thanks! |
| 01:07:43 | <MarcelineVQ> | putStr or putStrLn |
| 01:08:35 | → | xff0x_ joins (~fox@2001:1a81:53ac:b300:4ccb:e51f:bb16:7d67) |
| 01:08:39 | <sim590> | MarcelineVQ: I don't think so: http://sprunge.us/TKoZBk. And here's mapL: http://sprunge.us/9NIrK4. If you need to go deeper, here's http://sprunge.us/jUAklr. |
| 01:08:45 | <lechner> | Sorry, it's actually a Data.ByteString.Char8.ByteString |
| 01:08:59 | <jumper149> | lechner: `print` is the same as `putStrLn . show` https://hackage.haskell.org/package/base-4.14.0.0/docs/src/System.IO.html#print |
| 01:09:16 | <lechner> | jumper149: yes, but that adds the quotes |
| 01:09:37 | <lechner> | i currently use putStrLn show |
| 01:09:43 | <jumper149> | Was just making sure you understand what each part does! |
| 01:10:02 | <lechner> | i think the show is not pretty |
| 01:10:22 | × | root_ quits (~root@140.213.56.183) (Ping timeout: 272 seconds) |
| 01:10:23 | <sim590> | MarcelineVQ: also this: `type LBSTree a = BSTree (LBSNode a)` should clarify things. There's LBSTree, but also BSTree which is the base for the former. But the message is just warning also. It's not an error, but I don't like that. |
| 01:10:52 | → | rprije joins (~rprije@27.143.220.203.dial.dynamic.acc01-myal-dub.comindico.com.au) |
| 01:10:56 | <jumper149> | How about BS.putStr https://hackage.haskell.org/package/bytestring-0.10.12.0/docs/Data-ByteString-Char8.html#v:putStr |
| 01:11:01 | × | Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 264 seconds) |
| 01:11:27 | <lechner> | i am concatenating with ++ so i have to convert first |
| 01:12:05 | <jumper149> | Also if you use functions on String like Prelude.print and ++ you will lose some of the benefits from ByteString. |
| 01:12:23 | <jumper149> | I guess you just want it to work and only use bytestring because a library gives it to you? |
| 01:12:41 | <MarcelineVQ> | sim590: What's the full warning? |
| 01:13:26 | <yushyin> | lechner: with String use prelude's putStr with Bytestring use Bytestring's putStr |
| 01:13:55 | <lechner> | I would like to concatenate. last line here: https://dpaste.com/7RQPNTE63 |
| 01:14:21 | <sim590> | MarcelineVQ: http://sprunge.us/NW5U6N. I'm getting it on two different calls. The first that I pasted and another one lower. |
| 01:15:16 | <sim590> | MarcelineVQ: here's the whole file if that helps: http://sprunge.us/PxW93j |
| 01:16:14 | <sim590> | MarcelineVQ: I just tried RecordWildCards but it didn't help me fix it. |
| 01:16:57 | <MarcelineVQ> | sim590: that's not about the left side pattern that error is pointing at the right side, ghc isn't super smart here so it's being conservative: it's telling you that "return $ l {index = i+amount}" could be dangerous because l might be LBSInternalNode instead of LBSLeaf which doesn't have an 'index' field |
| 01:17:02 | <jumper149> | lechner: For conversion functions there is pack and unpack in the ByteString library |
| 01:17:09 | <jumper149> | They will convert from and to String |
| 01:17:20 | <jumper149> | so for you it would be C.unpack |
| 01:17:26 | <divVerent> | 135 one seems a false positive as you asserted on the ViewPattern before |
| 01:17:26 | <MarcelineVQ> | Now, we know better, but it doesn't it looks like |
| 01:18:13 | <MarcelineVQ> | fyi using record syntax on sum types like this is avoided for that reason, if you forget to make sure what constructor you have your field accesor could crash your program since it might try to get 'index' from LBSNode which doesn't have one |
| 01:18:33 | <divVerent> | same in the second one |
| 01:18:43 | × | ntwhaaci^ quits (ntwoaaci@ip98-184-89-2.mc.at.cox.net) () |
| 01:19:00 | <divVerent> | yes, but here technically the compiler should already know which record case is taken |
| 01:19:33 | <OmegaDoug> | Is there a way in to tell stack where to write the executable when running "stack build"? I'd like to put in the root of the "stack-work" folder. |
| 01:19:44 | <sim590> | MarcelineVQ: OK, but on line 120, I'm using the "same technique" but it doesn't complain. Am I not? |
| 01:20:03 | <sim590> | Oh I'm sorry. You said the right side, so it's not the same thing |
| 01:20:09 | × | xpika quits (~alan@2001:8003:5d32:1f00:65e7:740e:363f:f90f) (Ping timeout: 244 seconds) |
| 01:20:15 | <lechner> | jumper149: thanks! |
| 01:20:27 | <sim590> | But isn't the type of the right side determined by the left side since l is just the name of the pattern matched? |
| 01:21:07 | <lechner> | what is the difference between the <- and the =<< operator, please? |
| 01:21:49 | <MarcelineVQ> | sim590: afaict the issue is that you're updating `l` and `l` might not always have `index` as a field, appearantly pattern matching it didn't inform ghc that `l` is LBSLeaf and thus safe. I think this is weird but is the only explanation I can think of |
| 01:21:51 | <ski> | lechner : `=<<' is an ordinary operator, defined in a library. `<-' is special syntax, like `=' or `::' |
| 01:21:55 | <jumper149> | lechner: First of all <- is a keyword and part of the do-nation and =<< is a function |
| 01:22:16 | <ski> | @type (=<<) |
| 01:22:17 | <lambdabot> | Monad m => (a -> m b) -> m a -> m b |
| 01:23:25 | <ski> | f =<< act = do x <- act |
| 01:23:28 | <ski> | f x |
| 01:23:39 | <ski> | is how it could be defined |
| 01:23:56 | <ski> | (the actual definition is probably something like |
| 01:23:59 | <ski> | @src =<< |
| 01:23:59 | <lambdabot> | f =<< x = x >>= f |
| 01:24:00 | <lechner> | ski: thanks, that's what I thought! |
| 01:24:14 | <MarcelineVQ> | sim590: I'm could be wrong though, something about that warning is bugging me |
| 01:24:24 | <ski> | where the `do'-notation syntactic sugar expands to calls to `>>=' (and `>>')) |
| 01:25:09 | <ski> | `<-' is part of `do'-notation (the same symbol `<-' is also used in list comprehensions) |
| 01:25:22 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 260 seconds) |
| 01:25:33 | <sim590> | MarcelineVQ: Yeah... I find that weird also. It really seems to be related to https://gitlab.haskell.org/ghc/ghc/-/issues/5728, but this issue is quite old and since they flagged it as a duplicate of some issue that they claim having fixed, I'm a bit confused. |
| 01:26:25 | <MarcelineVQ> | the answer is likely in the haskell report or ghc manual since it's related to record update syntax |
| 01:27:00 | × | nbloomf quits (~nbloomf@104-183-67-6.lightspeed.fyvlar.sbcglobal.net) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 01:29:02 | <MarcelineVQ> | sim590: really though the answer you're gonna get mostly is do not use record syntax for sum types like Trees :> |
| 01:30:00 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 01:30:26 | <sim590> | MarcelineVQ: but I'm really just updating a Node inside a Tree, not the Tree itself! |
| 01:30:44 | <sim590> | I mean that I have a complex type that is a the Node here. It's LBSNode. |
| 01:30:47 | × | acidjnk_new2 quits (~acidjnk@p200300d0c7365818803e8c849f4b43fc.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 01:31:20 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 01:31:27 | <ski> | > Node {rootLabel = (),subForest = []} |
| 01:31:30 | <lambdabot> | Node {rootLabel = (), subForest = []} |
| 01:31:31 | <ski> | > (Node) {rootLabel = (),subForest = []} |
| 01:31:33 | <lambdabot> | error: |
| 01:31:33 | <lambdabot> | • Couldn't match expected type ‘Tree a1’ |
| 01:31:33 | <lambdabot> | with actual type ‘a0 -> Forest a0 -> Tree a0’ |
| 01:33:18 | <MarcelineVQ> | But you are updating a tree, `index` takes a tree not a leaf, it just only works if the tree was a leaf right? |
| 01:33:37 | <MarcelineVQ> | this is the most relevant report section I can find https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-490003.15 |
| 01:34:20 | <MarcelineVQ> | starting with "data T = T1 { y :: Int } | T2 { y :: Bool } -- BAD" :> |
| 01:35:33 | <sim590> | MarcelineVQ: no. Look at the full file: http://sprunge.us/PxW93j. The type of `index` is `LBSNode a -> Int`. A LBSNode has a LBSLeaf as constructor. |
| 01:35:38 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:b852:f831:8cd4:429) |
| 01:36:13 | × | maroloccio quits (~marolocci@2a02:8084:601d:7f80:164f:8aff:fed8:411d) (Ping timeout: 272 seconds) |
| 01:36:46 | <MarcelineVQ> | alright then, a sum datatype still |
| 01:37:06 | <MarcelineVQ> | All that aside what I'd try, if I wanted to keep the labels, is probably incIndex LBSLeaf{index = i, leafContent = c} = return $ LBSLeaf {index = i+amount, leafContent = c} |
| 01:37:36 | <MarcelineVQ> | so that we're not updating `l` but making a LBSLeaf |
| 01:37:46 | <MarcelineVQ> | and you can probably use RecordWildcards or punning to shorten that if you want |
| 01:38:32 | <MarcelineVQ> | idk if that's the exact right syntax for record construction since I've never really needed to do it, hopefully the idea comes across |
| 01:39:00 | <ski> | it is |
| 01:39:22 | <sim590> | Hmmm. Yeah. I guess I can do that in order to avoid the warning. But definitely, GHC should not display a warning in principle. May be I can file a bug. |
| 01:39:23 | <ski> | (also that `$' is redundant) |
| 01:39:38 | <MarcelineVQ> | Really ghc should be satisfied that you matched on LBSLeaf but it's being a bit of a penis |
| 01:40:08 | × | oxide quits (~lambda@unaffiliated/mclaren) (Ping timeout: 272 seconds) |
| 01:40:18 | <MarcelineVQ> | satisfied as in: should understand that `l` has to be LBSLeaf |
| 01:40:58 | → | eric joins (~eric@2804:431:c7d4:402a:4dc9:97ef:220b:73aa) |
| 01:41:34 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Quit: WeeChat 2.9) |
| 01:42:14 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 01:43:11 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 01:43:47 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 01:44:04 | <sim590> | Yeah. So, this is a bug. May be it's already reported.. Ahhh. 4,060 bugs to look through. Mehhhh. ;). |
| 01:45:23 | <sim590> | Is there a performance difference between both ways of writing it? What I mean is Between record-update and Construction of the same type with the same values. Will GHC be able use some properties of persistent data structure in order to avoid copying things? Does update-record even do that? |
| 01:45:43 | × | eric quits (~eric@2804:431:c7d4:402a:4dc9:97ef:220b:73aa) (Ping timeout: 272 seconds) |
| 01:45:56 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Ping timeout: 256 seconds) |
| 01:47:27 | hackage | regex-pcre-builtin 0.95.1.1.8.44 - PCRE Backend for "Text.Regex" (regex-base) https://hackage.haskell.org/package/regex-pcre-builtin-0.95.1.1.8.44 (AudreyTang) |
| 01:47:42 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 01:48:27 | hackage | source-constraints 0.0.2 - Source constraints GHC plugin https://hackage.haskell.org/package/source-constraints-0.0.2 (mbj) |
| 01:48:31 | <MarcelineVQ> | Pretty much the same steps are taken regardless. |
| 01:48:54 | <MarcelineVQ> | check out the translation table in section 3.15.3 |
| 01:49:23 | → | kleisli_ joins (~kleisli@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) |
| 01:49:45 | <MarcelineVQ> | Either you case and build a record or update syntax is gonna case and build a record |
| 01:50:18 | <MarcelineVQ> | Which is surely also our source for the unmatched pattern warning |
| 01:51:38 | <ski> | (hm, in Mercury, if it can prove the old reference is unique, it will do an update-in-place, iirc) |
| 01:52:20 | → | Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-131-172.cust.tzulo.com) |
| 01:52:34 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 01:52:34 | <MarcelineVQ> | ski: ghc is probably smarter than the report here, but just based on this it's not something to be too concerned about |
| 01:53:03 | → | gestone joins (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) |
| 01:53:15 | <MarcelineVQ> | sim590: it you're worried about it it could be an interesting benchmark to do |
| 01:54:28 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 01:54:40 | × | kyagrd__ quits (sid102627@gateway/web/irccloud.com/x-mzcjmohivbettnaw) (Read error: Connection reset by peer) |
| 01:54:42 | × | mcfilib quits (sid302703@gateway/web/irccloud.com/x-jpgleryxlbiywuvp) (Read error: Connection reset by peer) |
| 01:54:56 | → | kyagrd__ joins (sid102627@gateway/web/irccloud.com/x-umexjnjqxisrtwcp) |
| 01:55:39 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 01:56:15 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 01:56:28 | → | mcfilib joins (sid302703@gateway/web/irccloud.com/x-mcvztaukmltliuld) |
| 01:57:49 | <sim590> | Well. It's not very worrying. I was mainly wondering in order to know for other use cases. |
| 01:58:40 | <sim590> | But then since I have to use the constructor, I can go back to the following syntax `incIndex (LBSLeaf i c) = return $ LBSLeaf (i+amount) c` which is the default I normally use. |
| 01:58:46 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 01:58:59 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 01:58:59 | × | pera quits (~pera@unaffiliated/pera) (Ping timeout: 240 seconds) |
| 01:59:18 | <sim590> | The main point of using the record syntax is to update things, but since I cannot do that here without creating a warning, then it's not worth writing the fields in the record syntax. |
| 01:59:47 | × | Amras quits (~Amras@unaffiliated/amras0000) (Remote host closed the connection) |
| 02:00:01 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 02:00:35 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 02:00:36 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 02:00:48 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 02:00:55 | → | booppoob joins (uid425746@gateway/web/irccloud.com/x-zlvvmspyhmlayeab) |
| 02:01:23 | ← | booppoob parts (uid425746@gateway/web/irccloud.com/x-zlvvmspyhmlayeab) () |
| 02:01:37 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 02:02:04 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:b852:f831:8cd4:429) (Quit: Textual IRC Client: www.textualapp.com) |
| 02:02:42 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 02:04:06 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:7d39:b02b:8868:9bea) |
| 02:04:12 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 02:06:27 | hackage | stm-queue 0.1.0.0 - An implementation of a real-time concurrent queue https://hackage.haskell.org/package/stm-queue-0.1.0.0 (sgschlesinger) |
| 02:08:24 | <dolio> | sim590: You could turn off -Wincomplete-record-updates if it's not smart enough to figure it out. |
| 02:08:27 | × | OmegaDoug quits (6ca87592@dhcp-108-168-117-146.cable.user.start.ca) (Remote host closed the connection) |
| 02:08:35 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Ping timeout: 240 seconds) |
| 02:08:57 | → | jumper149 joins (~jumper149@ip185225.wh.uni-hannover.de) |
| 02:09:09 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 272 seconds) |
| 02:09:57 | × | wwwww quits (~wwwww@unaffiliated/wwwww) (Ping timeout: 260 seconds) |
| 02:10:09 | <sim590> | dolio: Yes, but what if I make some other mistakes that it could find for me and I have disabled it? |
| 02:10:47 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 244 seconds) |
| 02:10:47 | × | jumper149 quits (~jumper149@ip185225.wh.uni-hannover.de) (Client Quit) |
| 02:11:03 | × | denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Ping timeout: 240 seconds) |
| 02:11:24 | → | denisse joins (~spaceCat@gateway/tor-sasl/alephzer0) |
| 02:12:13 | → | wwwww joins (~wwwww@unaffiliated/wwwww) |
| 02:15:38 | × | gnumonik quits (~gnumonik@c-73-170-91-210.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 02:16:48 | × | bloodsta1ker quits (~bloodstal@46.166.187.178) (Remote host closed the connection) |
| 02:17:19 | → | toorevitimirp joins (~tooreviti@117.182.182.33) |
| 02:27:20 | → | machinedgod joins (~machinedg@24.51.251.11) |
| 02:28:07 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 02:33:03 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Killed (verne.freenode.net (Nickname regained by services))) |
| 02:33:10 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 02:34:39 | × | toorevitimirp quits (~tooreviti@117.182.182.33) (Remote host closed the connection) |
| 02:37:14 | → | toorevitimirp joins (~tooreviti@117.182.182.33) |
| 02:37:54 | → | elliott_ joins (~elliott@2607:fb90:18d6:fc61:a84:10d2:ef86:f415) |
| 02:38:02 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 02:39:02 | <lechner> | Hi, in a new standard stack setup, are the files stack.yaml.lock and *.cabal generated? I would like to add them to .gitignore. Thanks! |
| 02:43:03 | <glguy> | The .cabal is generated if you have a package.yaml, but these days it's better to stick with deleting the package.yaml and maintaining the .cabal file |
| 02:46:40 | <lechner> | glguy: thanks! |
| 02:48:25 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 02:52:38 | × | manjaroi3 quits (~manjaro-i@2600:1700:9f00:b3df:a02:eef:be70:88de) (Remote host closed the connection) |
| 02:52:53 | × | machinedgod quits (~machinedg@24.51.251.11) (Ping timeout: 260 seconds) |
| 02:56:52 | → | gestone joins (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) |
| 02:57:24 | × | ryansmccoy quits (~ryansmcco@68.235.48.108) (Ping timeout: 272 seconds) |
| 02:58:06 | × | a3f quits (~a3f@chimeria.ext.pengutronix.de) (Ping timeout: 246 seconds) |
| 02:58:18 | → | ryansmccoy joins (~ryansmcco@193.37.254.27) |
| 02:59:53 | → | a3f joins (~a3f@chimeria.ext.pengutronix.de) |
| 02:59:54 | → | __Joker joins (~Joker@180.151.105.65) |
| 03:00:02 | × | toony1 quits (~toony@s91904426.blix.com) () |
| 03:01:17 | × | theDon quits (~td@muedsl-82-207-238-084.citykom.de) (Ping timeout: 260 seconds) |
| 03:02:49 | → | zacts joins (~zacts@dragora/developer/zacts) |
| 03:03:03 | → | theDon joins (~td@muedsl-82-207-238-073.citykom.de) |
| 03:05:26 | × | toorevitimirp quits (~tooreviti@117.182.182.33) (Remote host closed the connection) |
| 03:05:45 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 240 seconds) |
| 03:06:41 | → | toorevitimirp joins (~tooreviti@117.182.182.33) |
| 03:11:38 | × | polyrain quits (~polyrain@2001:8003:e501:6901:a8a8:546d:e1e3:2f7b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:11:59 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 03:13:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 03:13:59 | → | tylerjl joins (~leothrix@elastic/staff/leothrix) |
| 03:14:04 | × | toorevitimirp quits (~tooreviti@117.182.182.33) (Remote host closed the connection) |
| 03:14:24 | → | pera joins (~pera@unaffiliated/pera) |
| 03:14:41 | → | wei2912 joins (~wei2912@unaffiliated/wei2912) |
| 03:15:59 | → | bitmagie joins (~Thunderbi@200116b806ecb800483bd36953a84bd2.dip.versatel-1u1.de) |
| 03:16:01 | → | polyrain joins (~polyrain@2001:8003:e501:6901:a8a8:546d:e1e3:2f7b) |
| 03:16:18 | → | toorevitimirp joins (~tooreviti@117.182.182.33) |
| 03:17:40 | × | leothrix quits (~leothrix@elastic/staff/leothrix) (Ping timeout: 272 seconds) |
| 03:17:41 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 03:18:31 | × | z0_ quits (~z0@bl15-35-201.dsl.telepac.pt) (Quit: Lost terminal) |
| 03:18:55 | × | p-core quits (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) (Remote host closed the connection) |
| 03:19:12 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) () |
| 03:19:12 | → | p-core joins (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) |
| 03:21:32 | × | polyrain quits (~polyrain@2001:8003:e501:6901:a8a8:546d:e1e3:2f7b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:24:44 | × | toorevitimirp quits (~tooreviti@117.182.182.33) (Remote host closed the connection) |
| 03:26:15 | → | toorevitimirp joins (~tooreviti@117.182.182.33) |
| 03:26:43 | × | toorevitimirp quits (~tooreviti@117.182.182.33) (Read error: Connection reset by peer) |
| 03:28:09 | → | toorevitimirp joins (~tooreviti@117.182.182.33) |
| 03:28:09 | → | __Joker joins (~Joker@180.151.105.65) |
| 03:28:35 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 03:31:58 | hackage | stm-queue 0.1.1.0 - An implementation of a real-time concurrent queue https://hackage.haskell.org/package/stm-queue-0.1.1.0 (sgschlesinger) |
| 03:33:09 | → | abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) |
| 03:34:25 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 260 seconds) |
| 03:35:52 | × | silver quits (~silver@178.121.68.26) (Read error: Connection reset by peer) |
| 03:37:54 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 03:38:06 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 03:38:26 | → | bitmagie1 joins (~Thunderbi@200116b8062b2e00fc59d02ac7bcf06a.dip.versatel-1u1.de) |
| 03:39:32 | × | bitmagie quits (~Thunderbi@200116b806ecb800483bd36953a84bd2.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 03:39:33 | bitmagie1 | is now known as bitmagie |
| 03:43:00 | × | zacts quits (~zacts@dragora/developer/zacts) (Ping timeout: 272 seconds) |
| 03:44:04 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection) |
| 03:44:32 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 03:45:15 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 03:47:57 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 03:50:27 | × | jedws quits (~jedws@121.209.139.222) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 03:50:37 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 03:54:11 | → | sepi joins (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) |
| 03:55:08 | <sepi> | Hello guys, why doesn't this return false after running out of elements in a list? |
| 03:55:24 | <sepi> | memb x [] = Falsememb x (y:ys) | x `elem` y:ys = True | otherwise = memb x (y:ys) |
| 03:55:33 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection) |
| 03:55:58 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 03:57:11 | → | r2wj joins (~r2wj@185.244.214.216) |
| 03:57:43 | <dolio> | Because it can't run out. |
| 03:58:08 | <ski> | it's an infinite loop, in case the element isn't there |
| 03:59:03 | <ski> | > let memb x [] = False; memb x (y:ys) | x `elem` y:ys = True | otherwise = memb x (y:ys) in memb 3 [] |
| 03:59:05 | <lambdabot> | False |
| 03:59:14 | <ski> | > let memb x [] = False; memb x (y:ys) | x `elem` y:ys = True | otherwise = memb x (y:ys) in memb 3 [0,2,3,1] |
| 03:59:17 | <lambdabot> | True |
| 03:59:21 | <ski> | > let memb x [] = False; memb x (y:ys) | x `elem` y:ys = True | otherwise = memb x (y:ys) in memb 3 [0,2,1] |
| 03:59:27 | <lambdabot> | mueval-core: Time limit exceeded |
| 03:59:41 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Ping timeout: 256 seconds) |
| 04:00:01 | <ski> | sepi : do you see why it loops ? |
| 04:00:37 | → | Rudd0 joins (~Rudd0@185.189.115.118) |
| 04:00:45 | <lechner> | Hi, I would like to abstract the calls to the three hash calculations in this code and get the warnings below it. Can I not include 'do' in the function? https://dpaste.com/4ZCGYR975 |
| 04:00:59 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection) |
| 04:01:25 | <sepi> | Yeah it checks if its in there, if its not it'll keep calling itself. I suppose I want to know how to stop if it reaches the end of the list |
| 04:01:39 | <ski> | compute :: (Char8.ByteString -> Char8.ByteString) -> String -> Char8.ByteString |
| 04:01:42 | <ski> | should be |
| 04:01:43 | <ski> | compute :: (Char8.ByteString -> Char8.ByteString) -> String -> IO Char8.ByteString |
| 04:02:13 | × | bitmagie quits (~Thunderbi@200116b8062b2e00fc59d02ac7bcf06a.dip.versatel-1u1.de) (Quit: bitmagie) |
| 04:02:15 | <lechner> | ski: i thought the <- drops the IO? |
| 04:02:17 | <ski> | sepi : make sure you take a step forward, rather than walking in place, standing still |
| 04:02:19 | × | denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Remote host closed the connection) |
| 04:02:22 | <ski> | no, lechner |
| 04:02:35 | → | denisse joins (~spaceCat@gateway/tor-sasl/alephzer0) |
| 04:02:40 | <ski> | the whole `do'-expression will still have type `IO T', for some type `T' |
| 04:02:47 | <ski> | (you can't escape) |
| 04:03:40 | × | DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection) |
| 04:03:50 | <ski> | btw, probably it's better to give a name to `Char8.pack contents', in order to not recompute it ? |
| 04:03:59 | <ski> | (in `main', i mean) |
| 04:04:09 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 04:05:02 | <ski> | sepi : also .. if you care to tell, what is `memb' supposed to compute ? |
| 04:05:15 | <lechner> | i thought perhaps the compiler would be smart enough not to, although I thought that the 'effect' from readFile may force it. |
| 04:05:40 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 04:05:53 | <ski> | lechner : anyway, if you move the `readFile' out of `compute', you can probably avoid the `IO' in its return type |
| 04:05:53 | × | denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Remote host closed the connection) |
| 04:06:09 | → | denisse joins (~spaceCat@gateway/tor-sasl/alephzer0) |
| 04:06:22 | <lechner> | i will, but bear with me for a minute please. i changed the code the way you said, but now the code below fails even though i did not change it. |
| 04:06:26 | <sepi> | like if x = ["abc", "def"]. memb says is ["def"] in x? |
| 04:06:34 | <sepi> | True |
| 04:06:51 | <lechner> | https://dpaste.com/553FLPZG5 |
| 04:06:54 | <ski> | lechner : smart enough not to do what ? recompute the calls to `Char8.pack' ? or reread the file ? |
| 04:07:03 | × | ChaiTRex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Ping timeout: 240 seconds) |
| 04:07:04 | × | toorevitimirp quits (~tooreviti@117.182.182.33) (Ping timeout: 272 seconds) |
| 04:07:17 | <ski> | sepi : now try `memb "ghij" x' |
| 04:07:47 | <lechner> | ski: i thought the effectful action of readFile might retrigger the remaining computation, but without that the compiler should not repack |
| 04:08:14 | → | shad0w_ joins (~shad0w_@160.202.36.27) |
| 04:08:16 | <ski> | GHC only does limited CSE |
| 04:08:21 | → | ChaiTRex joins (~ChaiTRex@gateway/tor-sasl/chaitrex) |
| 04:09:22 | <ski> | lechner : anyway, the second error message is because you still have a mistake in `compute'. but perhaps you want to keep the `IO' out of it ? |
| 04:09:22 | <sepi> | It'll just sit there and I have to suspend it rather than being false |
| 04:09:54 | <ski> | (in that case, it would be better to fix that first. although, if you want to, you could fix the other error) |
| 04:10:02 | <ski> | sepi : and why's that ? |
| 04:10:18 | <lechner> | ski: i see. sorry i misread the error message. it's my first day with Haskell |
| 04:10:33 | <ski> | it's okay |
| 04:10:55 | <ski> | it's not that uncommon that fixing an error in one place will trigger an error to be flagged in another location |
| 04:11:29 | <ski> | sometimes it can be hard to know whether one will get out of the "tunnel(s) of error", fixing one after the other |
| 04:11:40 | <ski> | with more experience, you should be able to tell this, quicker |
| 04:12:12 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 260 seconds) |
| 04:12:25 | <lechner> | ski: How do I add the IO to the result? |
| 04:13:03 | <sepi> | its going to keep looking for the match because recursion, because I suppose there isn't a "if it reaches end, false" statement |
| 04:13:18 | <lechner> | and why is the expected type now without the IO even though I just added it up top? |
| 04:13:56 | <ski> | (this effect can also be noticed, when refactoring, changing the type signature. this can often trigger an error in other places, and fixing those can trigger further errors, like a ripple effect. this is normally a good thing, the implementation telling you all places you must fix, after having changed one place, in order to not encounter problems when running the code) |
| 04:14:32 | × | elliott_ quits (~elliott@2607:fb90:18d6:fc61:a84:10d2:ef86:f415) (Ping timeout: 260 seconds) |
| 04:14:52 | <lechner> | but why did it not accept the actual type without the IO in the first place. just because of the 'do'? |
| 04:15:16 | <ski> | sepi : there is a "if it reaches end, false" case, that's `memb x [] = False'. the problem is that you never take a step closer to it, you're moving your legs up and down, standing still |
| 04:16:04 | <ski> | lechner : "but why did it not accept the actual type without the IO in the first place. just because of the 'do'?" -- no, because of the `readFile' |
| 04:16:14 | × | danso quits (~dan@107-190-41-58.cpe.teksavvy.com) (Read error: Connection reset by peer) |
| 04:16:32 | <ski> | "How do I add the IO to the result?" -- result of what ? `compute' ? |
| 04:16:50 | <lechner> | hashMethod $ Char8.pack contents |
| 04:16:52 | → | danso joins (~dan@107-190-41-58.cpe.teksavvy.com) |
| 04:17:07 | <ski> | "and why is the expected type now without the IO even though I just added it up top?" -- what do you mean ? in <https://dpaste.com/553FLPZG5>, the expected type does have an `IO' |
| 04:17:20 | <ski> | lechner : `return :: a -> IO a' |
| 04:17:26 | <lechner> | yes, but only because I added it up top |
| 04:17:34 | → | jedws joins (~jedws@121.209.139.222) |
| 04:18:06 | <lechner> | thanks. where do I place this return statement, please? and do I retain the name 'a'? |
| 04:18:13 | <ski> | it's complaining that `hashMethod :: Char8.ByteString -> Char8.ByteString', while you're attempting to use it as if it was `hashMethod :: Char8.ByteString -> IO Char8.ByteString' |
| 04:18:24 | <lechner> | right |
| 04:18:44 | <ski> | `a' is a type variable. in your case, `a' would become `Char8.ByteString' |
| 04:19:01 | <ski> | (so that you get `return :: Char8.ByteString -> IO Char8.ByteString' ..) |
| 04:19:54 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 04:19:57 | → | drbean joins (~drbean@TC210-63-209-59.static.apol.com.tw) |
| 04:20:25 | <ski> | (another way to fix the type mismatch for `hashMethod' would be to change the signature of `compute' so that the specified callback (that's `hashMethod'), actually had type `Char8.ByteString -> IO Char8.ByteString' .. but i'm not convinced you actually want to do this) |
| 04:21:07 | → | Saukk joins (~Saukk@2001:998:dc:4a67:1c59:9bb5:b94c:4) |
| 04:21:09 | <lechner> | I will eventually remove the IO out of that function. right now, I am just learning. Where does that return statement go, please? |
| 04:21:14 | × | jedws quits (~jedws@121.209.139.222) (Client Quit) |
| 04:21:29 | <lechner> | and is this thing still called a function? |
| 04:21:52 | <ski> | (usually, especially as a beginner, one should think twice, before putting `IO' inside argument types. it's not that it's dangerous, but rather that it adds extra power, with possibility for extra confusion, that one relatively rarely needs) |
| 04:22:01 | <ski> | `compute' ? sure |
| 04:22:11 | <ski> | `hashMethod' as well |
| 04:22:11 | <lechner> | i agree with that |
| 04:22:34 | <lechner> | i thought perhaps the 'do' would turn compute into a monad |
| 04:22:38 | <ski> | no |
| 04:22:55 | <ski> | monads are not values that you deal with, at run-time |
| 04:22:58 | hackage | reanimate 1.0.0.0 - Animation library based on SVGs. https://hackage.haskell.org/package/reanimate-1.0.0.0 (DavidHimmelstrup) |
| 04:23:06 | <ski> | take e.g. `getLine :: IO String' |
| 04:23:15 | <ski> | `getLine' is not a monad. `IO' is the monad |
| 04:23:23 | <lechner> | i see. that's not a monad either |
| 04:23:28 | <lechner> | or is it? |
| 04:23:28 | <ski> | `getLine' is a monadic action, or just action, for short |
| 04:23:35 | <ski> | if you have |
| 04:23:39 | <ski> | compute :: (Char8.ByteString -> Char8.ByteString) -> String -> IO Char8.ByteString |
| 04:23:43 | <lechner> | the IO is the monad? |
| 04:23:57 | <ski> | then `compute hashMethod fileName' will also be an action. an `IO'-action (since `IO' is the monad here) |
| 04:24:00 | <ski> | yes |
| 04:24:32 | <ski> | the type `IO' (together with its instance of the `Monad' type class) is the monad |
| 04:25:07 | <lechner> | okay, sorry to be persistent. in which line do i stick that return statement, please? |
| 04:25:17 | <ski> | so .. `compute' is a function that computes/returns an action |
| 04:25:41 | <sepi> | I know I would want (y:ys) to be where y gets thrown out, next in ys becomes y. Now I'm trying to figure out how to translate that over |
| 04:25:50 | <ski> | the line in which you currently need `IO Blah', while you actually only have something of type `Blah' in |
| 04:26:12 | <ski> | sepi : perhaps try throwing out `y', then |
| 04:26:13 | <lechner> | so it goes before, which makes it kind of ling |
| 04:26:19 | <lechner> | long |
| 04:26:51 | <ski> | you mean the line of code ? |
| 04:27:16 | <lechner> | i am sticking in before the last line of compute |
| 04:28:05 | <lechner> | something is wrong |
| 04:29:07 | × | Orbstheorem quits (~roosember@hellendaal.orbstheorem.ch) (Ping timeout: 240 seconds) |
| 04:29:13 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 04:29:54 | <ski> | sepi : btw, you didn't say what `memb' is supposed to compute |
| 04:31:30 | ski | idly wonders what lechner is trying |
| 04:31:35 | × | ambiso quits (~ambiso@209.182.239.205) (Quit: Ping timeout (120 seconds)) |
| 04:31:54 | → | ambiso joins (~ambiso@209.182.239.205) |
| 04:32:15 | <sepi> | its supposed to compute true or false, saying true"abc" is in there, or false it isn't in there |
| 04:32:15 | × | irc_user quits (uid423822@gateway/web/irccloud.com/x-yamugsoddzfdaipx) (Quit: Connection closed for inactivity) |
| 04:32:20 | <lechner> | i feel so dumb. i can't put this line in the right place: return :: Char8.ByteString -> IO Char8.ByteString |
| 04:32:22 | <sepi> | I think I got it though |
| 04:33:00 | <sepi> | Thanks I was here for a few hours to get to this point, appreciate your push in the right direction |
| 04:33:03 | <ski> | sepi : what is `memb x ys' supposed to compute, for an arbitrary `x' and list `ys' ? |
| 04:34:09 | <ski> | lechner : oh, i should clarify that i only intended you to use `return'. the `:: Char8.ByteString -> IO Char8.ByteString' was only a clarification, to tell you what type it would have, in your case |
| 04:34:24 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 04:34:28 | <ski> | sepi : show the code ? |
| 04:35:37 | <ski> | (if you really want to, you could type in `return :: Char8.ByteString -> IO Char8.ByteString' .. but you'd have to bracket it like `(return :: Char8.ByteString -> IO Char8.ByteString)') |
| 04:37:33 | <lechner> | i was just missing some parentheses (or perhaps a dollar sign). return is a function! |
| 04:37:39 | <ski> | yes, of course |
| 04:37:44 | <ski> | it has a `->' in its type |
| 04:38:08 | <ski> | all values whose types are of the general shape `... -> ...' are functions |
| 04:38:09 | <lechner> | doesn't everything in Haskell? :) |
| 04:38:14 | <ski> | (and only those are functions) |
| 04:38:18 | <lechner> | just kidding |
| 04:38:37 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:7d39:b02b:8868:9bea) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 04:38:46 | <ski> | yea .. "Everything is a function" does not hold in the Functional Programming paradigm |
| 04:38:58 | <lechner> | it was a bad joke |
| 04:39:00 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 04:39:55 | <ski> | see <http://conal.net/blog/posts/everything-is-a-function-in-haskell> :) |
| 04:41:00 | <ski> | lechner : so .. how does your `compute' look, now ? |
| 04:41:15 | <sepi> | memb x [] = Falsememb x (y:ys) | x `elem` y:ys = True | otherwise = mMemb where mMemb = memb x (ys) |
| 04:41:56 | <ski> | that's better |
| 04:42:17 | <lechner> | ski: it's working. https://dpaste.com/CBE8R6EU2 |
| 04:42:20 | <ski> | sepi : although that code not had redundant functionality |
| 04:42:22 | <ski> | er |
| 04:42:25 | <ski> | sepi : although that code now had redundant functionality |
| 04:42:32 | <lechner> | ski: I am just getting the hang of it. thanks so much for your help. |
| 04:43:08 | <lechner> | ski: i'll be back. my first day with haskell is ending, and it's time to call it a night. |
| 04:43:09 | <sepi> | the extra where part? |
| 04:43:10 | <ski> | lechner : yea. btw, i would probably write that last line as `return (hashMethod (Char8.pack contents))' |
| 04:43:27 | <lechner> | that's what I had. why is that superior, please? |
| 04:43:33 | <ski> | sepi : no, not that |
| 04:43:48 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 04:44:12 | <ski> | sepi : can you tell me, in words, what `memb x ys' is supposed to compute/check ? |
| 04:44:25 | <ski> | lechner : it uses less `$'s :) |
| 04:44:43 | → | Orbstheorem joins (~roosember@hellendaal.orbstheorem.ch) |
| 04:44:47 | <ski> | `$' rarely improve code, imho |
| 04:44:58 | <sepi> | the x = y:ys ? |
| 04:45:11 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) |
| 04:45:19 | → | __Joker joins (~Joker@180.151.105.65) |
| 04:45:26 | <ski> | sepi : that question was not about your code, but about what behaviour your code is supposed to have |
| 04:46:03 | <lechner> | thanks again for all your help! unfortunately, i have to go but thanks to you my experience in this channel was super |
| 04:46:06 | <sepi> | Its supposed to check if what's given in x is in the ys list |
| 04:46:07 | → | brandly joins (~brandly@c-73-68-15-46.hsd1.ma.comcast.net) |
| 04:46:35 | <ski> | lechner : in general, it's probably better to replace `f $ g $ h $ x' with `f . g . h $ x' or (i prefer) `(f . g . h) x' .. or just `f (g (h x))' (brackets are nothing to be afraid of) |
| 04:46:54 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) (Client Quit) |
| 04:47:22 | <ski> | lechner : the `f . g . h' "chain"/"pipeline" is better, since you can break out and factor away any part of it, giving it a new name. not so with the repeated `$'s |
| 04:47:58 | <ski> | lechner : have fun, and good luck with your continued learning |
| 04:48:08 | <ski> | sepi : yes, thank you |
| 04:48:39 | <ski> | sepi : now, what is x `elem` ys supposed to compute/check ? |
| 04:52:01 | × | perrier-jouet quits (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) (Quit: WeeChat 2.9) |
| 04:52:12 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) |
| 04:53:27 | hackage | tagstew 0 - Black magic tagsoup https://hackage.haskell.org/package/tagstew-0 (FumiakiKinoshita) |
| 04:54:14 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 04:55:57 | × | Orbstheorem quits (~roosember@hellendaal.orbstheorem.ch) (Ping timeout: 260 seconds) |
| 04:57:42 | <sepi> | I see that is my redundant part 😅 |
| 04:59:09 | <sepi> | I'm not sure without my = true, my | becomes a parse error input |
| 04:59:40 | <ski> | how do you mean ? |
| 05:01:54 | → | mmohammadi981261 joins (~mmohammad@5.238.182.51) |
| 05:02:15 | <sepi> | does it need a true or false claim before using otherwise? |
| 05:02:30 | × | urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna) |
| 05:02:32 | <ski> | a guard, introduced by the |
| 05:02:56 | <ski> | `|' symbol, expects an expresion evaluating to `True' or `False', after it, yes |
| 05:04:40 | × | shad0w_ quits (~shad0w_@160.202.36.27) (Remote host closed the connection) |
| 05:05:58 | <sepi> | memb x (y:ys) | x == y = True | otherwise = mMemb |
| 05:06:21 | <sepi> | that gets rid of redundancy correct |
| 05:06:22 | <ski> | yay :) |
| 05:06:28 | <ski> | yes |
| 05:07:11 | <sepi> | 💀💀 thank you |
| 05:07:16 | <ski> | now, do you know how to express this using, say, `if'-`then'-`else', instead of guards ? |
| 05:07:24 | <ski> | (or any other way ?) |
| 05:07:28 | hackage | typesafe-precure 0.7.9.1 - Type-safe transformations and purifications of PreCures (Japanese Battle Heroine) https://hackage.haskell.org/package/typesafe-precure-0.7.9.1 (igrep) |
| 05:08:20 | × | mmohammadi981261 quits (~mmohammad@5.238.182.51) (Quit: I quit (╯°□°）╯︵ ┻━┻) |
| 05:08:25 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-157-9.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection) |
| 05:08:32 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:64a7:3952:c5b0:2946) (Ping timeout: 260 seconds) |
| 05:09:49 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-55-157-9.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 05:11:41 | × | HarveyPwca quits (~HarveyPwc@c-98-220-98-201.hsd1.il.comcast.net) (Quit: Leaving) |
| 05:13:24 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 05:13:26 | → | Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 05:14:12 | × | Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 272 seconds) |
| 05:14:48 | Lord_of_Life_ | is now known as Lord_of_Life |
| 05:16:31 | <sepi> | I know how I'd want to do it conceptually but I'm not too sure on the syntax |
| 05:17:18 | → | abaiste^ joins (abaiste@ip98-184-89-2.mc.at.cox.net) |
| 05:18:01 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 05:18:40 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 05:20:16 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:e941:4ff:7183:882c) |
| 05:22:44 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 05:23:00 | <sepi> | If you could show an example or reference that's similar to my function that'd be cool. I'll be heading to bed for the night soon |
| 05:27:02 | → | rihards joins (~rihards@balticom-142-78-50.balticom.lv) |
| 05:27:13 | × | Alleria_ quits (~AllahuAkb@2604:2000:1484:26:1c6a:a4a1:e2e0:f856) (Ping timeout: 244 seconds) |
| 05:27:19 | <c_wraith> | sepi: it's easier than you might think. memb x (y:ys) = if ... then ... else ... |
| 05:28:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 05:28:54 | → | Alleria_ joins (~AllahuAkb@2604:2000:1484:26:f9f7:186a:b38:3c1e) |
| 05:29:49 | × | ryansmccoy quits (~ryansmcco@193.37.254.27) (Ping timeout: 260 seconds) |
| 05:30:47 | → | ryansmccoy joins (~ryansmcco@156.96.151.132) |
| 05:33:19 | → | gestone joins (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) |
| 05:33:54 | × | abaiste^ quits (abaiste@ip98-184-89-2.mc.at.cox.net) () |
| 05:36:12 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 05:39:47 | × | brandly quits (~brandly@c-73-68-15-46.hsd1.ma.comcast.net) (Ping timeout: 240 seconds) |
| 05:40:04 | × | sepi quits (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) (Ping timeout: 245 seconds) |
| 05:41:34 | → | eric joins (~eric@2804:431:c7d4:402a:4dc9:97ef:220b:73aa) |
| 05:43:03 | × | drbean quits (~drbean@TC210-63-209-59.static.apol.com.tw) (Read error: Connection reset by peer) |
| 05:43:14 | × | Rudd0 quits (~Rudd0@185.189.115.118) (Ping timeout: 260 seconds) |
| 05:44:16 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 05:44:27 | → | moondaddi joins (3ae9ffcb@58.233.255.203) |
| 05:45:24 | → | drbean joins (~drbean@TC210-63-209-213.static.apol.com.tw) |
| 05:45:45 | × | eric quits (~eric@2804:431:c7d4:402a:4dc9:97ef:220b:73aa) (Ping timeout: 246 seconds) |
| 05:48:45 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 05:48:49 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 260 seconds) |
| 05:49:40 | → | __Joker joins (~Joker@180.151.105.65) |
| 05:52:55 | → | Saten-san joins (~Saten-san@ip-83-134-68-146.dsl.scarlet.be) |
| 05:56:34 | × | roconnor quits (~roconnor@host-45-78-192-132.dyn.295.ca) (Ping timeout: 256 seconds) |
| 05:56:51 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 05:57:31 | × | evanjs quits (~evanjs@075-129-188-019.res.spectrum.com) (Quit: ZNC 1.8.1 - https://znc.in) |
| 06:00:02 | × | r2wj quits (~r2wj@185.244.214.216) () |
| 06:00:32 | → | evanjs joins (~evanjs@075-129-188-019.res.spectrum.com) |
| 06:00:47 | × | xff0x_ quits (~fox@2001:1a81:53ac:b300:4ccb:e51f:bb16:7d67) (Ping timeout: 246 seconds) |
| 06:01:37 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 06:01:45 | → | xff0x_ joins (~fox@port-92-195-46-13.dynamic.as20676.net) |
| 06:01:47 | → | notzmv` joins (~user@177.103.86.92) |
| 06:02:50 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 06:04:49 | × | notzmv quits (~user@unaffiliated/zmv) (Disconnected by services) |
| 06:04:55 | notzmv` | is now known as notzmv |
| 06:05:00 | × | notzmv quits (~user@177.103.86.92) (Changing host) |
| 06:05:00 | → | notzmv joins (~user@unaffiliated/zmv) |
| 06:05:55 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 06:07:29 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Ping timeout: 260 seconds) |
| 06:07:39 | × | Saukk quits (~Saukk@2001:998:dc:4a67:1c59:9bb5:b94c:4) (Remote host closed the connection) |
| 06:07:43 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 06:08:43 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 06:10:45 | × | gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 06:11:17 | × | gienah quits (~mwright@gentoo/developer/gienah) (Quit: leaving) |
| 06:12:42 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 246 seconds) |
| 06:15:06 | → | mirrorbird joins (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2) |
| 06:15:38 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-131-172.cust.tzulo.com) (Ping timeout: 272 seconds) |
| 06:16:20 | × | Volt_ quits (~Volt_@c-73-145-164-70.hsd1.mi.comcast.net) (Quit: ) |
| 06:17:13 | → | TooDifficult joins (~TooDiffic@139.59.59.230) |
| 06:17:28 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 06:17:58 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 06:22:38 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 06:23:58 | → | ggole joins (~ggole@2001:8003:8119:7200:a81f:ad25:a0f4:9303) |
| 06:26:44 | × | moondaddi quits (3ae9ffcb@58.233.255.203) (Ping timeout: 245 seconds) |
| 06:26:55 | → | gestone joins (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) |
| 06:33:32 | → | polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) |
| 06:35:01 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Ping timeout: 264 seconds) |
| 06:37:40 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 06:38:04 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 06:38:46 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 06:43:05 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 06:43:52 | × | kleisli_ quits (~kleisli@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Ping timeout: 260 seconds) |
| 06:47:37 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 06:48:42 | × | TooDifficult quits (~TooDiffic@139.59.59.230) (Ping timeout: 258 seconds) |
| 06:51:06 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:52:17 | → | nehsou^ joins (nehsou@ip98-184-89-2.mc.at.cox.net) |
| 06:56:26 | → | jjj joins (~jjj@178.239.168.171) |
| 06:56:48 | → | ph88 joins (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) |
| 06:57:08 | → | TooDifficult joins (~TooDiffic@139.59.59.230) |
| 06:58:05 | × | Saten-san quits (~Saten-san@ip-83-134-68-146.dsl.scarlet.be) (Quit: WeeChat 2.8) |
| 06:59:38 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 07:01:09 | × | ph88 quits (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 07:01:40 | → | shafox joins (~shafox@106.51.234.111) |
| 07:02:09 | × | TooDifficult quits (~TooDiffic@139.59.59.230) (Quit: TooDifficult) |
| 07:02:57 | → | TooDifficult joins (~TooDiffic@139.59.59.230) |
| 07:03:57 | hackage | webauthn 0 - Web Authentication API https://hackage.haskell.org/package/webauthn-0 (FumiakiKinoshita) |
| 07:04:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 07:05:45 | × | nehsou^ quits (nehsou@ip98-184-89-2.mc.at.cox.net) () |
| 07:07:04 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:09:21 | → | tsrt^ joins (tsrt@ip98-184-89-2.mc.at.cox.net) |
| 07:11:47 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 07:13:58 | × | Maxdamantus quits (~Maxdamant@unaffiliated/maxdamantus) (Ping timeout: 256 seconds) |
| 07:15:39 | × | codygman quits (~codygman@47-184-107-46.dlls.tx.frontiernet.net) (Read error: Connection reset by peer) |
| 07:15:54 | → | codygman joins (codygman@gateway/vpn/privateinternetaccess/codygman) |
| 07:15:55 | × | codygman quits (codygman@gateway/vpn/privateinternetaccess/codygman) (Client Quit) |
| 07:15:55 | → | Maxdamantus joins (~Maxdamant@unaffiliated/maxdamantus) |
| 07:20:30 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 07:21:35 | × | danso quits (~dan@107-190-41-58.cpe.teksavvy.com) (Quit: WeeChat 2.9) |
| 07:25:18 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 07:28:26 | → | CMCDragonkai1 joins (~Thunderbi@120.17.10.7) |
| 07:41:07 | × | shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:c058:b9a7:8857:8837) (Ping timeout: 244 seconds) |
| 07:41:11 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 07:42:06 | → | mmohammadi981261 joins (~mmohammad@2.178.205.88) |
| 07:43:02 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:45:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 07:45:42 | × | proteusguy quits (~proteusgu@cm-58-10-208-180.revip7.asianet.co.th) (Ping timeout: 256 seconds) |
| 07:47:14 | → | shutdown_-h_now joins (~arjan@2001:1c06:2d0b:2312:b1b9:b40:f655:8986) |
| 07:48:19 | × | lambda-11235 quits (~lambda-11@108-237-120-58.lightspeed.frokca.sbcglobal.net) (Quit: Bye) |
| 07:48:20 | → | danvet_ joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) |
| 07:50:17 | Guest38587 | is now known as lep-delete |
| 07:50:18 | lep-delete | is now known as Guest38587 |
| 07:50:18 | Guest38587 | is now known as lep-delete |
| 07:50:20 | <perdent> | How would you decode this Cistercian Monk Numerals cipher from this image programtically? https://imgur.com/lWxfMHf https://www.dcode.fr/cistercian-numbers |
| 07:51:24 | → | knupfer joins (~Thunderbi@i59F7FF48.versanet.de) |
| 07:52:44 | × | mmohammadi981261 quits (~mmohammad@2.178.205.88) (Ping timeout: 260 seconds) |
| 07:54:06 | × | tzh quits (~tzh@2601:448:c500:5300::ad1c) (Quit: zzz) |
| 07:54:49 | × | wavemode quits (~wavemode@097-070-075-143.res.spectrum.com) (Ping timeout: 264 seconds) |
| 07:56:28 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Quit: Goodbye) |
| 07:56:46 | → | asan joins (~yan4138@124.78.18.192) |
| 07:57:58 | → | proteusguy joins (~proteusgu@cm-58-10-208-180.revip7.asianet.co.th) |
| 08:00:07 | <cheater> | you mean with OCR? |
| 08:00:11 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-55-157-9.dhcp-dynamic.fibreop.nb.bellaliant.net) (Read error: Connection reset by peer) |
| 08:00:45 | × | blackfield quits (~blackfiel@unaffiliated/blackfield) (Quit: see you) |
| 08:01:42 | <perdent> | cheater: yeah, or is there an easier way? |
| 08:01:49 | × | ddellacosta quits (~dd@86.106.121.168) (Ping timeout: 260 seconds) |
| 08:02:04 | → | blackfield joins (~blackfiel@85.255.4.218) |
| 08:02:10 | <perdent> | Can't ffind any on github |
| 08:02:16 | <perdent> | That do this |
| 08:02:31 | <cheater> | why not just enter the data by hand? |
| 08:02:41 | <cheater> | do you have huge amounts of data to OCR? |
| 08:02:46 | × | blackfield quits (~blackfiel@85.255.4.218) (Changing host) |
| 08:02:46 | → | blackfield joins (~blackfiel@unaffiliated/blackfield) |
| 08:03:29 | <perdent> | I could doit by hand, would be nice to have a script to do it though |
| 08:03:52 | <perdent> | What did you get by hand? |
| 08:06:10 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 08:06:34 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 08:06:47 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 08:08:46 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 08:10:46 | → | jedws joins (~jedws@121.209.139.222) |
| 08:13:05 | → | shad0w_ joins (~shad0w_@160.202.36.27) |
| 08:13:19 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 272 seconds) |
| 08:13:24 | × | jedws quits (~jedws@121.209.139.222) (Client Quit) |
| 08:13:36 | <shad0w_> | Hi. i was following up on a link i was suggested to read here yesterday. https://wiki.haskell.org/How_to_write_a_Haskell_program |
| 08:14:08 | <shad0w_> | in the `program structure` section, it gives you a link for reading more about monad transformers. |
| 08:14:14 | <shad0w_> | that link seems to be dead. |
| 08:14:40 | <cheater> | are you new to haskell? |
| 08:14:48 | <shad0w_> | sure |
| 08:15:04 | <cheater> | don't read about monad transformers |
| 08:15:15 | <shad0w_> | lmao |
| 08:15:37 | <cheater> | just saving you a headache |
| 08:15:47 | <shad0w_> | just out of curosity. why ? |
| 08:16:10 | <shad0w_> | are they more complex than they are worth ? or they arent the preffered way anymore ? |
| 08:16:17 | <perdent> | i solved it |
| 08:16:28 | <cheater> | because it's an advanced topic you most certainly will not need for a long time, and any explanation you'll come across will likely be way over your head |
| 08:16:45 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 08:16:49 | <shad0w_> | gotcha |
| 08:16:54 | <shad0w_> | seems fair. |
| 08:17:49 | <perdent> | HTB{m0Nks_kN3w!} |
| 08:17:54 | <perdent> | is what i got |
| 08:18:15 | <cheater> | perdent: 🤷♂️ |
| 08:18:43 | <perdent> | capital M |
| 08:19:11 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:dcd7:c4bd:12f0:39d4) |
| 08:19:51 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:dcd7:c4bd:12f0:39d4) (Remote host closed the connection) |
| 08:22:14 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 08:22:18 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Read error: Connection reset by peer) |
| 08:22:27 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 08:22:45 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 08:23:48 | → | supercoven joins (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) |
| 08:24:13 | × | knupfer quits (~Thunderbi@i59F7FF48.versanet.de) (Ping timeout: 260 seconds) |
| 08:26:28 | <shad0w_> | i had another question. is cabal sandboxing still a thing ? |
| 08:26:39 | → | kleisli_ joins (~kleisli@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) |
| 08:27:05 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 08:27:55 | <shad0w_> | i can only find 1 command `v1-sandbox` in cabal help and its listed under `legacy commands` |
| 08:29:15 | <cheater> | yes, v1-sandbox is still a thing, it's what sandbox used to be |
| 08:29:27 | <cheater> | if you use v2-* commands, they work like a sandbox now |
| 08:29:29 | <int-e> | shad0w_: Barely, it'll be removed in version 3.4. You can presumably get a similar effect by manipulating the store directory. |
| 08:29:31 | <cheater> | but the sandboxes are global |
| 08:29:35 | <cheater> | ish |
| 08:29:39 | <cheater> | it's not really like that |
| 08:29:48 | × | pera quits (~pera@unaffiliated/pera) (Quit: leaving) |
| 08:29:51 | <cheater> | but for what you want, using v2-* commands is what you want if you were using sandboxes before |
| 08:30:03 | × | supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Max SendQ exceeded) |
| 08:30:06 | <cheater> | int-e's suggestion of manipulating the store dir isn't necessary |
| 08:30:17 | → | supercoven joins (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) |
| 08:30:29 | <int-e> | cheater: I *wanted* to keep local build artefacts. |
| 08:30:50 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 08:31:28 | <cheater> | int-e: shad0w_ is just a person new to haskell doing some basic projects. shad0w_ doesn't need to do any of that crazy stuff. |
| 08:31:29 | <shad0w_> | so, if hypothetically, i am writing a new project, doing cabal init will sandbox it to the very folder ? |
| 08:31:45 | <shad0w_> | cheater: +1 |
| 08:31:49 | <cheater> | shad0w_: not really, no. it will be global. but it will be done so that you don't get cabal hell |
| 08:32:27 | <shad0w_> | now suppose if 2 of my projects depend on the same dep but different version ? |
| 08:32:48 | <shad0w_> | for eg:- say hlint. |
| 08:32:57 | <shad0w_> | i just updated to 3.2 recently |
| 08:33:00 | <cheater> | you used to get cabal hell due to conflicting library versions. you don't get that anymore. every combination of versions is kept separate, so to speak. so two projects using the same exact lib versions will use the same build artefacts. but two projects using different lib versions will use separate lib artefacts and won't know about each other. |
| 08:33:35 | <shad0w_> | and globals can only be 1 copy right ? |
| 08:33:47 | <shad0w_> | like hlint is installed in .cabal/bin/hlint |
| 08:33:57 | <shad0w_> | it seems to be a symlink to a store folder |
| 08:35:46 | <cheater> | i forgot how that works |
| 08:35:53 | <cheater> | i just know you can set it up to work |
| 08:36:10 | <shad0w_> | cool |
| 08:36:15 | × | supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Max SendQ exceeded) |
| 08:36:27 | × | jjj quits (~jjj@178.239.168.171) (Remote host closed the connection) |
| 08:36:29 | <shad0w_> | tl;dr, sandboxing isn't necessary now ? |
| 08:36:33 | → | supercoven joins (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) |
| 08:36:49 | <cheater> | yes |
| 08:36:50 | <int-e> | cheater: fair enough, I should've asked why they want sandboxes first. |
| 08:36:52 | <cheater> | use v2-* |
| 08:36:58 | <cheater> | int-e: it's okay :) |
| 08:36:59 | → | acidjnk_new2 joins (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) |
| 08:37:08 | <shad0w_> | thanks @cheater |
| 08:37:09 | <cheater> | int-e: you were trying to help, that's what matters :) |
| 08:37:12 | <cheater> | yw shad0w_ |
| 08:37:51 | <shad0w_> | one more thing |
| 08:37:59 | <shad0w_> | there are v2- commands like you said. |
| 08:38:11 | <shad0w_> | there also happens to be some `new-` commands |
| 08:38:27 | <shad0w_> | do they succeed `v2-` commands ? |
| 08:38:59 | <shad0w_> | thanks @int-e too : ) |
| 08:39:32 | × | kori quits (~kori@arrowheads/kori) (Quit: WeeChat 2.8) |
| 08:39:50 | <int-e> | shad0w_: no, the new- command are the v2- commands |
| 08:40:46 | <cheater> | new-* is the current new stuff. once we have v3, new will refer to v3 and not v2 any more. |
| 08:40:49 | <cheater> | v2 is forever v2. |
| 08:40:52 | <cheater> | until it gets removed. |
| 08:40:52 | <int-e> | For historical reasons, the old commands were there, then the 'new-' commands were added. Then somebody realized that this will make the switch awkward, and the 'v1-' aliases for the old commands and the 'v2-' aliases for the new commands were added. |
| 08:41:09 | <int-e> | By now the 'v2-' commands are the default, and the 'new-' prefix is confusing. |
| 08:41:39 | <shad0w_> | so the new- seems like a pointer to the newest stuff, which just happens to be v2- in this case ? |
| 08:41:43 | → | Orbstheorem joins (~roosember@hellendaal.orbstheorem.ch) |
| 08:41:53 | <shad0w_> | while v2- is always hard v2- |
| 08:42:04 | <cheater> | yes |
| 08:42:09 | <shad0w_> | got it. |
| 08:42:21 | <shad0w_> | damn you guys are helpful. |
| 08:42:25 | <shad0w_> | : ) |
| 08:42:48 | <shad0w_> | happy weekend guys. |
| 08:42:58 | <int-e> | cheater: please tell me there are no current plans for a v3 set of cabal commands. |
| 08:43:00 | → | fendor joins (~fendor@212095005091.public.telering.at) |
| 08:43:06 | × | DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection) |
| 08:43:09 | <cheater> | int-e: not that i know of |
| 08:43:20 | <cheater> | int-e: but that's what i was told some time ago |
| 08:43:26 | <cheater> | you too shad0w_ |
| 08:43:40 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 08:43:51 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 08:45:33 | → | kori joins (~kori@arrowheads/kori) |
| 08:45:45 | → | coot joins (~coot@37.30.55.202.nat.umts.dynamic.t-mobile.pl) |
| 08:46:54 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 08:47:23 | → | knupfer1 joins (~Thunderbi@i59F7FF48.versanet.de) |
| 08:48:16 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 08:49:47 | knupfer1 | is now known as knupfer |
| 08:50:14 | × | coot quits (~coot@37.30.55.202.nat.umts.dynamic.t-mobile.pl) (Client Quit) |
| 08:50:30 | → | coot joins (~coot@37.30.55.202.nat.umts.dynamic.t-mobile.pl) |
| 08:51:02 | × | Orbstheorem quits (~roosember@hellendaal.orbstheorem.ch) (Ping timeout: 260 seconds) |
| 08:52:42 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 08:52:57 | → | jedws joins (~jedws@121.209.139.222) |
| 08:54:04 | → | kicov joins (959c7c03@nat.ds3.agh.edu.pl) |
| 08:58:19 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 246 seconds) |
| 08:58:37 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:e941:4ff:7183:882c) (Ping timeout: 260 seconds) |
| 09:00:09 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 09:00:38 | <kicov> | Hi, was just wondering how to approach doing things with State monad and liquid haskell. Let's say our state is int, and we'd like a check for a function `successor` that checks whether the current int is mod 2. If it is, then we return state+1, if it isn't, boom. |
| 09:00:52 | ← | stites[m] parts (stitesmatr@gateway/shell/matrix.org/x-yuspkxyvracibmrk) ("Kicked by @appservice-irc:matrix.org : Idle for 30+ days") |
| 09:04:28 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 09:07:03 | → | ph88 joins (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) |
| 09:08:58 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 09:09:04 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 09:10:59 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:2032:8cd9:bb36:4db2) |
| 09:11:28 | × | blackfield quits (~blackfiel@unaffiliated/blackfield) (Quit: see you) |
| 09:12:27 | → | hiroaki joins (~hiroaki@2a02:908:4b14:d500:8d4c:a111:9cac:718b) |
| 09:13:22 | → | Dolly joins (585fd1fd@ti0203q160-5312.bb.online.no) |
| 09:15:48 | × | asan quits (~yan4138@124.78.18.192) (Ping timeout: 256 seconds) |
| 09:17:52 | × | TooDifficult quits (~TooDiffic@139.59.59.230) (Quit: TooDifficult) |
| 09:18:09 | → | TooDifficult joins (~TooDiffic@139.59.59.230) |
| 09:18:16 | × | TooDifficult quits (~TooDiffic@139.59.59.230) (Remote host closed the connection) |
| 09:18:31 | → | TooDifficult joins (~TooDiffic@139.59.59.230) |
| 09:18:38 | → | oxide joins (~lambda@unaffiliated/mclaren) |
| 09:22:07 | × | TooDifficult quits (~TooDiffic@139.59.59.230) (Client Quit) |
| 09:22:58 | × | OscarZ quits (~oscarz@95.175.104.39) (Quit: Leaving) |
| 09:23:11 | × | unlink__ quits (~unlink2@p200300ebcf25bd0068eb9d9c94da2a17.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 09:24:22 | × | knupfer quits (~Thunderbi@i59F7FF48.versanet.de) (Ping timeout: 272 seconds) |
| 09:24:46 | → | unlink2 joins (~unlink2@p5dc0ae0e.dip0.t-ipconnect.de) |
| 09:25:01 | <ski> | kicov : sounds like you want to encode precondition and postcondition on the state, that is some kind of Hoare triple ? |
| 09:25:26 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 09:29:00 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 09:29:48 | → | kayvan`` joins (~user@52-119-115-243.PUBLIC.monkeybrains.net) |
| 09:30:01 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 09:30:59 | × | suppi quits (~suppi@172.246.241.246) (Ping timeout: 240 seconds) |
| 09:31:13 | × | kayvan` quits (~user@52-119-115-243.PUBLIC.monkeybrains.net) (Ping timeout: 246 seconds) |
| 09:31:36 | → | suppi joins (~suppi@2605:f700:40:c00::e6fc:6842) |
| 09:31:47 | × | drbean quits (~drbean@TC210-63-209-213.static.apol.com.tw) (Quit: ZNC 1.8.2+cygwin1 - https://znc.in) |
| 09:33:11 | × | mirrorbird quits (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2) (Quit: Leaving) |
| 09:33:34 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 244 seconds) |
| 09:34:02 | × | jedws quits (~jedws@121.209.139.222) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 09:38:11 | → | eric_ joins (~eric@2804:431:c7d4:402a:4dc9:97ef:220b:73aa) |
| 09:42:34 | → | ph88^ joins (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) |
| 09:42:42 | × | eric_ quits (~eric@2804:431:c7d4:402a:4dc9:97ef:220b:73aa) (Ping timeout: 260 seconds) |
| 09:43:05 | × | ph88 quits (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 09:46:06 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 09:48:06 | <dminuoso> | kicov: What is "boom"? |
| 09:50:33 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 09:53:28 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 09:55:37 | <kicov> | dminuoso: failed constraint |
| 09:56:44 | → | priyesh joins (~priyesh@84.39.117.57) |
| 09:57:18 | × | sw1nn quits (~sw1nn@host81-146-21-49.range81-146.btcentralplus.com) (Quit: WeeChat 2.9) |
| 09:58:07 | × | Sgeo quits (~Sgeo@ool-18b982ad.dyn.optonline.net) (Read error: Connection reset by peer) |
| 09:58:23 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 09:58:40 | → | sw1nn joins (~sw1nn@host81-146-21-49.range81-146.btcentralplus.com) |
| 09:59:39 | <ski> | kicov : so, what does "checks whether the current int is mod 2" mean ? |
| 10:00:35 | <kicov> | ski: Never heard of them, but that would be possible. Maybe continuation passing style could have a similiar problem |
| 10:01:17 | <kicov> | ski: i (the state) `mod` 2 == 0 |
| 10:01:39 | <kicov> | sorry, should be more clear |
| 10:01:43 | <dminuoso> | kicov: So what you're proposing is `successor :: State Int ()` with a matching LH signature that suggests that the *input* state is always even? |
| 10:01:51 | <ski> | kicov : <https://en.wikipedia.org/wiki/Hoare_logic> |
| 10:01:58 | <dminuoso> | kicov: Did I get that right? |
| 10:02:06 | → | Rudd0 joins (~Rudd0@185.189.115.103) |
| 10:02:23 | <kicov> | dminuoso : yep! |
| 10:02:28 | <ski> | presumably also that the output state is always odd, i'd gather |
| 10:02:51 | → | gestone joins (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) |
| 10:03:04 | <dminuoso> | Mmm, I wonder, is there some `liftState :: a -> a -> StateT a ()` function perhaps? |
| 10:03:05 | <ski> | (or maybe even that it's just the successor of the input) |
| 10:03:19 | <dminuoso> | Oh, State rather |
| 10:03:25 | <ski> | what would it do ? |
| 10:03:46 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 10:04:05 | <dminuoso> | Oh hah, that's just modify I guess |
| 10:04:19 | <ski> | oh .. i was beginning to wonder if it was missing some brackets |
| 10:04:29 | → | maroloccio joins (~marolocci@2a02:8084:601d:7f80:164f:8aff:fed8:411d) |
| 10:05:08 | <dminuoso> | Ah indeed, weird. |
| 10:05:08 | × | fendor quits (~fendor@212095005091.public.telering.at) (Remote host closed the connection) |
| 10:05:51 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 10:06:55 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 10:07:26 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Ping timeout: 256 seconds) |
| 10:07:28 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 10:07:51 | → | nyd joins (~nyd@unaffiliated/elysian) |
| 10:09:41 | × | ystael quits (~ystael@209.6.50.55) (Ping timeout: 260 seconds) |
| 10:11:52 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 10:13:47 | → | Rudd0^ joins (~Rudd0@185.189.115.108) |
| 10:14:37 | × | Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 264 seconds) |
| 10:18:42 | → | day joins (~Unknown@unaffiliated/day) |
| 10:20:41 | × | berberman quits (~berberman@2408:8207:256b:da50::a44) (Quit: ZNC 1.7.5 - https://znc.in) |
| 10:21:01 | → | gienah joins (~mwright@gentoo/developer/gienah) |
| 10:21:06 | × | Dolly quits (585fd1fd@ti0203q160-5312.bb.online.no) (Remote host closed the connection) |
| 10:21:50 | → | Rudd0 joins (~Rudd0@185.189.115.108) |
| 10:23:23 | → | berberman joins (~berberman@2408:8207:2565:18d0:584e:a9ff:fe9b:d3fe) |
| 10:24:08 | × | Rudd0^ quits (~Rudd0@185.189.115.108) (Ping timeout: 258 seconds) |
| 10:24:50 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 10:26:37 | × | polyrain quits (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 10:27:08 | → | polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) |
| 10:27:25 | × | polyrain quits (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) (Client Quit) |
| 10:27:42 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 10:28:51 | <siraben> | What a good alternative to the monad-gen package? |
| 10:32:32 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 10:35:16 | → | Orbstheorem joins (~roosember@hellendaal.orbstheorem.ch) |
| 10:36:15 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 10:41:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 10:42:53 | → | solonarv joins (~solonarv@astrasbourg-653-1-186-165.w90-13.abo.wanadoo.fr) |
| 10:47:34 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Quit: gone to sleep. ZZZzzz…) |
| 10:47:39 | → | random joins (~random@185.219.70.106) |
| 10:47:52 | <random> | hey guys, am I not getting this right or there is no phone parser library for Haskell |
| 10:47:59 | <random> | besides the one that requires libphonenumber? |
| 10:48:30 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 10:48:47 | <Rembane> | random: Is that US phone numbers? |
| 10:48:57 | <random> | I need for european ones |
| 10:49:17 | <random> | but there doesn't seem to be anything for US phones as well |
| 10:49:24 | <random> | thought this was quite a common usecase |
| 10:49:43 | <Rembane> | random: Got it. Maybe it is too simple to write a parser using Megaparsec that everyone does that instead? |
| 10:50:09 | <Rembane> | siraben: I have used this: https://hackage.haskell.org/package/quickcheck-transformer What is good for you? |
| 10:50:30 | → | ystael joins (~ystael@209.6.50.55) |
| 10:50:32 | <random> | Rembane: I guess not too simple but I'll be doing it as well lol... |
| 10:50:59 | <random> | the country code numbers are quite variable |
| 10:52:24 | <Rembane> | random: Yeah. :) |
| 10:52:39 | <Rembane> | random: Just out of curiosity, do you have some examples of country code numbers? |
| 10:52:53 | <random> | https://countrycode.org/ |
| 10:52:55 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Ping timeout: 272 seconds) |
| 10:53:40 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds) |
| 10:53:58 | → | knupfer joins (~Thunderbi@i59F7FF48.versanet.de) |
| 10:55:09 | <cheater> | random: phone numbers are a very difficult thing to parse, like time zone data and time strings, if there's going to be a competent library there's only going to be one |
| 10:55:29 | <random> | cheater: yeah but it relies on a C dep |
| 10:55:34 | <random> | we're in AWS Lambda so that hurts |
| 10:55:42 | <random> | I'll fix it of course, just found it weird |
| 10:55:43 | <Rembane> | random: Dashes! Why?! <- rhetorical question |
| 10:55:46 | <cheater> | that's pretty tough |
| 10:55:47 | <cheater> | sorry |
| 10:56:20 | <random> | alright, putting on my devops gloves |
| 10:56:25 | <random> | wish me luck guys *cries* |
| 10:58:40 | <Rembane> | random: GL HF! |
| 10:58:59 | × | random quits (~random@185.219.70.106) (Quit: Leaving) |
| 10:59:50 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 265 seconds) |
| 11:00:01 | × | maroloccio quits (~marolocci@2a02:8084:601d:7f80:164f:8aff:fed8:411d) (Quit: WeeChat 2.3) |
| 11:00:19 | <edwardk> | Forgive me, father, for I have sinned. It has been 33 years since my last confession. I used an overlapping instance, and looked lustfully upon another man's type system. What is my penance? |
| 11:01:40 | → | miguel_clean joins (~Miguel@89-72-187-203.dynamic.chello.pl) |
| 11:04:09 | → | AlterEgo- joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 11:05:19 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 11:06:05 | × | phaul quits (~phaul@ruby/staff/phaul) (Ping timeout: 240 seconds) |
| 11:06:23 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 11:07:55 | → | phaul joins (~phaul@ruby/staff/phaul) |
| 11:09:08 | × | kleisli_ quits (~kleisli@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Quit: Leaving) |
| 11:09:16 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 11:09:26 | → | outerpassage joins (~outerpass@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) |
| 11:10:21 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 11:11:29 | × | miguel_clean quits (~Miguel@89-72-187-203.dynamic.chello.pl) (Read error: Connection reset by peer) |
| 11:12:14 | → | bicho_rastrero joins (~cerdito@169.85-87-37.dynamic.clientes.euskaltel.es) |
| 11:13:27 | → | gpvs joins (~gp@37.57.178.79) |
| 11:14:05 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 11:14:08 | <phadej> | recite "why functional programming matters" ten times, and contribute to GHC. |
| 11:14:29 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 11:15:55 | <edwardk> | tough but fair |
| 11:20:25 | → | oo_miguel joins (~miguel@89-72-187-203.dynamic.chello.pl) |
| 11:20:26 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 246 seconds) |
| 11:20:37 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 265 seconds) |
| 11:21:18 | × | oo_miguel quits (~miguel@89-72-187-203.dynamic.chello.pl) (Client Quit) |
| 11:22:35 | <gpvs> | Hello. I can't make this compile: |
| 11:22:35 | <gpvs> | Class (Show type_self, AWord type_word) => Animal type_self where |
| 11:22:35 | <gpvs> | say :: type_self -> [type_word] |
| 11:22:35 | <gpvs> | I tried: |
| 11:22:35 | <gpvs> | Class Show type_self => Animal type_self where |
| 11:22:36 | <gpvs> | say :: AWord type_word => type_self -> [type_word] |
| 11:22:36 | <gpvs> | and it compiled, but then |
| 11:22:37 | <gpvs> | instance Animal AnimalSpecific where |
| 11:22:37 | <gpvs> | say (AnimalSpecific arrayOfInstancesOfAWord) = arrayOfInstanceOfAWord |
| 11:22:37 | × | gpvs quits (~gp@37.57.178.79) (Killed (Sigyn (Spam is off topic on freenode.))) |
| 11:23:39 | → | Amras joins (~Amras@unaffiliated/amras0000) |
| 11:23:48 | × | DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection) |
| 11:23:48 | ChanServ | sets mode +o ski |
| 11:23:53 | → | gpvs joins (~gp@37.57.178.79) |
| 11:23:54 | <Cale> | oops |
| 11:24:15 | <gpvs> | Hello. How do I paste multiline here not getting banned? |
| 11:24:22 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 11:24:26 | <Rembane> | gpvs: What error message do you get? Can you put it in a pastebin? See topic for information. |
| 11:24:33 | <Rembane> | gpvs: You can access topic by running the command /topic |
| 11:24:33 | <Cale> | try https://dpaste.com/ |
| 11:24:39 | <niko> | ski: already lifted |
| 11:24:50 | ChanServ | sets mode -o ski |
| 11:24:53 | <ski> | ok |
| 11:25:10 | → | tchouri joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 11:25:12 | <Rembane> | edwardk: Was it 33 years since you used an overlapping instance last time?! :O |
| 11:25:30 | <edwardk> | pretty close |
| 11:25:36 | <edwardk> | i used one other really |
| 11:26:02 | <int-e> | Overlapping instances is the devil's way of leading you towards incoherent instances. |
| 11:26:03 | <edwardk> | but i was granted an indulgence by one of the simons, so that sin never existed to be forgiven |
| 11:26:40 | <phadej> | I think that my overlapped instance count is negative |
| 11:26:43 | × | hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds) |
| 11:27:00 | <edwardk> | here i'm trying to hack around the fact that 1 + isn't injective for Nat. |
| 11:27:05 | <edwardk> | So I've had to get creative |
| 11:27:08 | <Rembane> | edwardk: Seems legit |
| 11:27:37 | <edwardk> | There appears to be a pattern synonym I _can't_ write without injectivity on succ, despite the fact that the GADT version typechecks, i can't emulate the GADT right. |
| 11:28:06 | <Rembane> | I'm probably extremely dense here, but I cannot see why 1 + isn't injective. What have I missed? |
| 11:28:20 | <phadej> | nobody told GHC |
| 11:28:37 | <Rembane> | Oh |
| 11:28:44 | <edwardk> | in theory if i can get the type information at just the right point so that names are in scopes maybe i can unsafeCoerce a :~~: to make the proof i need |
| 11:29:03 | <edwardk> | Rembane: the builtin Nat kind is crippled |
| 11:29:20 | <edwardk> | + only computes will fully grounded numbers |
| 11:29:32 | × | jespada quits (~jespada@90.254.241.6) (Quit: Sleeping) |
| 11:29:44 | <Cale> | At the term level, you have infinity = Succ infinity, which also messes up the injectivity of 1+ |
| 11:29:48 | <Rembane> | edwardk: How terrible is it to uncripple it? |
| 11:29:51 | <edwardk> | so i wind up in situations where i need to know 0 and 1+x are disjoint, or that 1+x = 1 + y => x + y |
| 11:29:58 | <Cale> | er, nevermind |
| 11:30:03 | <Cale> | It's just a fixed point |
| 11:30:07 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 11:30:32 | <phadej> | I think though that GHC knows some weak version of injectivity for (+) though, as otherwise one would get a lot more ambiguous type erros |
| 11:30:36 | <edwardk> | Rembane: that is a ghc hq thing. nats have been terrible for several years, so i'm not holding my breath. |
| 11:30:59 | <ski> | gpvs : do you understand the problem you're getting ? perhaps you want to make `Animal' a MPTC, parameterized by both `type_self' and `type_word' ? do you really need to make a type class at all ? |
| 11:31:06 | <Rembane> | edwardk: Got it. Then I assume that it isn't "just" to e-mail a patch and hope for the best. |
| 11:31:13 | <edwardk> | phadej: oh? afaict all it does it leave it dangling there as a stuck type family |
| 11:31:43 | <edwardk> | unless the args are fully grounded out by previous applications of the magic rule for the type family |
| 11:33:18 | <gpvs> | ski: wait a second please, forming dpaste from another PC |
| 11:33:27 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 11:33:55 | <phadej> | edwardk: if you write foo :: Proxy (x + y) -> Proxy x -> (); foo _ _ = () -- it is accepted |
| 11:34:21 | <phadej> | clearly means that (+ y) is injective. |
| 11:34:25 | × | oxide quits (~lambda@unaffiliated/mclaren) (Ping timeout: 264 seconds) |
| 11:34:31 | <phadej> | "clearly" |
| 11:34:38 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 11:35:22 | → | oxide joins (~lambda@unaffiliated/mclaren) |
| 11:35:50 | <edwardk> | hrmm |
| 11:36:51 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 11:37:32 | <edwardk> | the (+) type family is weird |
| 11:37:38 | <phadej> | git grep -i "interaction with inerts" in GHC code |
| 11:37:49 | <phadej> | I just know that makes that `foo` code type-checks |
| 11:37:53 | × | Cale quits (~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com) (Ping timeout: 272 seconds) |
| 11:38:09 | <phadej> | but how, ask someone else |
| 11:38:22 | <phadej> | (e.g. why it doesn't make partially applied + injective) |
| 11:38:51 | × | Turmfalke quits (~user@unaffiliated/siracusa) (Quit: Bye!) |
| 11:38:56 | <phadej> | but yes, wired-in magic type-families are weird. |
| 11:39:05 | <edwardk> | the fact that + has some kind of privileged f'd up position explains a bit of how i get errors with it i can't get elsewhere |
| 11:39:10 | → | dddddd_ joins (~dddddd@unaffiliated/dddddd) |
| 11:39:15 | × | NieDzejkob quits (~quassel@188.123.215.55) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 11:39:31 | <phadej> | re ground terms |
| 11:39:40 | <phadej> | 5 + n ~ 8 does simplify to n ~ 3 |
| 11:39:49 | <gpvs> | I seek to explain to GHC that I want a Class. Class's requirement has a function. Function's "return" type must be instance of another specific Class. Here is what I tried and errors I got: dpaste.com/FTAG9S4MQ , dpaste.com/EG5RM5HXY |
| 11:40:03 | × | Unhammer quits (~Unhammer@gateway/tor-sasl/unhammer) (Ping timeout: 240 seconds) |
| 11:40:24 | <edwardk> | yet it can't figure out 1 + n ~ 1 + m => n ~ m |
| 11:40:29 | <phadej> | no |
| 11:40:34 | <phadej> | nobody told it *that* :) |
| 11:40:42 | <phadej> | there isn't ring-solver in GHC |
| 11:40:53 | <phadej> | (it's available as a plugin) |
| 11:41:09 | <phadej> | https://hackage.haskell.org/package/ghc-typelits-natnormalise |
| 11:41:12 | <edwardk> | yeah |
| 11:41:25 | <edwardk> | was going to try the natnormalize plugin to see if i could use it to compile the pattern i need |
| 11:41:37 | × | dddddd quits (~dddddd@unaffiliated/dddddd) (Ping timeout: 264 seconds) |
| 11:41:58 | <phadej> | I guess Christiaan would appreaciate if you tell him that *it works for you* ;) |
| 11:42:09 | → | NieDzejkob joins (~quassel@188.123.215.55) |
| 11:42:28 | <ski> | gpvs : so you want to associate each `type_self', that you make an instance for, with a particular `type_word' |
| 11:42:54 | <edwardk> | let me add the example i'm fighting with to the repo |
| 11:43:05 | → | utopic_int0x80 joins (~lucid_0x8@188.253.237.87) |
| 11:44:17 | <gpvs> | ski: If I got you correctly: I may, but where is no need to. AWord is good enough abstraction for Animal-s to work with, there is no need to bind particular animals to particular words |
| 11:44:29 | <kicov> | Got a few cpsy + liquid haskell examples: https://dpaste.com/3YX484ND7 and https://dpaste.com/FHMQ5DZ44 - just wondering how both examples could work using single cpsy annotation. |
| 11:44:41 | <gpvs> | ski: and if I must to associate it, how would I do that? |
| 11:44:46 | <edwardk> | oh weeee, more regressions |
| 11:44:47 | × | alx741 quits (~alx741@186.178.110.2) (Ping timeout: 265 seconds) |
| 11:45:42 | → | __Joker joins (~Joker@180.151.105.65) |
| 11:45:42 | <ski> | gpvs : so you definitely don't want the `class Show type_self => Animal type_self where say :: AWord type_word => type_self -> [type_word]' version, since it means that if you pass a `AnimalSpecific' to `say', then `say' will have to be able to compute a list of `type_word's for any instance of `AWord' `type_word', that the caller wants, not just for the `AWordDog' instance |
| 11:45:47 | <edwardk> | phadej: https://github.com/ekmett/haskell/tree/master/types is the project in question |
| 11:45:47 | × | lucid_0x80 quits (~lucid_0x8@188.253.232.248) (Ping timeout: 258 seconds) |
| 11:46:10 | <edwardk> | if i compile with -f-injectiveSucc then examples/Vec.hs goes to hell |
| 11:46:53 | <ski> | gpvs : so, it seems you either want an existential (but i suspect you don't actually want that here), or else you want to make `type_word' an additional parameter of `Animal' (possibly with a Functional Dependency) |
| 11:47:04 | <gpvs> | ski: oh, now I got it. Any reason first approach should not work? |
| 11:47:05 | <edwardk> | you may need to disable the construction of the SingI instances in Data.Type.Internal.TH as well here https://github.com/ekmett/haskell/blob/master/types/src/Data/Type/Internal/TH.hs#L122 |
| 11:47:14 | <ski> | gpvs : hmm |
| 11:47:46 | <edwardk> | but if i write a manual data type that does it rather than emulate a GADT with my pattern synonym i can make it work *headdesk* |
| 11:48:05 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 11:48:19 | <ski> | gpvs : "AWord is good enough abstraction for Animal-s to work with, there is no need to bind particular animals to particular words" -- but you just tried to associate `AnimalSpecific', not to arbitrary instances of `AWord', but specifically to `AWordDog' |
| 11:48:24 | <edwardk> | but i can't have the actual data type because i need a homogeneous representation for my singletons or i lose a huge performance tax. |
| 11:48:51 | <ski> | gpvs : that is, your implementation of `say' tried to do that |
| 11:49:00 | <phadej> | edwardk: I only understood "right and slow vs. doesn't work fast" |
| 11:49:09 | <gpvs> | ski: what's existential? could you provide a link or googling term please? I'm truing two avoid making type_word a parameter to Animal not to bind them |
| 11:49:21 | <edwardk> | the cost is linear vs O(1) |
| 11:49:30 | <edwardk> | i have hacked around every other obstacle in the way |
| 11:49:38 | <edwardk> | this is the last farking leg |
| 11:49:55 | → | Cale joins (~cale@99.253.130.57) |
| 11:50:12 | <ski> | gpvs : do you want to require `say' to return a list of `type_word's, for some `type_word' that's an instance of `AWord' (but each `say' implementation should be allowed to pick which such `type_word' it wants) ? |
| 11:50:42 | × | shad0w_ quits (~shad0w_@160.202.36.27) (Remote host closed the connection) |
| 11:50:44 | <edwardk> | in the process i dragged the Nat kind and hacked it to work like Natural as a type (which will just work when ghc does it for real), hacked Type to look like TypeRep, hacked Symbol to look like String, used stuck data families to get me ways to use Int and Char meaningfully as kinds. |
| 11:50:57 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 11:51:00 | <edwardk> | and came up with a way to get constant time singletons |
| 11:51:13 | <edwardk> | which works for everything except when my singleton gets fancy enough |
| 11:51:17 | <edwardk> | and Nat is involved |
| 11:51:20 | <edwardk> | because Nat is awful |
| 11:51:30 | <gpvs> | ski: exactly. Any Animal's 'say' may return *any* value which is instance of AWord |
| 11:51:40 | <gpvs> | ski: * a list |
| 11:51:45 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 240 seconds) |
| 11:52:20 | <ski> | gpvs : could different elements of the list be of different types `type_word', provided all are instances of `AWord' ? or should all elements in the list be of the same type `type_word' ? |
| 11:53:10 | <gpvs> | ski: I don't have requirement for/against it at the moment. could you please provide both verions? |
| 11:53:19 | <edwardk> | phadej: that said, i really like using Type as Typeable.TypeRep. and then Type.Reflection.TypeRep becomes its singleton |
| 11:53:40 | <edwardk> | very pretty code results |
| 11:54:41 | dddddd_ | is now known as dddddd |
| 11:54:48 | × | Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Remote host closed the connection) |
| 11:54:59 | → | Raito_Bezarius joins (~Raito_Bez@2001:bc8:38ee::1) |
| 11:55:02 | <ski> | gpvs : hm, let's consider alternatives, and what they would mean |
| 11:55:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 246 seconds) |
| 11:55:31 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 11:55:35 | <Cale> | I'm pretty sure from the looks of the code that made it into the channel that gpvs wants a fundep |
| 11:55:46 | <Cale> | But maybe I missed something |
| 11:55:49 | × | sfvm quits (~sfvm@37.228.215.148) (Quit: off to the basement, mixing up the medicine) |
| 11:55:54 | × | Raito_Bezarius quits (~Raito_Bez@2001:bc8:38ee::1) (Changing host) |
| 11:55:54 | → | Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) |
| 11:56:04 | <ski> | gpvs : `class Show type_self => Animal type_self where say :: AWord type_word => type_self -> [type_word]' means that the caller of `say' will decide which `type_word' to pick, can pick any, as long as its an instance of `AWord'. and you said you don't want that |
| 11:56:15 | → | roconnor joins (~roconnor@host-45-78-255-115.dyn.295.ca) |
| 11:56:26 | → | Unhammer joins (~Unhammer@gateway/tor-sasl/unhammer) |
| 11:56:42 | <Cale> | gpvs: The type of the result should depend on the type of the input, right? |
| 11:57:04 | → | alx741 joins (~alx741@186.178.110.130) |
| 11:57:20 | × | Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Read error: Connection reset by peer) |
| 11:57:27 | × | priyesh quits (~priyesh@84.39.117.57) (Remote host closed the connection) |
| 11:57:33 | → | Raito_Bezarius joins (~Raito_Bez@2001:bc8:38ee::1) |
| 11:57:37 | <edwardk> | looks like ghc-typelits-natnormalise isn't able to help solve the 1 + n ~ 1 + m ==> n ~ m problem |
| 11:57:56 | <edwardk> | i get the same issue with the plugin enabled |
| 11:58:28 | <gpvs> | ski: I don't want the rigid return type to be defined at type instantiation moment. I'm interesting in both version where return type is define on call or by implementation itself |
| 11:58:39 | <Cale> | edwardk: Can you use unsafeCoerce to get yourself out of that? |
| 11:58:41 | <edwardk> | the problem is that i'm neck deep in a pattern synonym at the time it happens and can't. really get both n and m in type in scope to unsafeCoerce my way to glory |
| 11:58:43 | <ski> | gpvs : `class (Show type_self, AWord type_word) => Animal type_self where say :: type_self -> [type_word]' means that you have associations between particular `type_self's and particular `type_word'. so, for a particular `type_self', you don't need to have all possible instances `type_word' of `AWord' to consider. you could just have some of them, if you'd like to. also, you could enforce it to be at most one `type_word', if you'd want to |
| 11:58:55 | <Cale> | ahh |
| 11:58:56 | × | Raito_Bezarius quits (~Raito_Bez@2001:bc8:38ee::1) (Client Quit) |
| 11:58:58 | <edwardk> | i've been trying ever more esoteric dances to make that work |
| 11:59:07 | → | Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) |
| 11:59:25 | <Cale> | Pattern synonyms are jankier than I ever imagined they might be |
| 11:59:31 | <gpvs> | Cale: optionaly, but I don't want to bind Animal instances to particular AWord-s instances |
| 11:59:45 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 11:59:59 | <edwardk> | https://github.com/ekmett/haskell/blob/master/types/example/Vec.hs#L49 the issue is it can't figure out ys is well typed there. |
| 12:00:14 | × | Raito_Bezarius quits (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) (Read error: Connection reset by peer) |
| 12:00:23 | <Cale> | gpvs: Maybe the solution is just a simple two parameter type class then |
| 12:00:32 | → | Raito_Bezarius joins (~Raito_Bez@unaffiliated/raito-bezarius/x-8764578) |
| 12:00:38 | <edwardk> | there is another issue involving the SingI instance but i can hack around that by moving the type synonym around |
| 12:00:49 | <Cale> | gpvs: Though, that won't be terribly *convenient* since you'll probably have to annotate the type of the result a lot, given that it can't be determined by the type of the input |
| 12:00:58 | <edwardk> | Cale: i'm doing evil things in there |
| 12:01:27 | <ski> | gpvs : the last option is existentials, which here would be either `class Show type_self => Animal type_self where say :: type_self -> exists type_word. AWord type_word *> [type_word]' or `class Show type_self => Animal type_self where say :: type_self -> [exists type_word. AWord type_word *> type_word]'. both of these will allow the choice of `type_word' to depend on the run-time input to `say' (if you don't want that, that could be corrected) |
| 12:01:27 | <edwardk> | Cale: in particular i'm emulating GADTs on a non GADT using pattern synonyms and another GADT as a helper to sort of scaffold all the equalities i need |
| 12:01:40 | <gpvs> | Cale: resulting types will bind particula Animals to particular Words then, wouldn't they? |
| 12:01:43 | <ski> | (er, possibly cut off part was "(if you don't want that, that could be corrected)") |
| 12:01:44 | <edwardk> | the scaffolding GADT is just unsafeCoerced to offer what i need |
| 12:02:15 | × | kicov quits (959c7c03@nat.ds3.agh.edu.pl) (Remote host closed the connection) |
| 12:02:28 | <gpvs> | Cale: I've just read what fundeps are and I believe it's not what I want |
| 12:02:35 | × | wei2912 quits (~wei2912@unaffiliated/wei2912) (Quit: Lost terminal) |
| 12:02:41 | → | mirrorbird joins (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2) |
| 12:03:39 | <edwardk> | pattern SVCons :: forall k (n :: Nat) (r :: Vec k (1 + n)). () => forall (x :: k) (xs :: Vec k n). r ~ 'VCons x xs => Sing x -> Sing xs -> Sing r; pattern SVCons y ys <- ( upSVec -> SVCons' y ys) where SVCons (Sing y) (Sing ys) = UnsafeSing (VCons y ys); should basically faithfully emulate the GADT constructor that it delegates down to for proof |
| 12:03:47 | <Cale> | gpvs: It would mean that, say, given that you have a list of Cats as input, then the type of words that Cats produce would be determined by the fact that they are Cats |
| 12:04:00 | <Cale> | For example, maybe Cats produce Text |
| 12:04:03 | <edwardk> | upSVec casts from Sing x -> SVec' x |
| 12:04:07 | <gpvs> | ski: "means that the caller of `say' will decide which `type_word' to pick, can pick any" how do I express it in Haskell from the callers perspective? |
| 12:04:14 | <edwardk> | but the constructor for SVec' is well typed and happy |
| 12:04:29 | <edwardk> | i just can't figure out the right way to pass through the lesson from SVec' to Sing |
| 12:04:36 | <Cale> | gpvs: That's just the two-parameter class with no functional dependencies |
| 12:04:37 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) |
| 12:04:43 | <edwardk> | when it matches it learns a heterogeneous type equality |
| 12:04:52 | × | DavidEichmann quits (~david@43.240.198.146.dyn.plus.net) (Ping timeout: 246 seconds) |
| 12:05:07 | <Cale> | gpvs: and you can write type annotations like (say cats :: [Text]) to determine the type of result then |
| 12:05:24 | <Cale> | (or if it's determined by how the result is used, that's also fine |
| 12:05:26 | <Cale> | ) |
| 12:05:27 | <ski> | gpvs : that option was already expressed in Haskell. i dunno what you mean by "from the callers perspective" (i was already talking there about it being the caller who got to pick `type_word' there) |
| 12:05:27 | <edwardk> | that the output type is carrying an argument of kind Vec k (S n) relative to Vec k n for the inside argument to the vector. |
| 12:07:47 | <edwardk> | -- just works (S n = 1 + n as a type synonym, Z = 0) -- so now what i want is a pattern synonym as a next step that just basically wraps SVCons0 https://www.irccloud.com/pastebin/j3dAUDko/svec0 |
| 12:07:58 | hackage | binaryen 0.0.4.0 - Haskell bindings to binaryen https://hackage.haskell.org/package/binaryen-0.0.4.0 (terrorjack) |
| 12:08:01 | × | rprije quits (~rprije@27.143.220.203.dial.dynamic.acc01-myal-dub.comindico.com.au) (Ping timeout: 258 seconds) |
| 12:08:03 | × | p-core quits (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) (Quit: p-core) |
| 12:08:18 | <edwardk> | if that data type didn't type check this wouldn't be so infuriating |
| 12:08:23 | <edwardk> | because i'd know it was impossible |
| 12:08:25 | → | p-core joins (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) |
| 12:08:27 | <gpvs> | ski: `class Show type_self => Animal type_self where say :: AWord type_word => type_self -> [type_word]' I got error trying to compile it. It's in https://dpaste.com/EG5RM5HXY . Did I missed some required extensions? |
| 12:08:29 | <edwardk> | but that is just hunky dory |
| 12:08:45 | <Cale> | edwardk: hmm, think I'll have to fire up ghci here... :) |
| 12:10:15 | <gpvs> | ski: this `class (Show type_self, AWord type_word) => Animal type_self where say :: type_self -> [type_word]' got me compile error too. https://dpaste.com/FTAG9S4MQ |
| 12:10:16 | <ski> | gpvs : no, your `say' implementation doesn't satisfy that type signature |
| 12:10:34 | <ski> | (the `say :: AWord type_word => type_self -> [type_word]' one, i mean) |
| 12:11:03 | <Cale> | gpvs: You need another parameter on the class there |
| 12:11:29 | <Cale> | gpvs: class (Show s, AWord w) => Animal s w where say :: [s] -> [w] |
| 12:11:30 | <ski> | gpvs : oh, sorry. the middle alternative should have been `class (Show type_self, AWord type_word) => Animal type_self type_word where say :: type_self -> [type_word]' .. iow MPTC |
| 12:11:44 | <ski> | Cale : no list input |
| 12:11:45 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 12:12:07 | <Cale> | oh |
| 12:12:08 | × | p-core quits (~Thunderbi@koleje-wifi-0046.koleje.cuni.cz) (Client Quit) |
| 12:12:09 | <Cale> | okay |
| 12:12:17 | <Cale> | yeah, just s -> [w] in that case |
| 12:13:28 | <ski> | gpvs : anyway, perhaps we should first try to determine what you want, before diving into the how ? |
| 12:13:40 | <edwardk> | Cale: i have it boiled down to one file now |
| 12:14:08 | <edwardk> | https://www.irccloud.com/pastebin/KHWDco0s/BrokenVec.hs |
| 12:14:23 | <edwardk> | that is standalone and doesn't need the types library i'm writing |
| 12:14:45 | <Cale> | ah, cool |
| 12:15:31 | <gpvs> | Cale, ski: ok, as far as I can see to get a uniform list of instances I *must* bind types like with multiparam class. What about getting a non-uniform list? Like when Cat can say [WordType0, WordType2]. |
| 12:15:57 | <Cale> | gpvs: Well, what do those word types have in common? What are you going to do with the resulting list? |
| 12:16:19 | <ski> | gpvs : you could do that, too, with existentials |
| 12:16:22 | <gpvs> | ski: I want something like returning an array of objects confirming to interface in OO-kind stuff |
| 12:16:27 | <Cale> | gpvs: You can think of a type as representing permissions to use the corresponding values in particular ways. If you don't know what type something is, it becomes impossible to observe |
| 12:16:27 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 12:16:36 | <ski> | gpvs : yea, that sounds like existentials |
| 12:16:37 | → | PropositionJoe joins (~ConJoe@cm-84.215.192.230.getinternet.no) |
| 12:16:49 | <gpvs> | Cale: those word types all are instances of AWord class |
| 12:16:53 | <ski> | gpvs : however, often this is not a good idea / overkill. but you can do it |
| 12:16:53 | <PropositionJoe> | Why do I have to write "`div`" instead of just div? |
| 12:17:04 | <Cale> | Yeah, existentials give you one way to discard information about what type of thing you have |
| 12:17:11 | <ski> | > div 18 7 -- PropositionJoe |
| 12:17:14 | <lambdabot> | 2 |
| 12:17:14 | <edwardk> | > div 4 3 |
| 12:17:17 | <lambdabot> | 1 |
| 12:17:18 | <edwardk> | works for me |
| 12:17:21 | × | suppi quits (~suppi@2605:f700:40:c00::e6fc:6842) (Ping timeout: 244 seconds) |
| 12:17:31 | <PropositionJoe> | so div is prefix "`div`" is infix? |
| 12:17:34 | <ski> | yep |
| 12:17:35 | <Cale> | data SomeWord where MkSomeWord :: AWord w => w -> SomeWord |
| 12:17:37 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 12:17:40 | <PropositionJoe> | thanks ski |
| 12:17:48 | <edwardk> | putting backticks on makes anything infix |
| 12:17:49 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 12:17:50 | <ski> | PropositionJoe : works for any identifier |
| 12:17:51 | <Cale> | (that uses the GADTs extension) |
| 12:17:53 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Remote host closed the connection) |
| 12:18:20 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 12:19:41 | <ski> | gpvs : `AWord' class currently has no methods (and no superclasses). so `exists type_word. AWord type_word *> ..type_word..' is kind of pointless, you can't get any information out. but perhaps your shown `AWord' was a mockup, and you'll actually have useful methods or superclasses ? |
| 12:21:02 | <Cale> | gpvs: In my example, applying the MkSomeWord data constructor to a value whose type w is an instance of AWord will result in forgetting everything about which type w was, except that it had an instance of AWord, and then the only things you'll be allowed to do with the value when you get it out will be things you could do with any unknown instance of AWord |
| 12:21:07 | <ski> | gpvs : "I want something like returning an array of objects confirming to interface in OO-kind stuff" -- do you actually need that ? how are you going to use the result of calls to `say' ? (Cale's question) |
| 12:21:38 | <gpvs> | Cale, ski: looks like downcasting to me. Seems like I getting closer. I understand it doesn't make a lot sense in Haskell, just trying of how far it can extend. Yes, AWord is a mockup |
| 12:21:44 | <Cale> | If you want to be more like OO, it might be more sensible just to make object types which correspond to whatever your classes would have been |
| 12:21:58 | → | fulc927 joins (~fulc927@unaffiliated/fulc927) |
| 12:22:01 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 246 seconds) |
| 12:22:02 | <ski> | gpvs : there is no downcasting in Haskell, really |
| 12:22:04 | <Cale> | Don't try to use Haskell classes as OO classes, they're not the same thing |
| 12:22:29 | <Cale> | Instances of OO classes are values, instances of Haskell classes are types. |
| 12:22:30 | <gpvs> | ski: yes, I sayed that making a parallel to what it would be for me in OO |
| 12:22:32 | <ski> | gpvs : and how would you use downcasting, anyway ? test for particular types ? why not use a sum type ? |
| 12:22:45 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 12:22:58 | × | ystael quits (~ystael@209.6.50.55) (Ping timeout: 265 seconds) |
| 12:23:05 | <Cale> | Haskell classes are a good bit like interfaces though |
| 12:23:15 | tchouri | is now known as hekkaidekapus |
| 12:23:17 | <Cale> | But usually it makes more sense not to start from there |
| 12:23:21 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:2032:8cd9:bb36:4db2) (Ping timeout: 246 seconds) |
| 12:23:40 | <Cale> | What methods were you going to put in the AWord class? |
| 12:23:41 | <ski> | gpvs : if `AWord' is beefy enough for you to be able to do something sensible with values of an unknown type `type_word' that's an instance of `AWord', then existentials start to make more sense |
| 12:23:50 | <gpvs> | ski, Cale: "data SomeWord where MkSomeWord :: AWord w => w -> SomeWord" ok, maybe 'downcasting' is not the best term. Let me call it 'specialization' then. |
| 12:24:42 | <gpvs> | ski: yes, AWord in dpaste is a mockup |
| 12:24:47 | → | suppi joins (~suppi@2605:f700:40:c00::e6fc:6842) |
| 12:24:50 | <ski> | yea, i got that |
| 12:25:06 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 12:25:06 | → | __Joker joins (~Joker@180.151.105.65) |
| 12:25:28 | <ski> | gpvs : by "downcasting" i meant being able to do e.g. `toAWordDog :: AWord w => w -> Maybe AWordDog' |
| 12:25:47 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 12:25:48 | <gpvs> | Cale: I will not try to do OO with Haskell, pinkie-promise! :) Just looking at cases while learning. |
| 12:25:54 | <ski> | gpvs : that is the kind of thing you had in mind, yes ? |
| 12:26:57 | <gpvs> | ski: nodes of graph of different types and constructs which can reference each other regardless, relying on fact that all of them confirm to the basic interface |
| 12:27:25 | <ski> | gpvs : which question is that an answer to ? |
| 12:27:58 | <ski> | (it doesn't seem to obviously be about how to use downcasts, e.g.) |
| 12:28:55 | <Cale> | gpvs: Well, I think doing OO with Haskell can be quite good in some cases. The encoding, if you do it right, is indistinguishable from ordinary functional programming. You have first class functions and you have record types. Put those together, and you can make records of methods which can be defined differently for each value you construct. |
| 12:29:06 | <ski> | Cale : although you call interface methods on an object :) |
| 12:29:14 | <Cale> | gpvs: i.e. you don't need subclasses to override method implementations |
| 12:29:24 | <Cale> | (which is good, since you don't have subclasses) |
| 12:29:55 | <gpvs> | ski: I misread 'that' as 'what', sorry. It seems like that. Have to research existentials and try in ghc. |
| 12:30:13 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 264 seconds) |
| 12:30:15 | <Cale> | I would honestly avoid existentials initially |
| 12:30:26 | <Cale> | Most of the time, you won't really need them |
| 12:30:37 | <ski> | @where existential-antipattern |
| 12:30:37 | <lambdabot> | "Haskell Antipattern: Existential Typeclass" by Luke Palmer at <http://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-typeclass/> |
| 12:31:36 | <gpvs> | ski, Cale: thank you for your help! Will research existentials and try them for my case, just to know it's there. If you wondering, the original idea was "nodes of graph of different types and constructs which can reference each other regardless, relying on fact that all of them confirm to the basic interface" |
| 12:31:36 | <Cale> | gpvs: The important question to think about first is "what am I allowed to do with these things?" -- if you can figure out all the things you're allowed to do with a thing, then one of the ways of defining its type is just as a collection of the results of those operations |
| 12:31:39 | <ski> | gpvs : if we saw the actual `AWord' class, or if you told how you were going to use the results of `say', or both, we might be able to give better advice |
| 12:32:35 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 12:32:41 | <ski> | gpvs : that's a pretty vague, non-committal description |
| 12:33:01 | <gpvs> | lamdabot: thanks for the link |
| 12:34:05 | <ski> | gpvs : (a) often you don't want/need OO-style things; (b) if you do, ordinary lexical scoping with records commonly suffice; (c) sometimes existentials may be required |
| 12:34:30 | <bicho_rastrero> | I'm learning haskell and I saw this syntax in a function "merge list1@(x: xs) list2@(y : ys)", what is the name of the @ operator there? How is that structure named? |
| 12:34:36 | <ski> | gpvs : you should probably not reach for existentials, unless you really need them |
| 12:35:25 | <ski> | bicho_rastrero : "as-patterns" |
| 12:35:30 | <gpvs> | ski: part I stumbled on is the last part of description. Any type of class node should be able to return a list of nodes it's connected to, these nodes might be of different types, but of the same base class. |
| 12:35:48 | <bicho_rastrero> | Thank you, ski |
| 12:36:12 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:59cb:4e8f:c201:4e04) |
| 12:36:16 | <ski> | bicho_rastrero : it's both giving a name to the whole input, and simultaneously matching it with a pattern, so that you can check its shape, and name parts |
| 12:36:26 | × | carif quits (~mcarifio@cpe-67-246-228-200.rochester.res.rr.com) (Quit: Leaving) |
| 12:37:00 | <bicho_rastrero> | Yeah, that was my understanding, but I wanted to read an proper explanation with more examples. Thanks. |
| 12:37:04 | <ski> | gpvs : yea, it sounds like you could possibly do that with just (b) |
| 12:37:17 | <ski> | (depending on the specifics of what you want to do with them) |
| 12:37:23 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 12:37:31 | <ski> | gpvs : iow the record-of-operations that Cale mentioned |
| 12:39:01 | × | utopic_int0x80 quits (~lucid_0x8@188.253.237.87) (Ping timeout: 260 seconds) |
| 12:39:08 | → | drbean joins (~drbean@TC210-63-209-85.static.apol.com.tw) |
| 12:40:02 | → | ukari joins (~ukari@unaffiliated/ukari) |
| 12:42:28 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 12:42:54 | → | henninb joins (~henninb@63-226-191-96.mpls.qwest.net) |
| 12:44:15 | × | henninb quits (~henninb@63-226-191-96.mpls.qwest.net) (Client Quit) |
| 12:44:27 | <Cale> | edwardk: Ah, so annoying to try to get these n1 and n2 in scope... |
| 12:44:35 | <edwardk> | exactly! |
| 12:44:35 | → | henninb joins (~henninb@63-226-191-96.mpls.qwest.net) |
| 12:44:40 | × | henninb quits (~henninb@63-226-191-96.mpls.qwest.net) (Client Quit) |
| 12:45:06 | <Cale> | It's not even syntactically permitted to write something like pattern SVCons y (ys :: ...) |
| 12:45:13 | → | henninb joins (~henninb@63-226-191-96.mpls.qwest.net) |
| 12:45:19 | → | bitmagie joins (~Thunderbi@200116b8062b2e00fc59d02ac7bcf06a.dip.versatel-1u1.de) |
| 12:46:44 | <edwardk> | i fought with writing (\x -> case upSNat x of ... -> (sometypeequality,y,ys) ) -> (Refl,y,ys)) |
| 12:46:52 | <edwardk> | for the viewpattern |
| 12:47:00 | <edwardk> | but that didn't move the needle much |
| 12:47:26 | <edwardk> | if S is replaced with data family S :: Nat -> k -- this just works |
| 12:47:44 | <edwardk> | but then i'm adding exotic types to kind Nat |
| 12:47:47 | <Cale> | I wrote this thing: onePlusInj :: forall n m r. ((1+n) ~ (1+m)) => (n ~ m => r) -> r but of course, I need to disambiguate which types I want to use it with |
| 12:47:55 | <edwardk> | yeah |
| 12:47:58 | <edwardk> | did the same |
| 12:48:02 | <Cale> | The idea being that maybe we can stick it in using a view pattern |
| 12:48:17 | <edwardk> | thats the sort of thing the scenario above tried to use |
| 12:48:18 | × | coot quits (~coot@37.30.55.202.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 272 seconds) |
| 12:48:25 | <Cale> | yeah, I see |
| 12:48:26 | <Cale> | hmm |
| 12:48:27 | <edwardk> | the someTypeEquality thing there can be a refl built |
| 12:48:41 | <edwardk> | and in there i can see x and the types of y and ys |
| 12:48:54 | <edwardk> | before i return them out to the surrounding context |
| 12:50:18 | → | kicov joins (959c7c03@nat.ds3.agh.edu.pl) |
| 12:51:41 | <kicov> | Hi, one more question about liquid haskell : are annotation such as `function :: f:(Int -> Int) -> {ret : Int | f ret == 0}` possible, or is something similiar also possible ? |
| 12:51:55 | <Cale> | btw, I love the super janky required () => in the type of the pattern synonym |
| 12:52:09 | <Cale> | It inspires so much confidence in GHC |
| 12:52:48 | <edwardk> | i also run into problems when i go to write the SingI instance. morally its instance (SingI a, SingI b) => SingI ('VCons a b) -- but the argumentthere has a type synonym in it! |
| 12:53:18 | <edwardk> | which prevents me from hanging the instance |
| 12:53:19 | <Cale> | I wonder... can we bind (kind/type) variables in the pattern's type signature? Does that work? |
| 12:53:26 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 12:53:32 | <edwardk> | oh let me give you a longer worked version |
| 12:53:46 | <edwardk> | yes |
| 12:54:19 | <edwardk> | forall variables. (context needed to call the pattern) => forall more variables (stuff you learn by binding the pattern) => pattern args -> pattern result |
| 12:54:30 | <edwardk> | the two context thing is deliberate |
| 12:54:33 | <edwardk> | it was the chosen syntax |
| 12:54:39 | <edwardk> | by ghc ghc |
| 12:54:41 | <edwardk> | er ghc hq |
| 12:54:57 | hackage | inline-c 0.9.1.1 - Write Haskell source files including C code inline. No FFI required. https://hackage.haskell.org/package/inline-c-0.9.1.1 (FrancescoMazzoli) |
| 12:55:17 | <edwardk> | to disambiguate between what you need to call the pattern (like fromjson, tojson, etc.) and what you learn by matching. (like GADT existential args) |
| 12:55:33 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 12:56:19 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) |
| 12:56:40 | → | utopic_int0x80 joins (~lucid_0x8@188.253.237.87) |
| 12:57:56 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 12:58:25 | <gpvs> | lambdabot: <https://lukepalmer.wordpress.com/2010/01/24/haskell-antipattern-existential-typeclass/> yeah, this actually made sense for me once I recalled there is currying |
| 12:58:34 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 12:58:39 | <gpvs> | ski, Cale, lamdabot: thank you for your help! |
| 12:58:40 | → | ystael joins (~ystael@209.6.50.55) |
| 12:58:59 | × | gpvs quits (~gp@37.57.178.79) (Quit: Leaving.) |
| 13:00:58 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 272 seconds) |
| 13:01:47 | × | ph88^ quits (~ph88@ip5f5af726.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 13:03:19 | × | fiQ2 quits (~fiQ@mirkk.ninja) (Ping timeout: 246 seconds) |
| 13:04:02 | × | laxask quits (~lax@unaffiliated/laxask) (Ping timeout: 246 seconds) |
| 13:04:35 | ski | suspects gpvs meant "partial application" |
| 13:08:28 | <Cale> | edwardk: I got... something... to compile |
| 13:08:43 | <Cale> | I'm not sure if it's not just completely fucked, one sec :D |
| 13:08:43 | <edwardk> | i have a few versions that compile, but none that learn when they match |
| 13:08:54 | × | henninb quits (~henninb@63-226-191-96.mpls.qwest.net) (Quit: leaving) |
| 13:09:42 | × | bicho_rastrero quits (~cerdito@169.85-87-37.dynamic.clientes.euskaltel.es) (Remote host closed the connection) |
| 13:09:53 | <edwardk> | pattern SVCons :: forall (k::Type) (x::k) (n::Nat) (xs :: Vec k n). () => () => Sing x -> Sing xs -> Sing ('VCons x xs :: Vec k (S n)); pattern SVCons a b <- (upSVec -> (SVCons' a b :: SVec' ('VCons a b))) where SVCons (Sing y) (Sing ys) = UnsafeSing (VCons y ys) |
| 13:10:27 | → | polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) |
| 13:10:35 | <Cale> | Yeah, that looks pretty similar |
| 13:11:08 | → | laxask joins (~lax@unaffiliated/laxask) |
| 13:11:35 | <edwardk> | all of this is to hack around the injectivity of succ, if it was there i could just use literally the same code i generate via template haskell for everything else |
| 13:11:56 | <Cale> | oh wait, what if we just need r ~ 'VCons x xs twice? |
| 13:12:05 | <edwardk> | but if i get gimped by any attempt to use kind nat, which perforce infects Int and other numeric types i lift i get screwed up |
| 13:12:08 | <edwardk> | ? |
| 13:12:45 | × | utopic_int0x80 quits (~lucid_0x8@188.253.237.87) (Ping timeout: 240 seconds) |
| 13:12:45 | <edwardk> | oh, the ~ there is probably going to be a ~~ |
| 13:13:04 | <edwardk> | the starting Vec k n needs to learn it is Vec k n' but that is the kind for the argument type |
| 13:13:15 | <edwardk> | so you need to learn both the kind and the type |
| 13:13:20 | <edwardk> | which is ~~'s job |
| 13:13:32 | × | suppi quits (~suppi@2605:f700:40:c00::e6fc:6842) (Ping timeout: 260 seconds) |
| 13:13:33 | <Cale> | Do you have an example usage handy? |
| 13:13:47 | <Cale> | (of using the pattern synonym to learn the equality) |
| 13:14:11 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 13:14:28 | × | acidjnk_new2 quits (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 13:14:44 | <edwardk> | https://github.com/ekmett/haskell/blob/master/types/src/Data/Type/Internal.hs#L435 |
| 13:14:44 | × | bitmagie quits (~Thunderbi@200116b8062b2e00fc59d02ac7bcf06a.dip.versatel-1u1.de) (Quit: bitmagie) |
| 13:14:55 | → | acidjnk_new2 joins (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) |
| 13:14:57 | <edwardk> | each of the patterns in there and all the ones generated by TH learn the result type |
| 13:15:05 | → | suppi joins (~suppi@172.246.241.246) |
| 13:15:07 | <edwardk> | but the result argument's kind doesn't change unlike here |
| 13:17:23 | <edwardk> | when working with a S that is injective, (e.g. using the data family hack) you can just write |
| 13:17:27 | <edwardk> | pattern SVCons :: () => (r ~ 'VCons a b) => Sing a -> Sing b -> Sing r; pattern SVCons a b <- (upSVec -> SVCons' a b) where SVCons (Sing y) (Sing ys) = UnsafeSing (VCons y ys) |
| 13:17:31 | <edwardk> | like every other instance |
| 13:17:39 | <edwardk> | and my TH would have a hope in hell of autogenerating it |
| 13:18:41 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 13:19:57 | × | acidjnk_new2 quits (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 13:22:55 | × | PropositionJoe quits (~ConJoe@cm-84.215.192.230.getinternet.no) (Quit: Leaving) |
| 13:25:24 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 13:25:26 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 13:25:30 | × | nbloomf quits (~nbloomf@2600:1700:83e0:1f40:118d:2a8:7881:1f11) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 13:29:26 | → | jeremybennett joins (~jeremyben@185.244.214.216) |
| 13:31:18 | → | geekosaur joins (ae68c070@cpe-174-104-192-112.neo.res.rr.com) |
| 13:33:03 | <edwardk> | the main concern about dumping an S into kind Nat like that though is that you get two types that produce the same value, and i can't create a custom KnownNat instance for instance KnownNat n => KnownNat (S n) -- so i can only make an overlapping instance of SingI (S n) |
| 13:33:13 | <edwardk> | and overlapping makes me sad |
| 13:33:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 13:35:44 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 13:38:28 | → | danso joins (~dan@107-190-41-58.cpe.teksavvy.com) |
| 13:40:01 | <edwardk> | Cale: https://github.com/TimWSpence/stitch/blob/master/src/Language/Stitch/Exp.hs#L158 |
| 13:40:04 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 246 seconds) |
| 13:40:31 | <edwardk> | SVec ~ Sing here |
| 13:41:08 | <edwardk> | TypeRep a there is Sing (a :: Type) here |
| 13:41:41 | <edwardk> | exprType :: Sing ctx -> Exp ctx ty -> Sing ty |
| 13:42:19 | <edwardk> | comes about from the types library mashing everything into one rep |
| 13:46:49 | × | drbean quits (~drbean@TC210-63-209-85.static.apol.com.tw) (Ping timeout: 260 seconds) |
| 13:47:07 | × | outerpassage quits (~outerpass@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Ping timeout: 260 seconds) |
| 13:48:58 | <Cale> | On the one hand, this is all kind of cool, on the other hand, it's definitely crossing the line into dependently-typed stuff that I think Haskell just plain isn't good at yet. I think if you actually need explicit singletons, that's a pretty good indication of "oops, Haskell is going to suck at this". I wonder how long until we can realistically have a working pi. |
| 13:50:24 | → | troydm joins (~troydm@unaffiliated/troydm) |
| 13:50:43 | × | polyrain quits (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 13:51:27 | hackage | inline-c 0.9.1.2 - Write Haskell source files including C code inline. No FFI required. https://hackage.haskell.org/package/inline-c-0.9.1.2 (FrancescoMazzoli) |
| 13:53:37 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Ping timeout: 264 seconds) |
| 13:55:21 | → | jespada joins (~jespada@148.252.133.47) |
| 13:55:34 | → | acidjnk_new2 joins (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) |
| 13:55:47 | <edwardk> | well, i have been building a little dependent type checker in haskell, and every time i move more stuff into my types i catch more bugs =) |
| 13:56:09 | <edwardk> | so i'm just trying to push a few more things into them |
| 13:56:17 | <edwardk> | which is what prompted the singleton push |
| 13:56:31 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 13:56:36 | <edwardk> | getting the singleton stuff to be super fast and more homogeneous made me happy, til Nat made me sad |
| 13:59:56 | → | caumeslasal joins (~Thunderbi@157.139.207.77.rev.sfr.net) |
| 14:00:29 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 14:00:35 | × | caumeslasal quits (~Thunderbi@157.139.207.77.rev.sfr.net) (Client Quit) |
| 14:00:39 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:01:06 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 14:01:17 | → | son0p joins (~son0p@186.159.4.142) |
| 14:03:37 | × | kicov quits (959c7c03@nat.ds3.agh.edu.pl) (Remote host closed the connection) |
| 14:05:49 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 14:06:41 | → | gmt joins (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) |
| 14:06:53 | → | Ashely3 joins (5beb81b2@gateway/web/cgi-irc/kiwiirc.com/ip.91.235.129.178) |
| 14:08:36 | <edwardk> | i suppose what i could do is build a type data Unnat = Add Int# Nat -- relying on the fact that Int# doesn't promote so we don't have to worry about any 'native' terms in kind Unnat. use my data family trick to inject a S constructor, and one for, so that it morally models data Unnat = S Unnat | N Nat -- so i can distinguish between the base number type i got from type Nat and the number of times i called S on it |
| 14:08:56 | <edwardk> | that way i don't need to worry about S 1 ~ 2 causing the universe to collapse or something |
| 14:10:48 | <edwardk> | another another option is to just do what I do now which is use an hlist and carry a witness of the length around rather than use Vec a N |
| 14:11:05 | × | gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 240 seconds) |
| 14:11:16 | <Cale> | Also, I haven't really thought very hard about how this suggestion might help, but generally I think if you're going to use overlapping instances in order to compute things, everything is okay in the case that you can manage to avoid exporting the class. |
| 14:11:32 | → | polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) |
| 14:11:38 | <edwardk> | the class here is a very public offering |
| 14:11:41 | <Cale> | yeah |
| 14:12:06 | <edwardk> | i was hoping to split this out and ran into this issue while writing up examples |
| 14:12:44 | <edwardk> | i had started looking for 'all the instances i can add to base' when i ran afoul of this |
| 14:12:47 | <Cale> | I don't know if there's a way to make a private analogue and get anything related to what you want (like, make a public instance for that class that depends on an instance of the class that nobody's allowed to see, maybe) |
| 14:12:49 | <edwardk> | er from base |
| 14:13:24 | laxask | is now known as sudden |
| 14:13:42 | × | Ashely3 quits (5beb81b2@gateway/web/cgi-irc/kiwiirc.com/ip.91.235.129.178) (Disconnected by services) |
| 14:13:46 | <edwardk> | i'm inclined to just yolo the data family S thing |
| 14:13:50 | <edwardk> | and go on with my day |
| 14:13:56 | <edwardk> | and if it bites anyone say 'don't do that' |
| 14:14:17 | → | Ashely3 joins (c247e36b@gateway/web/cgi-irc/kiwiirc.com/ip.194.71.227.107) |
| 14:14:25 | × | Ashely3 quits (c247e36b@gateway/web/cgi-irc/kiwiirc.com/ip.194.71.227.107) (Disconnected by services) |
| 14:15:03 | <edwardk> | data family S' :: Nat -> k; type S :: Nat -> Nat; type S = S' -- just works .. til you need to feed it to + and want + to actually compute, because they closed the type family for + |
| 14:15:07 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 14:15:17 | <edwardk> | but i could offer my own + and have it delegate to the main + once i changed out the S's |
| 14:15:47 | <edwardk> | but then the benefit of working with base Nat is fleeing fast |
| 14:17:20 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 14:17:43 | × | nyd quits (~nyd@unaffiliated/elysian) (Quit: nyd) |
| 14:18:31 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 14:19:38 | <edwardk> | i want a way to export a thing only at the type level without having to infect it with a type like Type that doesn't exist as a term. |
| 14:19:52 | <edwardk> | where i can have constructors in it, without using my data families |
| 14:20:08 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Ping timeout: 272 seconds) |
| 14:20:52 | <edwardk> | leaning towards exporting my own Nat type, ignoring the TypeNats Nat and going on my way. |
| 14:21:19 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 14:21:47 | <edwardk> | since Natural currently doesn't promote i _could_ use the data family hack to put Z and S in it as a kind. |
| 14:21:52 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 14:22:15 | <edwardk> | then you could use linear time slow SingI instances if you had to |
| 14:23:16 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 14:23:17 | <edwardk> | and i'd have both Nat and Natural, with the former working for when i want a large literal and the latter when i want induction for things like environments that'll usually get built from 0, til... next ghc release or so when they merge Nat and Natural |
| 14:23:28 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 14:24:01 | <edwardk> | to make the linear time thing less awful, i could emulate a better basis, like binary nats, or zeroless binary or something. |
| 14:25:04 | → | bloodstalker joins (~bloodstal@46.166.187.178) |
| 14:25:09 | <edwardk> | that'd get me log time literals, and Z and S become type families acting on the type, but they require more type information about the rest of the nat to know what to do at some points |
| 14:25:42 | <edwardk> | where peano can succ without forcing or matching on anything |
| 14:25:58 | → | __Joker joins (~Joker@180.151.105.65) |
| 14:27:05 | <Cale> | Yeah, how does merging Nat and Natural work with type families wanting to compute anything? |
| 14:27:11 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 265 seconds) |
| 14:27:18 | <Cale> | I mean, in the future GHC case |
| 14:27:56 | → | kicov joins (959c7c03@nat.ds3.agh.edu.pl) |
| 14:28:56 | <Cale> | I guess they just have wired in type families anyway |
| 14:29:32 | <kicov> | Hi, just one more question - did someone try to use liquid haskell on lens? Got any tips how to write these annotations? `fn :: Int -> Lens' State a` doesn't work well |
| 14:30:54 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 272 seconds) |
| 14:31:00 | <Cale> | Is liquid haskell getting to the point where it can be used on nontrivial programs? |
| 14:31:19 | <kicov> | Just for reference: https://dpaste.com/H877D9HQU |
| 14:33:39 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-dtashatgyjqumlie) |
| 14:34:19 | <Cheery> | Haskell's still using STG in the runtime right? |
| 14:35:16 | <lechner> | Hi, will findFiles from System.Directory descend into subdirectories? |
| 14:35:23 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 14:35:30 | → | irc_user joins (uid423822@gateway/web/irccloud.com/x-yhvajookqrbnnurt) |
| 14:36:17 | <Cale> | Cheery: In name more than anything |
| 14:38:05 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 14:38:17 | <edwardk> | well, i suppose what i can do is this. i'll make Z and S hacks that can inhabit kind Natural for now. and when they merge I'll just take the name Nat and move them over there =) |
| 14:38:41 | <Cheery> | Cale: the 1992 paper describes the design space and abstract machine with denotational and operational semantics. Is this still the same? |
| 14:39:08 | <edwardk> | Cheery: the STG has gotten a few upgrades since then, dynamic pointer tagging, etc. |
| 14:39:20 | <edwardk> | but the general flavor is there |
| 14:39:23 | <Cale> | Understanding the original STG will still give a decent understanding of what exists today, even though it's no longer always spineless and usually no longer tagless |
| 14:40:13 | <Cale> | http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.19.411&rep=rep1&type=pdf -- "Putting the Spine back in the Spineless Tagless G-Machine" |
| 14:40:43 | <Cale> | https://simonmar.github.io/bib/papers/ptr-tagging.pdf -- "Faster laziness using dynamic pointer tagging" |
| 14:41:31 | → | pta2002 joins (~quassel@104.248.23.110) |
| 14:42:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 14:42:46 | → | urodna joins (~urodna@unaffiliated/urodna) |
| 14:43:53 | <Cheery> | I thought I do one last thing with RPython. Exploring eval/apply interpreters and STG. I'll see if there's something to propose in place of Javascript so that there's less room for people to replace it with crap. |
| 14:44:13 | <Cheery> | a nice FP runtime. :) |
| 14:44:13 | → | outerpassage joins (~outerpass@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) |
| 14:45:20 | <Cheery> | Also would love for an efficient logic programming runtime slipped in, but I'll try to not scope creep much. |
| 14:45:28 | × | CMCDragonkai1 quits (~Thunderbi@120.17.10.7) (Ping timeout: 272 seconds) |
| 14:47:04 | → | ddellacosta joins (~dd@86.106.121.168) |
| 14:48:22 | × | polyrain quits (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 14:49:33 | × | petersen quits (~petersen@redhat/juhp) (Quit: petersen) |
| 14:55:42 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 14:56:25 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 15:00:01 | × | jeremybennett quits (~jeremyben@185.244.214.216) () |
| 15:01:33 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 256 seconds) |
| 15:02:47 | <Orbstheorem> | If building a derivation is a linear process, why doesn't nix cache intemediate build steps ? (e.g. git@`buildPhase::c1kj2h31...`) |
| 15:03:08 | → | __Joker joins (~Joker@180.151.105.65) |
| 15:04:01 | × | outerpassage quits (~outerpass@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Quit: Leaving) |
| 15:08:16 | × | __Joker quits (~Joker@180.151.105.65) (Ping timeout: 272 seconds) |
| 15:08:26 | <Orbstheorem> | Oh, my bad, wrong buffer ><" |
| 15:10:39 | × | knupfer quits (~Thunderbi@i59F7FF48.versanet.de) (Quit: knupfer) |
| 15:10:39 | → | knupfer1 joins (~Thunderbi@200116b82c277000795bc1703ccafd48.dip.versatel-1u1.de) |
| 15:12:30 | → | pingiun joins (~pingiun@j63019.upc-j.chello.nl) |
| 15:12:48 | → | HeAvengin7_ joins (~sedx@112.198.75.236) |
| 15:13:03 | knupfer1 | is now known as knupfer |
| 15:16:30 | × | jespada quits (~jespada@148.252.133.47) (Read error: Connection reset by peer) |
| 15:16:45 | → | __Joker joins (~Joker@180.151.105.65) |
| 15:16:48 | × | HeAvengin7_ quits (~sedx@112.198.75.236) (Quit: Please click my blog: https://bit.ly/2RjfReh or https://bit.ly/33tb5lx) |
| 15:17:50 | <sm[m]> | hi lechner, doesn't it's doc say ? |
| 15:19:33 | × | dsf quits (~dsf@cpe-75-80-106-108.san.res.rr.com) (Ping timeout: 260 seconds) |
| 15:22:04 | → | ermau joins (~ermau@185.163.110.116) |
| 15:30:50 | × | knupfer quits (~Thunderbi@200116b82c277000795bc1703ccafd48.dip.versatel-1u1.de) (Quit: knupfer) |
| 15:31:14 | → | knupfer joins (~Thunderbi@200116b82c2770005077b6463d9d1f88.dip.versatel-1u1.de) |
| 15:32:40 | → | dsf joins (~dsf@cpe-75-82-64-167.socal.res.rr.com) |
| 15:37:11 | → | ClaudiusMaximus joins (~claude@198.123.199.146.dyn.plus.net) |
| 15:37:12 | × | ClaudiusMaximus quits (~claude@198.123.199.146.dyn.plus.net) (Changing host) |
| 15:37:12 | → | ClaudiusMaximus joins (~claude@unaffiliated/claudiusmaximus) |
| 15:39:57 | × | ukari quits (~ukari@unaffiliated/ukari) (Remote host closed the connection) |
| 15:40:42 | → | ukari joins (~ukari@unaffiliated/ukari) |
| 15:42:52 | → | Turmfalke joins (~user@unaffiliated/siracusa) |
| 15:46:22 | × | acidjnk_new2 quits (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 15:51:30 | × | kicov quits (959c7c03@nat.ds3.agh.edu.pl) (Remote host closed the connection) |
| 15:53:32 | → | gmt joins (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) |
| 16:00:39 | → | Rudd0 joins (~Rudd0@185.189.115.98) |
| 16:02:09 | × | gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 16:04:00 | → | outerpassage joins (outerpassa@2600:3c01::f03c:92ff:fed1:4643) |
| 16:04:11 | → | elliott_ joins (~elliott@2600:380:9266:42eb:7b5e:250e:ef35:8b08) |
| 16:07:59 | × | son0p quits (~son0p@186.159.4.142) (Read error: Connection reset by peer) |
| 16:09:19 | <lechner> | sm[m]: I am not sure. I can only see the "given list of directories"---which is elaborated on but not otherwise expanded to recursive behavior in the reference to findFilesWith here: https://hackage.haskell.org/package/directory-1.3.6.1/docs/System-Directory.html#v:findFiles |
| 16:11:01 | × | ryansmccoy quits (~ryansmcco@156.96.151.132) (Ping timeout: 264 seconds) |
| 16:11:12 | → | son0p joins (~son0p@186.159.4.142) |
| 16:11:28 | → | jflewkfjlwjefklf joins (~jfkeflkwe@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) |
| 16:11:42 | → | ryansmccoy joins (~ryansmcco@193.37.254.27) |
| 16:12:33 | × | jflewkfjlwjefklf quits (~jfkeflkwe@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Remote host closed the connection) |
| 16:16:59 | → | gmt joins (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) |
| 16:20:18 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-99-86.w86-212.abo.wanadoo.fr) |
| 16:20:52 | × | inkbottle quits (~inkbottle@aaubervilliers-654-1-100-182.w86-212.abo.wanadoo.fr) (Ping timeout: 256 seconds) |
| 16:22:18 | → | thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) |
| 16:22:23 | <thir> | #bitsnbugs |
| 16:22:33 | × | gmt quits (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) (Ping timeout: 260 seconds) |
| 16:22:47 | × | DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection) |
| 16:23:13 | → | DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) |
| 16:23:42 | ← | thir parts (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) () |
| 16:28:44 | → | pera joins (~pera@unaffiliated/pera) |
| 16:29:01 | → | Jeanne-Kamikaze joins (~Jeanne-Ka@104.200.129.62) |
| 16:30:36 | → | ajfelfjlsdkfjejf joins (~jfkeflkwe@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) |
| 16:31:27 | hackage | uniqueness-periods-vector-examples 0.5.3.0 - Examples of usage for the uniqueness-periods-vector series of packages https://hackage.haskell.org/package/uniqueness-periods-vector-examples-0.5.3.0 (OleksandrZhabenko) |
| 16:31:28 | × | carlomagno quits (~cararell@inet-hqmc02-o.oracle.com) (Remote host closed the connection) |
| 16:31:45 | → | jespada joins (~jespada@148.252.133.47) |
| 16:32:15 | → | carlomagno joins (~cararell@inet-hqmc02-o.oracle.com) |
| 16:32:27 | × | zopsi quits (~zopsi@irc.dir.ac) (Remote host closed the connection) |
| 16:32:45 | → | gestone joins (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) |
| 16:33:23 | → | zopsi joins (zopsi@2600:3c00::f03c:91ff:fe14:551f) |
| 16:33:26 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 16:34:39 | → | fendor joins (~fendor@77.119.128.171.wireless.dyn.drei.com) |
| 16:35:33 | × | ericsagnes quits (~ericsagne@2405:6580:0:5100:59cb:4e8f:c201:4e04) (Ping timeout: 272 seconds) |
| 16:35:40 | → | aenesidemus joins (~aenesidem@c-73-53-247-25.hsd1.fl.comcast.net) |
| 16:39:20 | → | tzh joins (~tzh@2601:448:c500:5300::ad1c) |
| 16:39:20 | × | cheater quits (~user@unaffiliated/cheater) (Quit: BitchX: the new hardcore, psycho, nitro client -- in a can) |
| 16:41:53 | → | cheater joins (~user@unaffiliated/cheater) |
| 16:43:26 | × | knupfer quits (~Thunderbi@200116b82c2770005077b6463d9d1f88.dip.versatel-1u1.de) (Ping timeout: 244 seconds) |
| 16:47:21 | → | ericsagnes joins (~ericsagne@2405:6580:0:5100:5585:9ff6:72b9:d99a) |
| 16:48:02 | <sm[m]> | lechner: you're right, it's not crystal clear, but yes I'm 99% sure it descends. Probably you tested it by now |
| 16:49:03 | → | Dolly joins (585fd1fd@ti0203q160-5312.bb.online.no) |
| 16:49:48 | → | knupfer joins (~Thunderbi@i59F7FF48.versanet.de) |
| 16:49:55 | → | igghibu joins (~igghibu@net-93-66-17-40.cust.vodafonedsl.it) |
| 16:50:47 | × | pingiun quits (~pingiun@j63019.upc-j.chello.nl) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 16:51:09 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 16:53:42 | <nshepperd2> | whoa i just converted this dynamic programming-based tokenization thing from a laziness based pure Vector implementation to a mutable unboxed vector in ST, and it got like 100 times faster |
| 16:54:02 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 16:54:26 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 16:54:39 | <ski> | top-down to bottom-up ? |
| 16:54:45 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 16:55:52 | <nshepperd2> | I'm not quite sure what those terms mean, but yes I think so |
| 16:57:15 | <nshepperd2> | the lazy one was let table = V.generate (n+1) go; go = ...; in table!n |
| 16:57:19 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 16:57:45 | <nshepperd2> | the fast one was to make a mutable unboxed vector and fill it out in order from 0 to n |
| 16:57:49 | <ski> | where `go' referred to `table' |
| 16:57:55 | <nshepperd2> | yeah |
| 16:58:17 | <sshine> | >_< |
| 16:58:24 | <ski> | hm, what kind of access pattern ? |
| 16:59:25 | <nshepperd2> | 'go i' would reference some or all cells between i-5 and i-1 |
| 16:59:34 | <hekkaidekapus> | sm[m]: The 1% wins again :p It does not descend. At its core, the function calls doesFileExist to the supplied dirs. |
| 17:00:12 | × | ajfelfjlsdkfjejf quits (~jfkeflkwe@2600:1700:4640:c560:68bd:9d76:dbd8:24e7) (Quit: Leaving) |
| 17:00:20 | <hekkaidekapus> | doesFileExist (dir </> file) |
| 17:00:24 | <ski> | "bottom-up" means that you fill in the "lower cells", before the higher ones, "prematurely" so to speak. "top-down" that you start demanding higher ones, which in turn demands lower ones (which are cached) |
| 17:00:39 | <dolio> | There's a lot of overhead in the top-down lazy approach. |
| 17:00:54 | <dolio> | If you're working with integers. |
| 17:01:10 | → | sleblanc joins (~sleblanc@unaffiliated/sebleblanc) |
| 17:01:47 | <nshepperd2> | ski: then yeah, that's exactly what i did |
| 17:01:59 | <ski> | nshepperd2 : i suppose you could even use a five-tuple, or a vector of size five, then |
| 17:02:41 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 260 seconds) |
| 17:03:28 | × | igghibu quits (~igghibu@net-93-66-17-40.cust.vodafonedsl.it) (Quit: Konversation terminated!) |
| 17:03:37 | <dolio> | Yeah, like computing fibonacci with an accumulator pair. |
| 17:04:10 | <ski> | (you'd use `mod i 5') |
| 17:05:09 | <ski> | i suppose the computation of the next cell isn't a linear function of the previous five ones .. |
| 17:05:10 | × | zaquest quits (~notzaques@5.128.210.178) (Quit: Leaving) |
| 17:06:52 | × | elliott_ quits (~elliott@2600:380:9266:42eb:7b5e:250e:ef35:8b08) (Ping timeout: 260 seconds) |
| 17:07:20 | <ski> | nshepperd2 : probably the lazy approach would work better, in case there's many cells which aren't needed to compute the result |
| 17:07:38 | → | coot joins (~coot@37.30.49.42.nat.umts.dynamic.t-mobile.pl) |
| 17:08:00 | → | notzmv` joins (~user@177.103.86.92) |
| 17:08:11 | <dolio> | Yeah, there are a lot of factors making it sub-optimal for this case. |
| 17:08:29 | → | zaquest joins (~notzaques@5.128.210.178) |
| 17:08:37 | → | hyperisco joins (~hyperisco@d192-186-117-226.static.comm.cgocable.net) |
| 17:10:10 | × | cheater quits (~user@unaffiliated/cheater) (Read error: Connection reset by peer) |
| 17:10:37 | <sshine> | I have a data type, data Foo a = X a | Y a | Z a | P | Q | R; and I'd like to make a type NumFoo = forall n. Num n => Foo n, but it seems that I can't do that. what are my alternatives? I was thinking of a data type with a type class constraint. |
| 17:10:59 | <sshine> | I think I can use GADTs, but that would require me to alter 'Foo', too, right? |
| 17:11:18 | × | notzmv quits (~user@unaffiliated/zmv) (Ping timeout: 256 seconds) |
| 17:11:46 | → | cheater joins (~user@unaffiliated/cheater) |
| 17:11:55 | <nshepperd2> | ski: yeah in this case pretty much all cells are eventually needed |
| 17:13:30 | <ski> | sshine : why can't you ? |
| 17:13:33 | <hyperisco> | sshine, what is the idea of this type? I don't understand |
| 17:14:26 | <ski> | a value of type `NumFoo' possibly contains a number of any numeric type the user wants to get |
| 17:14:52 | → | Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 17:15:26 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Remote host closed the connection) |
| 17:16:00 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 17:16:27 | → | igghibu joins (~igghibu@91.193.5.10) |
| 17:16:50 | × | Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 272 seconds) |
| 17:16:50 | Lord_of_Life_ | is now known as Lord_of_Life |
| 17:22:38 | × | igghibu quits (~igghibu@91.193.5.10) (Quit: Textual IRC Client: www.textualapp.com) |
| 17:22:54 | <zebrag> | I believe `cons :: a -> List l a -> List (Succ l) a` cannot be done with plain GADT? (The following ref, might suggest it could be done?? https://www.cis.upenn.edu/~sweirich/talks/GADT.pdf, page 9) |
| 17:23:15 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 17:23:45 | <hyperisco> | zebrag, is there a compiler error you're seeing? |
| 17:23:56 | × | Dolly quits (585fd1fd@ti0203q160-5312.bb.online.no) (Remote host closed the connection) |
| 17:24:14 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Remote host closed the connection) |
| 17:24:18 | <zebrag> | At least if you consider `Succ` is a data constructor |
| 17:24:25 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 17:24:39 | <zebrag> | hyperisco: no I'm just reading the slides above |
| 17:25:59 | <hyperisco> | all I don't understand is how that is an example of dependent types |
| 17:26:07 | × | tzh quits (~tzh@2601:448:c500:5300::ad1c) (Ping timeout: 260 seconds) |
| 17:26:20 | <hyperisco> | what is your objection? |
| 17:26:37 | → | kindaro joins (5f6e6241@h95-110-98-65.dyn.bashtel.ru) |
| 17:26:57 | × | suppi quits (~suppi@172.246.241.246) (Ping timeout: 260 seconds) |
| 17:27:06 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Remote host closed the connection) |
| 17:27:26 | → | pingiun joins (~pingiun@j63019.upc-j.chello.nl) |
| 17:27:30 | → | Dolly joins (585fd1fd@ti0203q160-5312.bb.online.no) |
| 17:29:08 | <Cale> | sshine: Just replace "type NumFoo = ..." with "data NumFoo = ..." and what you wrote is valid code, if a little bit useless. Forgetting everything about the type of number except that it was a type of number will mean that you can't really do a whole lot with it (in particular, you won't know that it's the same type as any other type of number, so the arithmetic you can perform is very limited) |
| 17:30:13 | <Cale> | sshine: Or did you really want to define a type synonym for the universal type? |
| 17:31:09 | <c_wraith> | Cale: it's a bit worse than that since Show is no longer a superclass of Num. Num doesn't give you any eliminator to see the value. |
| 17:31:10 | × | DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection) |
| 17:31:18 | <Cale> | Right |
| 17:31:27 | <Cale> | and Eq is gone too |
| 17:31:48 | <c_wraith> | Eq would be pretty useless, though, unless you wanted to test for lack of reflexivity or something |
| 17:32:16 | <Cale> | You could test out arithmetical identities involving your one value of the given type :) |
| 17:32:41 | <c_wraith> | hah. is x + x == x ? :) |
| 17:32:45 | <Cale> | yeah |
| 17:33:08 | <hyperisco> | no |
| 17:33:15 | → | GyroW_ joins (~GyroW@ptr-48ujrfb8c7gfd2lu92q.18120a2.ip6.access.telenet.be) |
| 17:33:18 | × | supercoven quits (~Supercove@dsl-hkibng32-54fb54-166.dhcp.inet.fi) (Ping timeout: 272 seconds) |
| 17:33:43 | <Cale> | (that's essentially the same as checking if x == 0, if the instance is lawful) |
| 17:33:48 | <c_wraith> | I suppose the Num instance would let you throw in literals too, so you could ask if x * 0 == x |
| 17:33:49 | × | GyroW quits (~GyroW@unaffiliated/gyrow) (Ping timeout: 272 seconds) |
| 17:33:51 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 17:34:21 | <c_wraith> | That's not true in a modular ring |
| 17:34:41 | <c_wraith> | Oh, I guess it is. nevermind me! |
| 17:34:49 | <phadej> | x * 0 = 0, not x ? |
| 17:35:14 | <Cale> | That was another equation that would only be satisfied when x == 0 |
| 17:35:27 | <c_wraith> | Anyway. The real point is that a value of an unknown type with a Num instance is very low. |
| 17:35:28 | <Cale> | (again, a fun thing to check holds in any ring) |
| 17:35:37 | <hyperisco> | I guess you can use this to dynamically determine which laws might hold |
| 17:35:54 | → | tzh joins (~tzh@c-73-94-222-143.hsd1.mn.comcast.net) |
| 17:35:56 | <c_wraith> | If you add in Eq, you can do that |
| 17:36:07 | <c_wraith> | but with *just* Num, you've got basically nothing. |
| 17:36:24 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) |
| 17:36:25 | <hyperisco> | I feel like Num without Ord is amiss |
| 17:36:52 | <c_wraith> | so... not a fan of complex numbers? |
| 17:37:23 | <hyperisco> | you telling me they can't be ordered or are you telling me Ord is too strong |
| 17:37:39 | <merijn> | hyperisco: There's two separate and equally valid orderings for them |
| 17:37:43 | <geekosaur> | they can't be ordered |
| 17:37:46 | <merijn> | Well, technically probably more |
| 17:37:54 | <geekosaur> | or, what merijn said. |
| 17:37:55 | <merijn> | But they can't be ordered in a arithmetically meaningful way |
| 17:38:06 | <merijn> | hyperisco: Consider this |
| 17:38:22 | <merijn> | hyperisco: Is "1 + 0i" > than "0 + 1i" or not? |
| 17:38:29 | → | Chi1thangoo joins (~Chi1thang@87.112.60.168) |
| 17:38:55 | <geekosaur> | basically "Ord" only makes sense if they can be squashed down to a line without data loss. complex numbers, quaternions, etc. have infinitely many such squashings, none of which has any claim to being primary |
| 17:39:05 | <hyperisco> | so you're telling me Ord is too strong |
| 17:39:23 | <merijn> | You could argue Num should be Eq |
| 17:39:30 | <merijn> | Which, in fact, the Haskell Report does |
| 17:39:37 | <merijn> | GHC ignores that, however |
| 17:39:40 | → | acidjnk_new2 joins (~acidjnk@p200300d0c736584378afc0f7e05aaafd.dip0.t-ipconnect.de) |
| 17:39:43 | <hyperisco> | what about the cherished function instance though |
| 17:39:49 | <merijn> | The report also mandates a Show instance as superclass of Num |
| 17:39:58 | <merijn> | hyperisco: Those aren't legal per the report |
| 17:40:02 | → | borne joins (~fritjof@200116b86490460022497ba62715fb72.dip.versatel-1u1.de) |
| 17:40:08 | <merijn> | Since they can't have Eq or Show |
| 17:40:14 | <hyperisco> | well the report can stuff itself in regards to Num |
| 17:40:29 | <merijn> | hyperisco: Well, you wanted Ord |
| 17:40:29 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 17:40:34 | <merijn> | hyperisco: Which requires Eq :p |
| 17:40:34 | <hyperisco> | it started this mess |
| 17:40:45 | <merijn> | hyperisco: So insisting on Ord for Num kills that instance too :p |
| 17:41:01 | <merijn> | It's easy |
| 17:41:01 | <monochrom> | "forall n. Num n => n" is very likely the same as "Integer". |
| 17:41:14 | <hyperisco> | if you think I'm giving one consistent position here, I'm not |
| 17:41:15 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 17:41:15 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Client Quit) |
| 17:41:20 | <merijn> | Num is perfectly adequate if you just give up on any notion of "math" definitions of arithmetic |
| 17:41:33 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 17:41:38 | <merijn> | hyperisco: There've been 50 different Num hierarchies "better" than the current one proposed |
| 17:41:56 | <merijn> | But no one uses them, because they're all a pain for anything anyone actually cares about doing |
| 17:41:57 | <phadej> | Num is an unsuccessful attempt to unify operations on `Integer` and `Double` |
| 17:41:58 | → | shad0w_ joins (~shad0w_@160.202.36.27) |
| 17:42:06 | <monochrom> | But you can't squash down those 50 alternatives down to a line. :) |
| 17:42:15 | <hyperisco> | I doubt it |
| 17:42:21 | <merijn> | Turns out the current Num hierarchy does passably well at "stuff people actually care about" |
| 17:42:34 | <phadej> | right now I think that exact and inexact math should just had different operator set :) |
| 17:42:35 | <Cale> | I think Num is pretty okay at the moment. The main things which always bothered me before were the Show and Eq constraints, and those are gone. |
| 17:42:35 | <merijn> | hyperisco: Well, feel free to work out and propose alternative 51 :) |
| 17:42:40 | <hyperisco> | no |
| 17:42:42 | <merijn> | Maybe this time someone will get it right :) |
| 17:43:03 | <hyperisco> | PureScript has a different hierarchy and soils it with invalid instances |
| 17:43:15 | <Cale> | signum/abs being there is a little weird perhaps, but those are always definable in some fashion |
| 17:43:16 | <monochrom> | I am somewhat bothered by the opposite, Cale. For example allowing X->Integer to be a Num instance. |
| 17:43:21 | <hyperisco> | but other than that, I've personally found ample utility in it |
| 17:43:43 | <merijn> | I have no clue about purescript's hierarchy |
| 17:43:58 | <hyperisco> | it is more disciplined than a bag called Num |
| 17:44:06 | <phadej> | I think PureScript makes the same mistake, by having e.g. Double as part of "the only numeric hierarchy" |
| 17:44:22 | <hyperisco> | but then it goes and gives the usual Double instance and pretends Int is Integer |
| 17:44:43 | <monochrom> | Then again I'm bothered by signum and abs, too. |
| 17:44:46 | <merijn> | hyperisco: Well, what's the alternative? |
| 17:44:49 | → | MorrowM joins (~max@bzq-110-168-31-106.red.bezeqint.net) |
| 17:44:59 | <merijn> | Do an Ocaml and use a different + for Int and Double? |
| 17:45:08 | <monochrom> | Yes. |
| 17:45:11 | <hyperisco> | I recommended that |
| 17:45:24 | <merijn> | That's one of the worst things in ocaml >.< |
| 17:45:32 | <monochrom> | It is why I came over to Haskell. :) |
| 17:45:32 | → | Tesseraction joins (~Tesseract@unaffiliated/tesseraction) |
| 17:45:36 | <hyperisco> | though the issue starts at division, not +, for Int |
| 17:45:39 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 17:45:58 | <hyperisco> | so long as we're willing to accept the reality that Int is a modular ring |
| 17:46:10 | <merijn> | hyperisco: Well, how is your hypothetical hierarchy going to unify + for Int and Double and not get this "wrong instance" for Double you're complaining about |
| 17:46:15 | <hyperisco> | a hard thing for programmers to do, seems |
| 17:46:30 | <hyperisco> | well that's easy |
| 17:46:37 | <hyperisco> | you just cast Double out of the hierarchy altogether |
| 17:46:41 | × | gestone quits (~gestone@c-98-225-37-68.hsd1.wa.comcast.net) (Quit: Lost terminal) |
| 17:46:43 | <merijn> | Right |
| 17:46:59 | <merijn> | So then + doesn't work on Double, but you just said the division start at division |
| 17:47:06 | <hyperisco> | and then you do the harder thing of figuring out truthful axioms for Double |
| 17:47:25 | <hyperisco> | for Int it does |
| 17:47:48 | <hyperisco> | for Double the problem started at the beginning |
| 17:47:55 | <dolio> | Maybe you could accept that not every type class needs to be a grand mathematical design, and sometimes people just want to overload stuff. |
| 17:48:23 | <hyperisco> | frankly that isn't why I use these languages |
| 17:49:16 | <hyperisco> | and I find it bemusing how concerned people get about overloading syntax |
| 17:49:51 | <hyperisco> | how do we get on if + cannot be used for both Int and Double in the same module |
| 17:53:17 | <maralorn> | I wanna design a small library and am uncertain about the design. I want to specify A) a data type representing certain dialog interactions with a user (like a menu, a text input, a yes/no question) and B) multiple implementations of IO actions that execute that dialog. So far so easy. But now I wonder how I can make the type of possible dialogs composable and giving the handlers an option to specify which types of dialogs |
| 17:53:17 | <maralorn> | they support. And I wonder if that's worth it. Because for my use case I could probably just have one data type for "dialogs" and extend it whenever I need to. |
| 17:54:18 | <hyperisco> | merijn, oh sorry I think the division is fine, though there are different ways to do it, but the problem starts at Euclidean rings because Int is not an integral domain |
| 17:54:41 | <maralorn> | On the other hand specifying possible dialog variants in a type level list will probably multiple my development time and lower the ease of use. |
| 17:55:13 | → | juuandyy joins (~juuandyy@90.166.144.65) |
| 17:55:23 | × | knupfer quits (~Thunderbi@i59F7FF48.versanet.de) (Ping timeout: 240 seconds) |
| 17:56:08 | <hyperisco> | merijn, no scratch that, EuclideanRing defines division. :P clumsily remembering the hierarchy |
| 17:56:14 | → | perrier-jouet joins (~perrier-j@modemcable012.251-130-66.mc.videotron.ca) |
| 17:56:25 | × | orion quits (~orion@unaffiliated/orion) (Ping timeout: 240 seconds) |
| 17:56:33 | ski | looks at sshine |
| 17:56:42 | → | suppi joins (~suppi@172.246.241.246) |
| 17:56:51 | MarcelineVQ | looks at rcloud |
| 17:56:54 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 17:56:54 | <hyperisco> | there is DivisionRing which defines multiplicative inverses but that can't be closed on Int |
| 17:57:03 | → | Lycurgus joins (~niemand@98.4.96.130) |
| 17:58:13 | <hyperisco> | but for example, I can count with semirings, and that has been helpful (technically could with a group, but for whatever reason groups are omitted from the hierarchy, painfully) |
| 17:58:54 | → | dansho joins (~dansho@ip68-108-167-185.lv.lv.cox.net) |
| 17:59:36 | → | worc3131 joins (~quassel@2a02:c7f:c026:9500:7d0b:65d0:38a4:4786) |
| 17:59:38 | <Cale> | hyperisco: Well, Euclidean domains usually are required to be integral domains, but practically speaking, I'm not sure how much trouble you run into with the generalisation... |
| 18:00:02 | × | ermau quits (~ermau@185.163.110.116) () |
| 18:00:16 | <hyperisco> | both instances given in the Prelude for PS are invalid, so I guess you run into trouble on all counts :P |
| 18:00:28 | <Cale> | for PS? |
| 18:00:33 | <hyperisco> | PureScript |
| 18:01:28 | Lycurgus | just reviewed from herstein the group/ring distinction |
| 18:02:13 | → | wavemode joins (~wavemode@097-070-075-143.res.spectrum.com) |
| 18:02:45 | <hyperisco> | I am guessing there are semirings and rings I could avail myself of but I am not instinctively inclined to see things that way yet |
| 18:03:10 | <Cale> | What's wrong with it apart from Int not being an integral domain? |
| 18:03:28 | <Cale> | (I'm not very familiar with purescript) |
| 18:04:13 | → | knupfer joins (~Thunderbi@i59F7FF48.versanet.de) |
| 18:04:42 | <hyperisco> | I stopped investigating at that point, I don't know if anything else is wrong |
| 18:04:59 | → | Sgeo joins (~Sgeo@ool-18b982ad.dyn.optonline.net) |
| 18:05:25 | maralorn | thinks, that trying to closely match any detailed mathematical hierarchy is to rigid. I guess Num is okayish. But I think I would go for more finegrained classes if someone forced me to think of a "correct" definition. Like have one for addition, another one for subtraction, one for multiplication, one or I guess two for division ... |
| 18:05:25 | → | AlterEgo__ joins (~ladew@124-198-158-163.dynamic.caiway.nl) |
| 18:05:31 | × | AlterEgo__ quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Remote host closed the connection) |
| 18:05:55 | <hyperisco> | I was doing something or other with Euclidean spaces I think and it became relevant to have actual an actual Euclidean ring |
| 18:06:15 | <hyperisco> | even the approximation of Double is more palatable than Int |
| 18:06:50 | <hyperisco> | but literally the all-powerful overloaded syntax argument was wheeled out to defend it |
| 18:07:17 | <hyperisco> | and if you're going to do that, I say Num was better |
| 18:07:22 | × | andreas303 quits (~andreas@gateway/tor-sasl/andreas303) (Remote host closed the connection) |
| 18:07:35 | <hyperisco> | lawless, no one ought to care that much about it, just a bag of overloaded names |
| 18:08:01 | × | hiroaki quits (~hiroaki@2a02:908:4b14:d500:8d4c:a111:9cac:718b) (Ping timeout: 272 seconds) |
| 18:08:16 | <hyperisco> | problem is, people aren't viewing this right, and I know it |
| 18:09:17 | <hyperisco> | if you started caring about, say, a Euclidean ring generically, ie the only thing important is the Euclidean ring itself, not any particular instances |
| 18:09:40 | <Cale> | Wait, Double isn't a useful approximation of a Euclidean domain... except in a trivial way |
| 18:09:44 | <hyperisco> | then you'd be upset that after going through that work it could be instantiated with potentially program-crashing instances |
| 18:10:23 | <Cale> | Fields are technically Euclidean domains, they're not very interesting ones though. |
| 18:10:33 | → | andreas303 joins (~andreas@gateway/tor-sasl/andreas303) |
| 18:13:05 | <hyperisco> | all I am saying is that I prefer the problems of Double to the problems of Int |
| 18:13:19 | <Cale> | ah |
| 18:14:01 | merijn | just embraced anarchy and lawlessness |
| 18:14:14 | <merijn> | Seems better for my blood pressure :p |
| 18:15:06 | × | xerox_ quits (~xerox@unaffiliated/xerox) (Ping timeout: 272 seconds) |
| 18:15:12 | × | jespada quits (~jespada@148.252.133.47) (Quit: Sleeping) |
| 18:16:52 | <hyperisco> | I appreciate how rarified the atmosphere is to be arguing with Haskellers over their precision |
| 18:17:31 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 18:17:54 | <Cale> | I just think I'd rather save a proper Ring class hierarchy for when we get dependent types, and even then, it probably doesn't need to be in the Prelude. |
| 18:18:33 | <hyperisco> | what can we gain from dts here? |
| 18:18:49 | <Cale> | Then you can add the actual laws as methods |
| 18:19:10 | <hyperisco> | oh well I feel like that is a broader discussion about how class laws are treated |
| 18:20:20 | <hyperisco> | Idris chose to have lawful and lawless versions of each class, and that seems odd |
| 18:21:17 | <Cale> | I think it makes sense if you try to use the lawful ones and don't enjoy wasting your time convincing the computer :P |
| 18:21:29 | <MarcelineVQ> | that's because idris isn't a proof assistant, it's a gp programming language, and a gp language should endeavor to be useable |
| 18:21:53 | → | laen_ joins (~laen_@s91904426.blix.com) |
| 18:22:01 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 18:22:02 | <hyperisco> | that is fine but why is that the chosen escape hatch |
| 18:22:11 | <hyperisco> | because another option is to just leave the proofs as TODOs |
| 18:22:16 | <MarcelineVQ> | There's other escape hatches, what problem are we escaping? |
| 18:23:05 | <geekosaur> | carrying around proofs that your typeclass instances are law-abiding |
| 18:23:20 | × | nibbling quits (~nibbling@165.227.18.242) (Quit: WeeChat 2.6) |
| 18:23:21 | <Cale> | The proposition might actually be untrue, but you might know that the extent to which it's untrue doesn't matter to you |
| 18:23:35 | <Cale> | (like in the case of most uses of Double for arithmetic) |
| 18:23:52 | <hyperisco> | I'd expect in Haskell, if we had such lawful classes, we could write in error "TODO" or some such instead of a proof |
| 18:23:57 | <MarcelineVQ> | The issue with providing an instance that claims to enforce laws and then not enforcing them is that you have users, and users and surprises are a bad combination |
| 18:24:45 | <hyperisco> | I don't feel like that tracks with the pragmatism argument though |
| 18:25:05 | <MarcelineVQ> | As a user I pragmatically don't like surprises :X |
| 18:25:35 | <hyperisco> | if I make a library do I require you to give me lawful or lawless instances? |
| 18:25:45 | <phadej> | Cale: it's fun (when you think about it) that there's plenty of research how to make computing with IEEE754 less-imprecise / numerically stable / ... |
| 18:25:47 | <hyperisco> | I'm deciding what work you need to do for me, at that point |
| 18:26:16 | <phadej> | Cale: and all of that is thrown away when you try to fit into (just) + and * of Ring class (for example) |
| 18:26:31 | <phadej> | repeating what I said, it is a wrong abstraction |
| 18:27:08 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 18:27:09 | <hyperisco> | on the flip, you give me a lawful instance and it is not truly law-abiding, I'll be upset, true |
| 18:27:13 | <phadej> | something as 'basic' as FMA |
| 18:27:51 | <phadej> | https://gitlab.haskell.org/ghc/ghc/-/issues/10364 :( |
| 18:27:52 | <Cale> | In what way do we throw out numerical stability analysis? |
| 18:28:14 | <phadej> | e.g. not offering fma, for example |
| 18:28:28 | <Cale> | Oh, I see, you just want more operations |
| 18:28:36 | <Cale> | I don't think that requires removing + and * |
| 18:29:09 | <hyperisco> | Cale, it is just that if Double actually works then probably the algebraic structure never mattered |
| 18:29:16 | <MarcelineVQ> | "<hyperisco> I'm deciding what work you need to do for me, at that point" Indeed, that's an issue with laws at api boundries, it's also why I so far advocate to not let dependent types into your api's. |
| 18:29:30 | <hyperisco> | the issue of perspective I am seeing is that people argue from a specific instance, rather than arguing from the algebraic structure |
| 18:29:33 | <Cale> | hyperisco: It *approximately* matters :) |
| 18:29:38 | <hyperisco> | and that is how we get syntax arguments |
| 18:30:19 | <Cale> | The algebraic laws are stated as equations, while what the application probably needed was only inequalities which bounded those things to be true within some interval of error |
| 18:30:49 | <Cale> | and only for values in a particular range |
| 18:30:56 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 18:32:04 | <hyperisco> | fine, but still did the generalisation of that structure, realised as a type class, ever matter |
| 18:32:12 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 18:32:34 | <hyperisco> | and I'm not saying you're making this argument |
| 18:33:34 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) (Quit: Quit.) |
| 18:34:45 | <Cale> | Not all that much, but it allowed for overloading, and possibly some reuse of functions defined in terms of Num which aren't part of it |
| 18:36:24 | <Cale> | phadej: I think to start with, we should have all the operations like fma but not in a class. |
| 18:36:37 | <Cale> | (maybe in their own class) |
| 18:37:03 | <phadej> | Cale: I'd argue that Double shouldn't be Num (or whatever Ring) to begin with |
| 18:37:03 | <Cale> | Presumably that could be done as a library, though perhaps it's worth wiring the operations into GHC... |
| 18:37:36 | <Cale> | Meh, it's got operations which roughly correspond to the operations of Num to the point that the meanings of things are predictable. |
| 18:37:37 | <phadej> | if you really want, then there could be a newtype wrapping IEEE754 type and pretending it's a Num (or Ring) |
| 18:38:28 | → | jespada joins (~jespada@90.254.241.6) |
| 18:38:36 | <Cale> | I don't think there's all that much value in making it any less convenient to add and multiply Double values |
| 18:39:01 | <Cale> | Or interpret integer literals as Double values, for that matter |
| 18:39:15 | <hyperisco> | biased way to put it but sure, I'd prefer not to lose that |
| 18:39:25 | × | son0p quits (~son0p@186.159.4.142) (Ping timeout: 240 seconds) |
| 18:39:39 | × | jespada quits (~jespada@90.254.241.6) (Read error: Connection reset by peer) |
| 18:40:28 | <Cale> | It's hard to see how kicking Double out of Num is going to result in the same level of convenience even -- at the very least, you're going to have to choose new, slightly more awkward names for the operations -- we're basically out of single-character infix operators |
| 18:41:12 | → | jespada joins (~jespada@90.254.241.6) |
| 18:41:27 | <Cale> | and then you lose all the things which were written to work with an arbitrary instance of Num, many of which still make sense for Double |
| 18:42:22 | <hyperisco> | I sometimes hate our editing tools too |
| 18:42:51 | <Cale> | Our keyboards need more keys |
| 18:43:02 | × | ukari quits (~ukari@unaffiliated/ukari) (Remote host closed the connection) |
| 18:43:24 | → | wroathe joins (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) |
| 18:43:36 | <hyperisco> | one idea is to decouple the notion of overloading |
| 18:43:49 | → | ukari joins (~ukari@unaffiliated/ukari) |
| 18:44:29 | → | xerox_ joins (~xerox@unaffiliated/xerox) |
| 18:44:33 | <Cale> | Add a subclass of Num called Ring, with no additional operations, but more laws |
| 18:44:38 | <hyperisco> | basically what Num does now, at least the report version |
| 18:44:53 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:b46b:1e98:8653:4550) (Remote host closed the connection) |
| 18:44:59 | <Cale> | and then things which truly care that they have a proper Ring can demand it |
| 18:45:47 | <phadej> | Ring is wrong for Natural |
| 18:46:15 | <phadej> | even without thinking about Double :) |
| 18:46:33 | <hyperisco> | a trouble being that Num defines a lot of syntax, more than say a semiring would want |
| 18:47:02 | <hyperisco> | I guess this is the Idris lawful/lawless duality all over again |
| 18:47:30 | <hyperisco> | one is just syntax, the other adds semantics |
| 18:47:56 | <hyperisco> | maybe just a different mechanism is warranted, than type classes |
| 18:48:09 | <hyperisco> | C++ has macros, by preprocessor or template |
| 18:48:15 | <hyperisco> | it isn't a shining example but it is more truthful |
| 18:48:24 | × | juuandyy quits (~juuandyy@90.166.144.65) (Ping timeout: 260 seconds) |
| 18:49:01 | <phadej> | I also don't know how much Ocaml people hate the difference between + and .+ |
| 18:49:39 | <phadej> | whether the dotted operators are driving people crazy and into Haskell |
| 18:49:52 | <hyperisco> | I suspect the best way to solve this is with the editor / code viewer |
| 18:49:53 | <[exa]> | is there a squiggly variant of + in utf8 that could mark the approximate + on doubles etc ? |
| 18:50:14 | <[exa]> | because this is really just ascii problem |
| 18:50:14 | <hyperisco> | but that upends probably the most entrenched aspect of programming |
| 18:51:06 | <hyperisco> | I already use compose sequences to type things like → |
| 18:51:08 | <ski> | ⍭ |
| 18:51:10 | <ski> | maybe ? |
| 18:51:31 | <[exa]> | looks too precise |
| 18:52:26 | <ski> | ⨤ |
| 18:52:32 | <hyperisco> | if the same symbol was used in two ways then all I'd ask is there be some subtle indication of overloading, be it by colour or an extra mark (especially for the colourblind) |
| 18:52:42 | <hyperisco> | and the editor affords a way to unmask the overload |
| 18:53:01 | <[exa]> | ski: that's a strong candidate! |
| 18:53:18 | <hyperisco> | so then we don't have to play the unicode game either |
| 18:53:19 | × | shad0w_ quits (~shad0w_@160.202.36.27) (Remote host closed the connection) |
| 18:53:56 | <ski> | (there's ⌜⨦⌝, too) |
| 18:54:04 | <hyperisco> | in other words, there is a difference of syntax representation in a way somewhat similar to the compose sequences I use |
| 18:54:23 | <hyperisco> | I have multiple ways to type → say, but they present the same |
| 18:55:06 | <hyperisco> | and all I'd want to know is that 1) → represents more than one sequence and 2) which sequence it represents, but I only need to know (2) by explicitly asking |
| 18:55:23 | → | orion joins (~orion@c-76-19-238-5.hsd1.nh.comcast.net) |
| 18:55:23 | × | orion quits (~orion@c-76-19-238-5.hsd1.nh.comcast.net) (Changing host) |
| 18:55:23 | → | orion joins (~orion@unaffiliated/orion) |
| 18:55:31 | <hyperisco> | so then we can have + and .+ and whatever, and these present both as + |
| 18:55:56 | <hyperisco> | plus some signal it is overloaded |
| 18:56:51 | <hyperisco> | and all this without having to go off the deep end of projectional editing |
| 18:57:40 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Remote host closed the connection) |
| 18:58:10 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 18:58:17 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 19:00:27 | → | sfvm joins (~sfvm@37.228.215.148) |
| 19:00:41 | → | adam_wespiser joins (~adam_wesp@209.6.42.110) |
| 19:00:45 | × | abhixec quits (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 19:01:18 | → | abhixec joins (~abhixec@c-67-169-141-95.hsd1.ca.comcast.net) |
| 19:01:20 | <sm[m]> | I don't suppose there's any easy way to tell GHCI to use the extensions configured for a particular module ? |
| 19:01:48 | adam_wespiser | is now known as adamwespiser |
| 19:02:33 | <adamwespiser> | On load, you should be able to load a specific module, if I recall correctly, and in that module can be your extensions |
| 19:02:55 | <geekosaur> | but that doesn't set them for interactive use |
| 19:02:57 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Ping timeout: 260 seconds) |
| 19:03:08 | <sm[m]> | right |
| 19:03:10 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 258 seconds) |
| 19:03:12 | × | Dolly quits (585fd1fd@ti0203q160-5312.bb.online.no) (Remote host closed the connection) |
| 19:03:18 | <geekosaur> | nor does having multiple modules loaded and switching between them |
| 19:03:31 | <sm[m]> | I'm always being thwarted by mismatches between the module and ghci |
| 19:03:33 | × | Lycurgus quits (~niemand@98.4.96.130) (Quit: Exeunt) |
| 19:04:11 | <geekosaur> | (and this is often a feature, consider ExtendedDefaultRules which you probably don't want turned off by loading a module) |
| 19:04:16 | <sm[m]> | I guess I can make some shorter aliases to turn them on/off |
| 19:05:32 | <ddellacosta> | kind of a nix question, but can anyone tell me (or point me at docs for) how to override a dependency in a nix Haskell project with a local version of that package which I've compiled myself? Basically I just want to install my copy of the library just for that Haskell project |
| 19:06:35 | <sm[m]> | on another note, if anyone here has experience with sdl2, I have questions. Eg, why does destroyWindow not get rid of the window when running in GHCI. And, why does kill -TERM not kill a sdl app, it must be kill -KILL |
| 19:08:35 | → | bennofs joins (~quassel@dslb-178-000-064-245.178.000.pools.vodafone-ip.de) |
| 19:09:04 | → | thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) |
| 19:10:47 | × | shafox quits (~shafox@106.51.234.111) (Remote host closed the connection) |
| 19:12:34 | × | howdoi quits (uid224@gateway/web/irccloud.com/x-dtashatgyjqumlie) (Quit: Connection closed for inactivity) |
| 19:12:44 | × | bennofs_ quits (~quassel@dslb-188-106-250-199.188.106.pools.vodafone-ip.de) (Ping timeout: 272 seconds) |
| 19:13:04 | → | notzmv`` joins (~user@177.103.86.92) |
| 19:14:02 | × | thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 19:15:24 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 19:16:00 | → | josh joins (~josh@c-67-164-104-206.hsd1.ca.comcast.net) |
| 19:16:05 | × | notzmv` quits (~user@177.103.86.92) (Ping timeout: 240 seconds) |
| 19:17:41 | → | cosimone joins (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) |
| 19:18:44 | <koz_> | Is there a good way to generate a Text randomly which _is_ valid UTF-8, but _not_ valid Latin-1? |
| 19:19:24 | <geekosaur> | I don't think there's an invalid Latin-1 |
| 19:19:52 | <geekosaur> | unless you mean embedded control codes or similar, but that would also apply to UTF-8 |
| 19:19:55 | <koz_> | I think I'm being imprecise, sorry. I want to generate Text which contains at least one grapheme requiring a multi-byte encoding in UTF-8. |
| 19:20:05 | <koz_> | What's a good way to do this? |
| 19:20:16 | × | josh quits (~josh@c-67-164-104-206.hsd1.ca.comcast.net) (Ping timeout: 246 seconds) |
| 19:20:28 | <phadej> | arbitrary ++ [multibytechar] ++ arbitrary |
| 19:20:51 | <adamwespiser> | If you have a bytestring, I might use Data.Text.Encoding for that task |
| 19:20:53 | <geekosaur> | include at least one grapheme with a codepoint > 255 |
| 19:21:04 | <phadej> | geekosaur: >=128 |
| 19:21:16 | <phadej> | but >255 would work too |
| 19:21:24 | <geekosaur> | no, because 128..255 are valid Latin-1 |
| 19:21:36 | <phadej> | at least one grapheme requiring a multi-byte encoding in UTF-8. |
| 19:21:39 | <koz_> | phadej: Yeah, that's a good point. |
| 19:21:44 | <koz_> | Thanks! |
| 19:21:52 | <phadej> | codepoint 128 is encoded as two bytes |
| 19:22:04 | <phadej> | up to koz_ to refine the specification |
| 19:22:19 | <koz_> | phadej: The basic idea works well though. |
| 19:22:28 | <koz_> | Thanks for the suggestion. |
| 19:24:58 | hackage | stm-queue 0.1.2.0 - An implementation of a real-time concurrent queue https://hackage.haskell.org/package/stm-queue-0.1.2.0 (sgschlesinger) |
| 19:26:09 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 19:30:27 | hackage | Win32 2.10.0.0 - A binding to Windows Win32 API. https://hackage.haskell.org/package/Win32-2.10.0.0 (TamarChristina) |
| 19:30:50 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 19:31:00 | → | niHiggim joins (~manjaro-u@2606-a000-4545-ba00-0000-0000-0000-0006.inf6.spectrum.com) |
| 19:32:06 | → | knupfer1 joins (~Thunderbi@200116b82c2770004d12026ebf4c4ad8.dip.versatel-1u1.de) |
| 19:32:08 | × | knupfer quits (~Thunderbi@i59F7FF48.versanet.de) (Quit: knupfer) |
| 19:32:08 | knupfer1 | is now known as knupfer |
| 19:33:32 | × | ryansmccoy quits (~ryansmcco@193.37.254.27) (Ping timeout: 256 seconds) |
| 19:34:17 | → | ryansmccoy joins (~ryansmcco@156.96.151.132) |
| 19:36:03 | × | mirrorbird quits (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2) (Ping timeout: 272 seconds) |
| 19:38:17 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 260 seconds) |
| 19:42:31 | × | fendor quits (~fendor@77.119.128.171.wireless.dyn.drei.com) (Remote host closed the connection) |
| 19:49:19 | → | fendor joins (~fendor@77.119.128.171.wireless.dyn.drei.com) |
| 19:49:45 | × | solonarv quits (~solonarv@astrasbourg-653-1-186-165.w90-13.abo.wanadoo.fr) (Ping timeout: 260 seconds) |
| 19:51:25 | × | niHiggim quits (~manjaro-u@2606-a000-4545-ba00-0000-0000-0000-0006.inf6.spectrum.com) (Quit: Konversation terminated!) |
| 19:56:23 | → | ahmr88 joins (~ahmr88@cpc85006-haye22-2-0-cust131.17-4.cable.virginm.net) |
| 19:57:26 | × | ukari quits (~ukari@unaffiliated/ukari) (Remote host closed the connection) |
| 20:00:52 | × | auri__ quits (~auri_@fsf/memeber/auri-) (Ping timeout: 246 seconds) |
| 20:02:27 | → | auri_ joins (~auri_@fsf/memeber/auri-) |
| 20:03:02 | × | tsrt^ quits (tsrt@ip98-184-89-2.mc.at.cox.net) () |
| 20:03:45 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 20:03:58 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 20:04:17 | → | ntwhaaci^ joins (ntwhaaci@ip98-184-89-2.mc.at.cox.net) |
| 20:04:22 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 20:04:39 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 20:05:05 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 20:05:07 | × | wroathe quits (~wroathe@c-73-24-27-54.hsd1.mn.comcast.net) (Quit: leaving) |
| 20:06:48 | → | jobor_ joins (~jobor@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:07:02 | → | juuandyy joins (~juuandyy@90.166.144.65) |
| 20:08:44 | × | jobor_ quits (~jobor@83.24.161.211.ipv4.supernova.orange.pl) (Client Quit) |
| 20:09:09 | × | hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Remote host closed the connection) |
| 20:09:33 | → | johnyb joins (~johnyb@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:09:51 | → | hekkaidekapus joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 20:09:53 | × | geekosaur quits (ae68c070@cpe-174-104-192-112.neo.res.rr.com) (Remote host closed the connection) |
| 20:11:38 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 272 seconds) |
| 20:14:21 | → | g-belmonte joins (~g-belmont@2804:14c:8786:9312:3638:eaf5:dc36:146d) |
| 20:16:49 | <kindaro> | Is there a nice library for logging messages in IO to standard output/error? |
| 20:17:18 | <kindaro> | Like a fancy `putStrLn`, yes. |
| 20:17:41 | <merijn> | @hackage monad-logger |
| 20:17:41 | <lambdabot> | https://hackage.haskell.org/package/monad-logger |
| 20:17:47 | <Uniaika> | co-log exists too |
| 20:17:47 | <merijn> | And a billion others :p |
| 20:17:50 | <[exa]> | logging? |
| 20:17:58 | <[exa]> | ^^ actual package name |
| 20:18:07 | × | johnyb quits (~johnyb@83.24.161.211.ipv4.supernova.orange.pl) (Quit: Leaving...) |
| 20:18:22 | <kindaro> | No, these are not in IO, they have their own transformer or something. |
| 20:18:37 | <merijn> | What I like about monad-logger is that you can start out lazy just using LoggingT and then you can easily later replace it and implement your own stuff |
| 20:18:40 | <merijn> | eh |
| 20:18:48 | <merijn> | Well, then "hPutStrLn"? :p |
| 20:19:13 | <[exa]> | kindaro: https://hackage.haskell.org/package/logging even says "in IO" |
| 20:19:14 | <ddellacosta> | kindaro: logging that [exa] mentioned is just in IO I thought |
| 20:19:22 | <ddellacosta> | lol jinx |
| 20:19:30 | <[exa]> | :] |
| 20:19:30 | <kindaro> | I see `logging` has `log :: Text -> IO ()` — that I like. |
| 20:20:46 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 20:22:40 | → | johnyb joins (5318a1d3@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:24:29 | × | ggole quits (~ggole@2001:8003:8119:7200:a81f:ad25:a0f4:9303) (Quit: Leaving) |
| 20:25:18 | <kindaro> | By the way, I see `logging` is using the idiom of `logLevel = unsafePerformIO $ newIORef LevelDebug` for initializing an implicit global state. I know that `random` recently removed a similar feature. Has there been research that shows definitely that such use of `unsafePerformIO` is either safe or unsafe? |
| 20:25:27 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Ping timeout: 272 seconds) |
| 20:25:48 | × | borne quits (~fritjof@200116b86490460022497ba62715fb72.dip.versatel-1u1.de) (Ping timeout: 260 seconds) |
| 20:26:59 | <kindaro> | Particularly, see this explanation: https://github.com/haskell/random/issues/57#issuecomment-649473745 |
| 20:27:20 | <kindaro> | I am divided on this technique since then — should I like or dislike it? |
| 20:27:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 20:28:12 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 20:29:12 | <[exa]> | kindaro: unsafePerformIO is often quite practical, like for tracing |
| 20:29:45 | → | borne joins (~fritjof@200116b86490460022497ba62715fb72.dip.versatel-1u1.de) |
| 20:29:47 | <Cale> | I dislike it just because it means that only one usage is possible. It's fine to use mutable stuff, but it would make more sense to have a little bundle of mutable state containing a handle for where the log message was going, together with the current log level perhaps |
| 20:30:06 | <kindaro> | Not sure I follow. |
| 20:30:21 | <Cale> | I guess the assumption here is that the log is only going to stderr |
| 20:30:26 | × | polyphem quits (~p0lyph3m@2a02:810d:640:776c:76d7:55f6:f85b:c889) (Read error: Connection reset by peer) |
| 20:30:37 | <Cale> | But say multiple libraries decide to use this log library |
| 20:30:53 | <Cale> | Then they might interfere with each other when it comes to setting their log level |
| 20:30:56 | johnyb | is now known as JonathanB |
| 20:31:10 | JonathanB | is now known as JonatanB |
| 20:31:18 | <Cale> | One library can't have a different log level than the other, even if it might appear that way, because some initialisation function takes a log level |
| 20:31:22 | <Cale> | (and sets it) |
| 20:31:48 | <Cale> | Just because they accidentally both used logging |
| 20:32:08 | <c_wraith> | I'd probably argue libraries should never set the log level anyway, but that's beside the point a bit. With the point being that there are ways to design it that don't involve unsafePerformIO |
| 20:32:58 | → | polyphem joins (~p0lyph3m@2a02:810d:640:776c:76d7:55f6:f85b:c889) |
| 20:33:12 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 20:33:21 | <Cale> | Well, they might set the log level according to what the user of the library requests |
| 20:33:41 | <Cale> | But yeah, I suppose if you're using 'logging', you don't really do that |
| 20:34:06 | <Cale> | because it doesn't make sense, as you can't really have a distinct logging level from any other library which is using it |
| 20:34:09 | JonatanB | is now known as jonatanb |
| 20:36:42 | <jonatanb> | \nick jobo |
| 20:37:19 | × | jonatanb quits (5318a1d3@83.24.161.211.ipv4.supernova.orange.pl) (Remote host closed the connection) |
| 20:37:33 | → | jonatanb` joins (~user@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:38:13 | × | sense quits (uid464711@gateway/web/irccloud.com/x-rdruibjtxeskwext) (Quit: Connection closed for inactivity) |
| 20:38:23 | × | jonatanb` quits (~user@83.24.161.211.ipv4.supernova.orange.pl) (Client Quit) |
| 20:38:57 | → | jonatanb joins (~user@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:41:20 | → | jonatanb27 joins (5318a1d3@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:41:34 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 20:42:20 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 20:42:32 | × | jonatanb27 quits (5318a1d3@83.24.161.211.ipv4.supernova.orange.pl) (Remote host closed the connection) |
| 20:43:05 | → | bahamas joins (~lucian@188.24.181.166) |
| 20:43:05 | × | bahamas quits (~lucian@188.24.181.166) (Changing host) |
| 20:43:05 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 20:44:58 | × | coot quits (~coot@37.30.49.42.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 20:47:37 | → | mirk0_ joins (~mirko@unaffiliated/-mirko-/x-2946915) |
| 20:47:38 | × | lep-delete quits (~lep@94.31.82.44) (Read error: Connection reset by peer) |
| 20:47:55 | → | lep-delete joins (~lep@94.31.82.44) |
| 20:48:05 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 260 seconds) |
| 20:48:46 | × | jonatanb quits (~user@83.24.161.211.ipv4.supernova.orange.pl) (Quit: ERC (IRC client for Emacs 26.3)) |
| 20:49:08 | × | tabemann quits (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Ping timeout: 260 seconds) |
| 20:49:21 | → | jonatanb joins (~jonatanb@83.24.161.211.ipv4.supernova.orange.pl) |
| 20:49:22 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 20:51:47 | × | danso quits (~dan@107-190-41-58.cpe.teksavvy.com) (Read error: Connection reset by peer) |
| 20:51:47 | × | dansho quits (~dansho@ip68-108-167-185.lv.lv.cox.net) (Ping timeout: 240 seconds) |
| 20:51:58 | hackage | Rasterific 0.7.5.3 - A pure haskell drawing engine. https://hackage.haskell.org/package/Rasterific-0.7.5.3 (VincentBerthoux) |
| 20:52:56 | → | danso joins (~dan@107-190-41-58.cpe.teksavvy.com) |
| 20:52:59 | × | aidecoe quits (~aidecoe@unaffiliated/aidecoe) (Ping timeout: 240 seconds) |
| 20:53:59 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Read error: Connection reset by peer) |
| 20:54:49 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 20:59:05 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 20:59:12 | → | aidecoe joins (~aidecoe@unaffiliated/aidecoe) |
| 20:59:45 | × | juuandyy quits (~juuandyy@90.166.144.65) (Ping timeout: 260 seconds) |
| 21:00:02 | × | laen_ quits (~laen_@s91904426.blix.com) () |
| 21:00:13 | × | ryansmccoy quits (~ryansmcco@156.96.151.132) (Ping timeout: 260 seconds) |
| 21:00:37 | → | ryansmccoy joins (~ryansmcco@156.96.151.132) |
| 21:01:03 | × | knupfer quits (~Thunderbi@200116b82c2770004d12026ebf4c4ad8.dip.versatel-1u1.de) (Quit: knupfer) |
| 21:01:25 | → | knupfer joins (~Thunderbi@200116b82c27700031ead27836249122.dip.versatel-1u1.de) |
| 21:01:26 | × | knupfer quits (~Thunderbi@200116b82c27700031ead27836249122.dip.versatel-1u1.de) (Client Quit) |
| 21:01:42 | <lechner> | sm[m]: not sure what you are doing with sdl2, but maybe this helps https://discourse.libsdl.org/t/mac-os-x-avoid-the-sdl-to-catch-sigterm-and-sigint-signals/27357 |
| 21:01:45 | → | knupfer joins (~Thunderbi@200116b82c277000ad37883ab022eaf9.dip.versatel-1u1.de) |
| 21:01:56 | → | knupfer1 joins (~Thunderbi@200116b82c277000b09f08f0bf52a637.dip.versatel-1u1.de) |
| 21:01:56 | × | knupfer1 quits (~Thunderbi@200116b82c277000b09f08f0bf52a637.dip.versatel-1u1.de) (Read error: Connection reset by peer) |
| 21:02:03 | × | knupfer quits (~Thunderbi@200116b82c277000ad37883ab022eaf9.dip.versatel-1u1.de) (Read error: Connection reset by peer) |
| 21:02:11 | → | knupfer joins (~Thunderbi@200116b82c277000646991969a0bc875.dip.versatel-1u1.de) |
| 21:02:15 | × | knupfer quits (~Thunderbi@200116b82c277000646991969a0bc875.dip.versatel-1u1.de) (Client Quit) |
| 21:02:34 | × | kindaro quits (5f6e6241@h95-110-98-65.dyn.bashtel.ru) (Ping timeout: 245 seconds) |
| 21:02:37 | × | jonatanb quits (~jonatanb@83.24.161.211.ipv4.supernova.orange.pl) (Quit: Leaving...) |
| 21:02:45 | → | jonatanb joins (~jonatanb@83.24.161.211.ipv4.supernova.orange.pl) |
| 21:04:18 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 258 seconds) |
| 21:04:39 | <orion> | Hi. Does anyone know how to make this typecheck?: https://gist.github.com/centromere/b1f795418d00dff28e2cfcaefd727751 |
| 21:05:00 | <orion> | (The package is acid-state) |
| 21:05:34 | <orion> | I realize that the "event" expressed by the type signature is general, whereas I am trying to use it with a more specific type, leading to the error. |
| 21:05:45 | <orion> | I am not sure how to approach the issue though. |
| 21:05:53 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:10:35 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 21:11:43 | → | Volt_ joins (~Volt_@c-73-145-164-70.hsd1.mi.comcast.net) |
| 21:14:14 | × | oxide quits (~lambda@unaffiliated/mclaren) (Ping timeout: 260 seconds) |
| 21:15:11 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 21:16:14 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.) |
| 21:16:27 | <tomsmeding> | orion: EventState is a type family; what does 'EventState AppState' resolve to? |
| 21:16:57 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 258 seconds) |
| 21:16:58 | hackage | termbox 0.3.0 - termbox bindings https://hackage.haskell.org/package/termbox-0.3.0 (mitchellwrosen) |
| 21:18:13 | × | AlterEgo- quits (~ladew@124-198-158-163.dynamic.caiway.nl) (Read error: Connection reset by peer) |
| 21:19:37 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 246 seconds) |
| 21:20:55 | → | romtam joins (~romtam@s91904426.blix.com) |
| 21:21:53 | × | pingiun quits (~pingiun@j63019.upc-j.chello.nl) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 21:23:39 | × | jonatanb quits (~jonatanb@83.24.161.211.ipv4.supernova.orange.pl) (Quit: Leaving...) |
| 21:23:41 | <sm[m]> | lechner: that looks highly relevant, thanks! |
| 21:24:59 | <sm[m]> | I'm wanting to kill & restart my sdl app on rebuild with entr, which sends SIGTERM |
| 21:25:37 | × | ahmr88 quits (~ahmr88@cpc85006-haye22-2-0-cust131.17-4.cable.virginm.net) (Remote host closed the connection) |
| 21:26:43 | <sm[m]> | though if I could destroy the window from ghci, I would rather run it with ghcid |
| 21:38:04 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:38:05 | → | opticblast joins (~june@075-128-229-153.res.spectrum.com) |
| 21:41:10 | → | thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) |
| 21:41:10 | × | fendor quits (~fendor@77.119.128.171.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 21:52:56 | × | lortabac quits (~lortabac@51.158.65.124) (Ping timeout: 256 seconds) |
| 21:53:17 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 21:53:53 | × | hyperisco quits (~hyperisco@d192-186-117-226.static.comm.cgocable.net) (Ping timeout: 260 seconds) |
| 21:54:34 | notzmv`` | is now known as notzvm |
| 21:54:36 | notzvm | is now known as notzmv |
| 21:54:45 | × | notzmv quits (~user@177.103.86.92) (Changing host) |
| 21:54:45 | → | notzmv joins (~user@unaffiliated/zmv) |
| 21:55:30 | → | lortabac joins (~lortabac@51.158.65.124) |
| 21:55:40 | → | isovector1 joins (~isovector@node-1w7jr9squrfoy3fci95ksrhpu.ipv6.telus.net) |
| 21:56:11 | <hyiltiz> | What's the design choice of not sugaring `$ do` into something else (like $$ or whatev) in HSpec? I think it is because both $ and do is basic stuff and simply composing them as a basic HSpec operation is also nice, besides it is not too long to type |
| 21:56:34 | <hyiltiz> | Also, sometimes the do is not needed |
| 21:57:07 | <hyiltiz> | So sugaring it to $$ could lead to confusion |
| 21:57:23 | <edwardk> | hyiltiz: ? do is builtin syntax |
| 21:57:38 | <edwardk> | you can use BlockArguments to drop the $ though |
| 21:58:02 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 256 seconds) |
| 21:58:23 | <hyiltiz> | I c it is builtin syntax. I am just wondering why not wrap the EDSL into something less verbose |
| 21:58:36 | <ski> | (`$' is a library operation, though) |
| 21:59:06 | → | rprije joins (~rprije@27.143.220.203.dial.dynamic.acc01-myal-dub.comindico.com.au) |
| 21:59:11 | <hyiltiz> | oh wait that $ is overloaded? I thought it was the one from haskell? |
| 21:59:20 | × | adamwespiser quits (~adam_wesp@209.6.42.110) (Remote host closed the connection) |
| 22:00:07 | <edwardk> | not sure how you get lighter weight than do, it acts like parentheses you don't have to close |
| 22:00:27 | <edwardk> | given HSpec doesn't hide prelude's $, it is just the one from Prelude |
| 22:01:07 | <edwardk> | anyways do takes exactly as many characters as ()'s would and self closes when you outdent |
| 22:01:37 | <edwardk> | but using BlockArguments does clean up the 'noise' in an HSpec file |
| 22:02:26 | <edwardk> | BlockArguments https://www.irccloud.com/pastebin/R8v4pxNs/BlockSpec.hs |
| 22:02:47 | <edwardk> | you can swap each of those do's for a $ except the one on the line with describe |
| 22:03:23 | <edwardk> | BlockArguments lets you kill the $ before the lambda for property there as well |
| 22:03:36 | <edwardk> | > 2 * do 3 + 4 |
| 22:03:38 | <lambdabot> | 14 |
| 22:04:04 | <opticblast> | > :t do () |
| 22:04:07 | <lambdabot> | <hint>:1:1: error: <hint>:1:1: error: parse error on input ‘:’ |
| 22:04:08 | <ski> | hyiltiz : no, it's the usual `$' in the library |
| 22:04:23 | <opticblast> | @type do () |
| 22:04:25 | <lambdabot> | () |
| 22:04:29 | <opticblast> | well, that's confusing |
| 22:04:35 | <opticblast> | I thought it would be something like Identity () |
| 22:05:07 | <edwardk> | do doesn't change the types, it just desugars into >>= uses when there is ; -- and maybe does some applicative stuff if applicative do is on |
| 22:05:24 | <edwardk> | when there is only one expression there you want it passed through |
| 22:05:25 | → | adamwespiser joins (~adam_wesp@209.6.42.110) |
| 22:05:33 | <ski> | a `do'-expression has the same type as its last command (which in this case was `()') |
| 22:05:40 | <edwardk> | otherwise in your model do () and do (pure ()) -- would be ambiguous what to do |
| 22:05:53 | <edwardk> | or 'do x' where x happens to be pure y |
| 22:06:00 | <edwardk> | so it _can't_ do the thing you want opticblast |
| 22:06:12 | <opticblast> | ah, makes sense |
| 22:06:41 | <edwardk> | now, back in the day it used to be that do would guide inference to figure out that the type there was the application of some m to some a, but we got them to stop doing that a looong time ago |
| 22:07:14 | × | drdo quits (~drdo@overlord0.drdo.eu) (Remote host closed the connection) |
| 22:08:21 | → | drdo joins (~drdo@overlord0.drdo.eu) |
| 22:09:05 | → | obihann joins (~jhann@156.34.160.69) |
| 22:10:13 | × | adamwespiser quits (~adam_wesp@209.6.42.110) (Ping timeout: 260 seconds) |
| 22:12:08 | <hyiltiz> | edwardk: thx! BlockArguments seems to really clean up the verbose notation |
| 22:12:23 | <hyiltiz> | and I am sure it works not just work HSpec as well |
| 22:12:33 | <hyiltiz> | Reminds me of Ruby's blocks |
| 22:13:14 | × | sagax quits (~sagax_nb@213.138.71.146) (Ping timeout: 272 seconds) |
| 22:13:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 22:14:45 | <edwardk> | i use it more and more these days mostly because when some library messily needs to take a argument that will be very long right before some other empty list argument or something i can break things up by lines and then just use the do to self delimit _that_ argument, without having to figure out how to put the closing paren, or get all lispy with closing parens dangling on the far right of my screen |
| 22:15:27 | hackage | termbox-banana 0.3.0 - reactive-banana + termbox https://hackage.haskell.org/package/termbox-banana-0.3.0 (mitchellwrosen) |
| 22:15:44 | <yushyin> | 6 |
| 22:15:50 | <yushyin> | ups, sorry |
| 22:17:06 | → | tabemann joins (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 22:17:55 | <edwardk> | it amazes me that nobody has written an ncurses variant that knows how many lines worth of text it has scrolled in and gives you control over just that portion of the screen space, so it doesn't have to flip to the alt screen and works well for repls. |
| 22:18:04 | GyroW_ | is now known as GyroW |
| 22:18:05 | × | GyroW quits (~GyroW@ptr-48ujrfb8c7gfd2lu92q.18120a2.ip6.access.telenet.be) (Changing host) |
| 22:18:05 | → | GyroW joins (~GyroW@unaffiliated/gyrow) |
| 22:18:31 | <edwardk> | everything that works like this is some bespoke readline like monstrosity |
| 22:19:52 | × | thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 22:21:40 | → | mariatsji joins (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) |
| 22:23:12 | → | DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) |
| 22:27:38 | × | aenesidemus quits (~aenesidem@c-73-53-247-25.hsd1.fl.comcast.net) (Quit: Leaving) |
| 22:29:56 | <dolio> | I think block arguments are a good idea (mostly), but characterising two extra characters as 'verbose' seems a little silly. |
| 22:30:38 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 22:33:08 | × | isovector1 quits (~isovector@node-1w7jr9squrfoy3fci95ksrhpu.ipv6.telus.net) (Remote host closed the connection) |
| 22:33:16 | → | isovector1 joins (~isovector@d207-81-8-13.bchsia.telus.net) |
| 22:33:23 | <edwardk> | i mean i grumble about the extra : in :: all the time |
| 22:33:38 | → | ph88 joins (~ph88@2a02:8109:9e40:2704:b503:e755:2c19:955c) |
| 22:33:40 | <edwardk> | so who am i to begrudge someone a complaint about twice as many characters |
| 22:34:46 | <yushyin> | unfortunate hysterical reasons with the : vs. :: matter |
| 22:35:21 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 265 seconds) |
| 22:35:44 | <Rembane> | We need a Haskell dialect where the : and :: are swapped. |
| 22:35:55 | <koz_> | Rembane: So, Idris? :P |
| 22:36:48 | <edwardk> | then the laziness gets ya |
| 22:39:57 | → | adamwespiser joins (~adam_wesp@209.6.42.110) |
| 22:40:06 | <Rembane> | koz_: Yeah, why not? :) |
| 22:40:21 | <dolio> | I don't think the extra typing hurts as much as being different from the settled notation. |
| 22:40:29 | <yushyin> | Rembane: https://github.com/ghc-proposals/ghc-proposals/pull/118 |
| 22:41:07 | ski | . o O ( ⌜∷⌝ ) |
| 22:41:20 | <Axman6> | Rembane: DAML? |
| 22:42:53 | × | aidecoe quits (~aidecoe@unaffiliated/aidecoe) (Ping timeout: 272 seconds) |
| 22:43:27 | × | mariatsji quits (~mariatsji@2a01:79d:53aa:c66c:342b:5324:f59b:5b0e) (Ping timeout: 260 seconds) |
| 22:43:48 | → | pingiun joins (~pingiun@j63019.upc-j.chello.nl) |
| 22:43:50 | <Rembane> | yushyin: Wow. Nice. |
| 22:44:08 | <Rembane> | Axman6: Dots Are More LOL? |
| 22:46:11 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 22:47:12 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 22:47:43 | <koz_> | Rembane: Dots Are More Leet. |
| 22:47:48 | × | isovector1 quits (~isovector@d207-81-8-13.bchsia.telus.net) (Ping timeout: 258 seconds) |
| 22:47:56 | <dolio> | Regardless, it's never going to be worth changing in its own right. |
| 22:48:46 | <Rembane> | koz_: Of course! I'm way too tired to get that on the first try. |
| 22:53:01 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 22:53:09 | × | DataComputist quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Ping timeout: 260 seconds) |
| 22:53:50 | → | DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) |
| 22:54:32 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Ping timeout: 260 seconds) |
| 22:54:39 | <Axman6> | @google DAML |
| 22:54:40 | <lambdabot> | No Result Found. |
| 22:54:45 | <Axman6> | uwot |
| 22:55:06 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 22:55:10 | <MarcelineVQ> | don't all mutts leak? |
| 22:55:55 | <Axman6> | https://daml.com - a dialect of Haskell for smart contracts, its compiler GHC with some desugaring on the front end (including : <-> ::, ples a lot of other nice extensions which make using the language day to day really nice) |
| 22:56:07 | → | NaN joins (43aa4b1c@c-67-170-75-28.hsd1.wa.comcast.net) |
| 22:56:31 | NaN | is now known as Guest39453 |
| 22:56:52 | <koz_> | MarcelineVQ: Don't All Marsupials Lie? |
| 22:57:17 | <MarcelineVQ> | Driven Antelopes Must Leap |
| 22:57:30 | <Guest39453> | uh? |
| 22:57:42 | <Axman6> | this is the secret code, you are now authenticated |
| 22:58:18 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 22:58:48 | → | gmt joins (~gmt@pool-71-105-108-44.nycmny.fios.verizon.net) |
| 22:59:11 | <Guest39453> | @help |
| 22:59:12 | <lambdabot> | help <command>. Ask for help for <command>. Try 'list' for all commands |
| 22:59:26 | <Axman6> | plus* |
| 22:59:29 | ski | looks at Guest39453 |
| 23:00:00 | → | kenran joins (~maier@b2b-37-24-119-190.unitymedia.biz) |
| 23:00:01 | <Guest39453> | just seeing if lambdabot is real |
| 23:00:49 | <koz_> | Lambdabot is indeed a figment of your imagination. |
| 23:00:53 | <Axman6> | are bits real? |
| 23:00:56 | <MarcelineVQ> | how can lambdabot be real if our toes aren't real |
| 23:01:11 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-jznybxwchugeubau) |
| 23:01:29 | → | cosimone_ joins (~cosimone@5.170.241.4) |
| 23:03:06 | <Axman6> | deep |
| 23:03:17 | <Axman6> | but not like learning, like the ocean |
| 23:04:28 | × | cosimone quits (~cosimone@2001:b07:ae5:db26:b248:7aff:feea:34b6) (Ping timeout: 260 seconds) |
| 23:05:17 | × | kenran quits (~maier@b2b-37-24-119-190.unitymedia.biz) (Ping timeout: 260 seconds) |
| 23:06:15 | <orion> | tomsmeding: Is a type familiy the same as a type synonym?: https://github.com/acid-state/acid-state/blob/bf1fa2466e749f91d2e3152ced15331f062e8d10/src/Data/Acid/Common.hs#L54 |
| 23:06:58 | <Axman6> | no |
| 23:07:16 | cosimone_ | is now known as cosimone |
| 23:07:42 | × | MorrowM quits (~max@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 272 seconds) |
| 23:09:30 | → | bahamas joins (~lucian@188.24.181.166) |
| 23:09:30 | × | bahamas quits (~lucian@188.24.181.166) (Changing host) |
| 23:09:30 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 23:10:52 | × | cyphase quits (~cyphase@unaffiliated/cyphase) (Ping timeout: 272 seconds) |
| 23:12:56 | → | machinedgod joins (~machinedg@d67-193-126-196.home3.cgocable.net) |
| 23:13:03 | → | mitchellsalad joins (uid40617@gateway/web/irccloud.com/x-ahcdpvrnkonimwkz) |
| 23:14:01 | → | aidecoe joins (~aidecoe@unaffiliated/aidecoe) |
| 23:14:15 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 258 seconds) |
| 23:17:50 | <orion> | Oh, tomsmeding was talking about MethodState. |
| 23:19:01 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 23:19:35 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@104.200.129.62) (Quit: Leaving) |
| 23:20:29 | × | Guest39453 quits (43aa4b1c@c-67-170-75-28.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 23:20:58 | → | cyphase joins (~cyphase@unaffiliated/cyphase) |
| 23:28:29 | × | ph88 quits (~ph88@2a02:8109:9e40:2704:b503:e755:2c19:955c) (Ping timeout: 272 seconds) |
| 23:30:14 | <orion> | tomsmeding: type instance MethodState UpdateNow = AppState |
| 23:34:51 | → | sepi joins (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) |
| 23:36:12 | × | pera quits (~pera@unaffiliated/pera) (Ping timeout: 272 seconds) |
| 23:42:14 | × | sepi quits (49dc4892@c-73-220-72-146.hsd1.ca.comcast.net) (Remote host closed the connection) |
| 23:45:21 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection) |
| 23:46:45 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 23:49:15 | × | opticblast quits (~june@075-128-229-153.res.spectrum.com) (Quit: leaving) |
| 23:49:21 | → | jedws joins (~jedws@121.209.139.222) |
| 23:49:37 | <orion> | tomsmeding: I got it! All I had to do was change the type signature to this: update :: (UpdateEvent event, MethodState event ~ AppState, MonadIO m, MonadTime m) |
| 23:49:39 | → | bahamas joins (~lucian@unaffiliated/bahamas) |
| 23:50:07 | <orion> | Thank you for your assistance. |
| 23:52:43 | → | MorrowM joins (~max@bzq-110-168-31-106.red.bezeqint.net) |
| 23:53:10 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 23:53:20 | × | falafel quits (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) (Remote host closed the connection) |
| 23:53:57 | → | falafel joins (~falafel@2605:e000:1527:d491:f090:20fe:cddf:2a1a) |
| 23:54:34 | × | bahamas quits (~lucian@unaffiliated/bahamas) (Ping timeout: 272 seconds) |
| 23:57:51 | → | cipherchess joins (~oned4@151.51.54.223) |
| 23:58:07 | → | nbloomf joins (~nbloomf@2600:1700:83e0:1f40:10e:bca5:1dcc:68c6) |
| 23:58:14 | → | polyrain joins (~polyrain@2001:8003:e501:6901:3846:7fa4:c749:eb08) |
All times are in UTC on 2020-09-20.