| 2022-07-12 00:00:33 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 00:02:48 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2022-07-12 00:04:03 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 260 seconds) |
| 2022-07-12 00:05:23 +0200 | harry | (~harry@c-73-93-249-239.hsd1.ca.comcast.net) (Quit: harry) |
| 2022-07-12 00:05:36 +0200 | <ski> | seriously : `localMaxima' isn't defined for lists of length one and two (matching against the pattern `x:y:z:xs' happens before it would get a chance to get to the `length lst < 3' guard) |
| 2022-07-12 00:07:30 +0200 | <ski> | `snd' isn't defined on triples (only pairs) |
| 2022-07-12 00:07:51 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 2022-07-12 00:08:29 +0200 | <ski> | perhaps you meant `func (y:z:xs)' ? (`func y:z:xs' means `(func y):(z:xs)') |
| 2022-07-12 00:08:46 +0200 | <seriously> | ok ski thanks for the headsup... still working through how to .... |
| 2022-07-12 00:08:59 +0200 | <seriously> | thanks (: that was it |
| 2022-07-12 00:09:42 +0200 | Guest56 | (~Guest56@2a01:4b00:d001:8c00:7df5:f9db:fcc0:60b7) |
| 2022-07-12 00:10:05 +0200 | <ski> | (similarly, i'm suspecting that instead of `filter (\(...) -> ...) (...):(...)' you meant `func (\(...) -> ...) ((...):...)' .. otherwise you're only passing the `(x,y,z)' part, not the part with `func', as an argument to `filter') |
| 2022-07-12 00:10:44 +0200 | Guest56 | (~Guest56@2a01:4b00:d001:8c00:7df5:f9db:fcc0:60b7) (Client Quit) |
| 2022-07-12 00:11:21 +0200 | <monochrom> | Wait a second, why is an Elm kids' summer camp advertising in haskell-cafe? :) |
| 2022-07-12 00:11:39 +0200 | <ski> | btw, instead of using `y:z:xs', you could say e.g. `rest', if you change the pattern `lst@(x:y:z:xs)' into `lst@(x:rest@(y:z:xs))' |
| 2022-07-12 00:12:05 +0200 | <monochrom> | And the title is as if the 8-14yos found Haskell too easy :) |
| 2022-07-12 00:12:15 +0200 | <ski> | there are Elm kids' summer camps ? |
| 2022-07-12 00:12:47 +0200 | <geekosaur> | https://mail.haskell.org/pipermail/haskell-cafe/2022-July/135388.html |
| 2022-07-12 00:13:05 +0200 | <geekosaur> | say what now? |
| 2022-07-12 00:15:31 +0200 | <monochrom> | Heh pipermail is not going to make it easy to view an HTML email |
| 2022-07-12 00:15:35 +0200 | <hpc> | no plaintext fallback :( |
| 2022-07-12 00:15:52 +0200 | <hpc> | but they use a cid attachment for the image instead of embedding |
| 2022-07-12 00:16:03 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 00:16:12 +0200 | <monochrom> | But the title is "mastered Haskell and need a new challenge???", and the text begins with "Learn Elm! Free introduction for ages 8-14 with these coupons" |
| 2022-07-12 00:16:37 +0200 | ephemient | (uid407513@id-407513.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-07-12 00:17:00 +0200 | <sclv> | lmao. if you mastered haskell and need a new challenge and you are 8 years old i suggest you tackle the langlands program |
| 2022-07-12 00:17:03 +0200 | <Bulby[m]> | wtf |
| 2022-07-12 00:17:17 +0200 | <monochrom> | sclv: Well said haha |
| 2022-07-12 00:18:15 +0200 | <monochrom> | I do appreciate that of all summer programming camps, at least someone is trying to do FP in one. |
| 2022-07-12 00:19:08 +0200 | <monochrom> | Right? Everyone is crazy with "more kids need to see more python". It is beginning to feel like BASIC-esque. |
| 2022-07-12 00:19:58 +0200 | <geekosaur> | oh, it's been there for years |
| 2022-07-12 00:20:09 +0200 | <monochrom> | Those who have learned from history are doomed to helplessly watch other people repeat it. >:) |
| 2022-07-12 00:20:23 +0200 | christiansen | (~christian@83-95-137-75-dynamic.dk.customer.tdc.net) (Ping timeout: 272 seconds) |
| 2022-07-12 00:20:26 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 00:21:40 +0200 | <seriously> | ski since finding my errors was literally target practice for you: also unzip only works on a list of tuples. I needed unzip3 |
| 2022-07-12 00:21:51 +0200 | <dolio> | How much of a challenge is Elm for someone who's already mastered Haskell? |
| 2022-07-12 00:22:03 +0200 | <geekosaur> | I've been surprised someone hasn't recycled dijkstra's basic quote, tbh |
| 2022-07-12 00:23:42 +0200 | <monochrom> | Elm lacks a lot of user definability regarding type classes and instances, right? That would be a challenge. >:) |
| 2022-07-12 00:24:13 +0200 | <sclv> | i mean python was literally designed as a better teaching language than basic iirc |
| 2022-07-12 00:24:18 +0200 | <monochrom> | In the same way I would find BASIC a challenge today. What do you mean I may only have numbers and strings. |
| 2022-07-12 00:25:10 +0200 | <sclv> | the worst and weirdest thing basic taught me is that "a computer program has to have a sequence of numbers in front of the lines: 10, 20, 30, 40" and they never f'ing explained why in any of the intro material |
| 2022-07-12 00:25:29 +0200 | <meejah> | in case you want to use GOTO of course! |
| 2022-07-12 00:25:33 +0200 | <sclv> | that and the all caps etc - a lot of just "syntactic discipline for its own sake" |
| 2022-07-12 00:26:11 +0200 | meejah | found QuickBASIC flopies recently.. |
| 2022-07-12 00:26:12 +0200 | <geekosaur> | …leading me to write a preprocessor that did the line numbers for me |
| 2022-07-12 00:26:21 +0200 | <geekosaur> | and write in lowercase |
| 2022-07-12 00:27:03 +0200 | <dolio> | sclv: You need that to insert lines in the middle of the program later. |
| 2022-07-12 00:27:09 +0200 | <sclv> | right i mean by the time i was doing it, clearly writing such processors was straightforward and did not add much in the way of resource consumption |
| 2022-07-12 00:27:14 +0200 | <dolio> | Anticipated AOP. Way ahead of their time. |
| 2022-07-12 00:27:28 +0200 | <monochrom> | haha |
| 2022-07-12 00:27:50 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 00:28:06 +0200 | <sclv> | so like "we'll teach you this insane way to do things that involves a lot of work that could be done by a computer if only we had one OH WAIT YOU ARE USING ONE ALREADY:!?" was not a welcoming introduction to like "computer programs make your life better and simpler" |
| 2022-07-12 00:29:21 +0200 | <monochrom> | OK so one aspect is that back then we didn't have an editor, unless you could call something even more primitive than ed an editor. |
| 2022-07-12 00:30:00 +0200 | <monochrom> | Imagine a world in which only REPLs exist. |
| 2022-07-12 00:30:01 +0200 | <sclv> | by the time i was doing it we absolutely had editors more sophisticated than ed. |
| 2022-07-12 00:30:14 +0200 | <dolio> | That aspect is still lost on a lot of people today, though. |
| 2022-07-12 00:30:32 +0200 | <sclv> | like computers were already being used as full fledged typesetting word processors |
| 2022-07-12 00:30:33 +0200 | <monochrom> | haha |
| 2022-07-12 00:30:40 +0200 | <hpc> | imagine a world in which catting a file cost ink instead of bytes |
| 2022-07-12 00:30:47 +0200 | <hpc> | and that's how you get ed |
| 2022-07-12 00:31:34 +0200 | <hpc> | there's a reason your terminal device is called a tty, and it's not that unix likes to give things silly names :D |
| 2022-07-12 00:31:34 +0200 | <EvanR> | so wait, in old basic, you had to put numbers and you also had line numbers? |
| 2022-07-12 00:31:43 +0200 | <sclv> | speaking of AOP and GOTO i recall AOP at one point being described as "the ultimate COMEFROM" |
| 2022-07-12 00:31:53 +0200 | <EvanR> | 1 10 print hello world |
| 2022-07-12 00:31:55 +0200 | <EvanR> | 2 20 goto 10 |
| 2022-07-12 00:32:10 +0200 | <monochrom> | Nah you just need the 10 and 20. |
| 2022-07-12 00:32:16 +0200 | <hpc> | EvanR: yep, convention was 10x line number so you could insert 9 more lines before redoing your goto |
| 2022-07-12 00:32:42 +0200 | <EvanR> | i mean the editors didn't show the actual line numbers because you synthesized your own? |
| 2022-07-12 00:32:48 +0200 | <monochrom> | Yes. |
| 2022-07-12 00:32:54 +0200 | <EvanR> | mind blown |
| 2022-07-12 00:33:01 +0200 | <seriously> | i did it guys. I dont want to start naming all my supporters in fear that i may forget someone; so thank you everyone |
| 2022-07-12 00:33:49 +0200 | <EvanR> | hpc, obviously you need to graduate to 100 200 etc |
| 2022-07-12 00:33:55 +0200 | <monochrom> | You can use the fibonacci sequence if you want. |
| 2022-07-12 00:34:07 +0200 | <hpc> | 1 print "hello" |
| 2022-07-12 00:34:08 +0200 | <hpc> | 1 goto 1 |
| 2022-07-12 00:34:23 +0200 | <hpc> | 2 hang on a minute... |
| 2022-07-12 00:34:24 +0200 | <EvanR> | one day they will invent rationals |
| 2022-07-12 00:34:25 +0200 | <monochrom> | OK except for the duplicate "1, 1" beginning :) |
| 2022-07-12 00:34:37 +0200 | <sclv> | i forget what would happen if the sequence wasn't monotone increasing |
| 2022-07-12 00:34:55 +0200 | <seriously> | snd' :: (a,a,a) -> a |
| 2022-07-12 00:34:56 +0200 | <seriously> | snd' (x,y,z) = y |
| 2022-07-12 00:34:56 +0200 | <seriously> | hasMaxima :: Ord a => (a,a,a) -> Bool |
| 2022-07-12 00:34:57 +0200 | <seriously> | hasMaxima (x,y,z) = y > x && y > z |
| 2022-07-12 00:34:57 +0200 | <seriously> | localMaxima :: [Integer] -> [Integer] |
| 2022-07-12 00:34:57 +0200 | <hpc> | this is why you should use busy beaver numbers |
| 2022-07-12 00:34:58 +0200 | <seriously> | localMaxima [] = [] |
| 2022-07-12 00:34:58 +0200 | <seriously> | localMaxima [x] = [] |
| 2022-07-12 00:34:59 +0200 | <seriously> | localMaxima [x,y] = [] |
| 2022-07-12 00:34:59 +0200 | <seriously> | localMaxima (x:y:z:xs) = |
| 2022-07-12 00:35:00 +0200 | <seriously> | snd' (unzip3 (filter (\trip -> hasMaxima trip) ((x,y,z):(func (y:z:xs))))) |
| 2022-07-12 00:35:00 +0200 | <seriously> | where func [] = [] |
| 2022-07-12 00:35:01 +0200 | <seriously> | func [x] = [] |
| 2022-07-12 00:35:01 +0200 | <seriously> | func [x,y] = [] |
| 2022-07-12 00:35:02 +0200 | <seriously> | func (x:y:z:xs) = (x,y,z):func (y:z:xs) |
| 2022-07-12 00:35:03 +0200 | <monochrom> | Then you are inserting a line between somewhere, as dolio said. |
| 2022-07-12 00:35:07 +0200 | <hpc> | you're guaranteed to never run out of line numbers |
| 2022-07-12 00:35:13 +0200 | <seriously> | sorry to bloat chat; but incase any1 was curious |
| 2022-07-12 00:35:22 +0200 | <hpc> | @where paste |
| 2022-07-12 00:35:22 +0200 | <lambdabot> | Help us help you: please paste full code, input and/or output at e.g. https://paste.tomsmeding.com |
| 2022-07-12 00:35:24 +0200 | <hpc> | :P |
| 2022-07-12 00:35:25 +0200 | <sclv> | seriously: please don't paste large listings directly in chat. use the pastebin listed in the channel description |
| 2022-07-12 00:35:42 +0200 | <seriously> | ok ! |
| 2022-07-12 00:35:45 +0200 | <monochrom> | If 10 and 20 already exist, and you enter "15 whatever", it now sits between 10 and 20. |
| 2022-07-12 00:35:52 +0200 | <sclv> | lmao. |
| 2022-07-12 00:36:13 +0200 | <sclv> | somehow i thought it compiled in order and the line numbers were just jump labels |
| 2022-07-12 00:36:18 +0200 | <monochrom> | Last but not least, there is a "renumber" command to normalize your line numbers to [10, 20 ..] |
| 2022-07-12 00:36:19 +0200 | <EvanR> | i recall starting new sections at like 10000 because I figured what I was doing before could get pretty big |
| 2022-07-12 00:37:09 +0200 | <EvanR> | 10000, 20000, etc 10000 lines should be enough for anyone |
| 2022-07-12 00:39:27 +0200 | jjhoo | (~jahakala@user/jjhoo) (Remote host closed the connection) |
| 2022-07-12 00:40:01 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 272 seconds) |
| 2022-07-12 00:40:51 +0200 | <ski> | seriously : the first few defining equations of `localMaxima' is duplicating functionality of `func'. if you want to, you could avoid having multiple termination cases, by using a catch-all case (last). no need to bracket the `func (y:z:xs)' call |
| 2022-07-12 00:43:00 +0200 | <ski> | (spelling out the first point more : by the defining equation `func (x:y:z:xs) = (x,y,z):func (y:z:xs)', `(x,y,z):func (y:z:xs)' is equal to `func (x:y:z:xs)'. so you should be able to replace the former with the latter, in the last defining equation of `localMaxima' .. and then you could do further simplifications) |
| 2022-07-12 00:43:49 +0200 | jjhoo | (~jahakala@user/jjhoo) |
| 2022-07-12 00:44:18 +0200 | vglfr | (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 2022-07-12 00:44:27 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 272 seconds) |
| 2022-07-12 00:45:14 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-07-12 00:48:53 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 00:54:48 +0200 | <seriously> | ski can you elaborate on this? "the first few defining equations of `localMaxima' is duplicating functionality of `func'. if you want to, you could avoid having multiple termination cases, by using a catch-all case (last)" |
| 2022-07-12 00:55:20 +0200 | <seriously> | is "last" some sort of keyword ? |
| 2022-07-12 00:57:01 +0200 | <seriously> | I understand your bit about duplication; Im just not sure how I could remove that duplication** |
| 2022-07-12 00:57:39 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 00:58:27 +0200 | <geekosaur> | no, you put the catch-all case as the last one |
| 2022-07-12 00:58:28 +0200 | <ski> | no, not keyword |
| 2022-07-12 00:59:03 +0200 | <EvanR> | f 0 = 'a'; f 1 = 'b'; f _ = 'c' |
| 2022-07-12 00:59:19 +0200 | <ski> | @src zip |
| 2022-07-12 00:59:19 +0200 | <lambdabot> | zip (a:as) (b:bs) = (a,b) : zip as bs |
| 2022-07-12 00:59:19 +0200 | <lambdabot> | zip _ _ = [] |
| 2022-07-12 00:59:30 +0200 | <ski> | is another example of a catch-all |
| 2022-07-12 01:03:33 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 01:04:02 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 01:04:05 +0200 | kjak | (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) (Ping timeout: 272 seconds) |
| 2022-07-12 01:05:12 +0200 | <ski> | seriously : "Im just not sure how I could remove that duplication" -- well, one approach is "struck by lightning insight" (perhaps after "thinking hard" for a while), then change the code accordingly. another is incremental small changes. e.g. beginning with the replacement i suggested |
| 2022-07-12 01:06:03 +0200 | <seriously> | :ski got it ; just misunderstood the suggestion |
| 2022-07-12 01:07:05 +0200 | <ski> | (got it now ?) |
| 2022-07-12 01:07:11 +0200 | <seriously> | instead of defining the singleton list case and the [x,y] case for both func and localMaxima; I could use func _ = [] |
| 2022-07-12 01:09:56 +0200 | <ski> | you'll still need to do something more for `localMaxima', in order to have it handle all cases (while avoiding functionality duplication), i think |
| 2022-07-12 01:11:41 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-07-12 01:13:01 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 01:13:34 +0200 | <seriously> | ski heres what i got so far if tour iinterested https://paste.tomsmeding.com/4XNbmDe7 |
| 2022-07-12 01:13:38 +0200 | k60` | (~user@45.155.170.162) |
| 2022-07-12 01:15:24 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 2022-07-12 01:16:07 +0200 | <ski> | seriously : is there a reason you're checking (by pattern-matching) whether the list has three elements, in `localMaxima' ? |
| 2022-07-12 01:16:25 +0200 | <seriously> | nope |
| 2022-07-12 01:16:32 +0200 | <seriously> | thank you!! |
| 2022-07-12 01:18:33 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2022-07-12 01:18:50 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 01:21:32 +0200 | <ski> | seriously : part of the point of my comments is to realize that after getting the code working, often there can be simplifications one can perform. with practice, you'll be able to anticipate stuff like this earlier |
| 2022-07-12 01:24:11 +0200 | <seriously> | point well received *thubs up* |
| 2022-07-12 01:27:54 +0200 | hueso | (~root@user/hueso) (Ping timeout: 276 seconds) |
| 2022-07-12 01:28:09 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 272 seconds) |
| 2022-07-12 01:28:32 +0200 | hueso | (~root@user/hueso) |
| 2022-07-12 01:30:16 +0200 | seriously | (~seriously@ool-18bd55d4.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 2022-07-12 01:32:08 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-07-12 01:33:59 +0200 | enthropy | (~enthropy@24-246-69-9.cable.teksavvy.com) |
| 2022-07-12 01:35:49 +0200 | <enthropy> | Is this the best use of the monoid-statistics package: (each %%~ MS.calcMean . MS.asMean) . foldMap (each %~ MS.singletonMonoid) :: [(Double, Double,Double)] -> Maybe (Double, Double,Double) |
| 2022-07-12 01:36:39 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2022-07-12 01:37:09 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2022-07-12 01:37:58 +0200 | k60`` | (~user@94.25.174.91) |
| 2022-07-12 01:38:59 +0200 | k60` | (~user@45.155.170.162) (Ping timeout: 244 seconds) |
| 2022-07-12 01:39:53 +0200 | vglfr | (~vglfr@88.155.25.62) |
| 2022-07-12 01:39:58 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 01:42:01 +0200 | yauhsien_ | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-07-12 01:44:22 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2022-07-12 01:44:23 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 01:44:58 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-07-12 01:45:09 +0200 | Colere | (~colere@about/linux/staff/sauvin) (Ping timeout: 256 seconds) |
| 2022-07-12 01:45:52 +0200 | kimjetwav | (~user@2607:fea8:2340:fe00:730c:be2f:be5e:3847) |
| 2022-07-12 01:46:13 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 2022-07-12 01:46:54 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 2022-07-12 01:48:24 +0200 | Colere | (~colere@about/linux/staff/sauvin) |
| 2022-07-12 01:51:37 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-07-12 01:51:59 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::909a) |
| 2022-07-12 01:52:42 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-07-12 01:52:54 +0200 | dunj3 | (~dunj3@kingdread.de) (Ping timeout: 276 seconds) |
| 2022-07-12 01:53:39 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 2022-07-12 01:54:04 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-07-12 01:54:45 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 272 seconds) |
| 2022-07-12 01:57:50 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Ping timeout: 240 seconds) |
| 2022-07-12 01:58:41 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-07-12 02:05:04 +0200 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.5) |
| 2022-07-12 02:05:50 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) |
| 2022-07-12 02:06:46 +0200 | <talismanick> | Not Haskell-related necessarily, but tangential - I have some questions about the effectful semantics pf linear logic |
| 2022-07-12 02:07:35 +0200 | <talismanick> | I've been reading up on it, and while it does model resource transitions neatly, it seems less straightforward to model effects compared to, say, uniqueness typing |
| 2022-07-12 02:08:10 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 240 seconds) |
| 2022-07-12 02:08:42 +0200 | <talismanick> | But, given a single "world variable", it's straightforward to model effects with function composition - the effect is whatever the function substituted in the world argument before returning it |
| 2022-07-12 02:08:59 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 02:09:36 +0200 | <talismanick> | and, functions are naturally represented in first order logic as a 2-argument predicate with the first variable moded "in" and the second "out" (no clue if the notion of variable modes appears in formal studies of logic, but it's quite helpful in programming with Prolog) |
| 2022-07-12 02:10:46 +0200 | <talismanick> | My question is, is there a similar notion of "in and out moding of 2-predicates" in linear logic to represent sequential state transitions in a referentially-transparent-but-imperative fashion? |
| 2022-07-12 02:11:09 +0200 | alice1 | (~alice@ip68-3-91-223.ph.ph.cox.net) |
| 2022-07-12 02:11:43 +0200 | alice1 | (~alice@ip68-3-91-223.ph.ph.cox.net) (Client Quit) |
| 2022-07-12 02:11:45 +0200 | <talismanick> | Can Haskell's linear types (on arrows, right?) enforce that for the "linear logical counterpart to a function in classical logic"? |
| 2022-07-12 02:15:38 +0200 | <talismanick> | (on a related note, if categories are like groups... arrows are like homomorphisms?) |
| 2022-07-12 02:17:00 +0200 | mikoto-chan | (~mikoto-ch@d59mf84twhjn22gzzgy-4.rev.dnainternet.fi) |
| 2022-07-12 02:17:24 +0200 | <talismanick> | and, for those confused by what I mean by "moding", take a predicate in Prolog with head foo(X,Y) |
| 2022-07-12 02:19:03 +0200 | <talismanick> | If, when called with some input for X, i.e. `foo(arg, Y)`, Y is bound to a single output (X is in, Y is out because X is grounded and Y is free at calling), it can be straightforwardly translated to a function `foo X -> Y` |
| 2022-07-12 02:22:23 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 244 seconds) |
| 2022-07-12 02:27:54 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 02:30:57 +0200 | mikoto-chan | (~mikoto-ch@d59mf84twhjn22gzzgy-4.rev.dnainternet.fi) (Ping timeout: 276 seconds) |
| 2022-07-12 02:31:03 +0200 | vglfr | (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 2022-07-12 02:32:02 +0200 | seriously | (~seriously@ool-18bd55d4.dyn.optonline.net) |
| 2022-07-12 02:35:43 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2022-07-12 02:40:34 +0200 | Deide | (~deide@user/deide) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 02:42:58 +0200 | xff0x | (~xff0x@2405:6580:b080:900:1ebc:3cfb:759f:a6de) (Ping timeout: 240 seconds) |
| 2022-07-12 02:47:42 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Ping timeout: 244 seconds) |
| 2022-07-12 02:49:08 +0200 | <talismanick> | Quiet channel today, innit? |
| 2022-07-12 02:49:23 +0200 | Deide | (~deide@user/deide) |
| 2022-07-12 02:49:25 +0200 | <geekosaur> | it was busier earlier |
| 2022-07-12 02:49:44 +0200 | <geekosaur> | I'm around but the only parts of what you said that I really understood were the Prolog parts 🙂 |
| 2022-07-12 02:50:52 +0200 | <talismanick> | Funny, I explained those because I figured the Haskell crowd would be familiar with the other parts (I'm not so well-versed in type theory or mathematical at large - I'm mostly piecing it together from basic knowledge of abstract algebra) |
| 2022-07-12 02:51:08 +0200 | <talismanick> | mathematical logic at large* |
| 2022-07-12 02:51:33 +0200 | <geekosaur> | not all of us are experts on that stuff |
| 2022-07-12 02:51:52 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-07-12 02:52:44 +0200 | <hpc> | yeah, i only learned haskell after realizing i was too stupid to get by with just python :D |
| 2022-07-12 02:53:04 +0200 | <talismanick> | Linear logic itself is simple, almost stupidly so (a rule language for expressing "you can't have your cake and eat it too" instead of true/false, as Wadler put it); the hard part is all the machinery to connect it with other math/logic |
| 2022-07-12 02:56:42 +0200 | <talismanick> | I came across that revealing quote in "A Taste of Linear Logic", which does a good job as a mechanistic, programmer-accessible intro to the concepts |
| 2022-07-12 02:56:43 +0200 | <talismanick> | https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf |
| 2022-07-12 02:57:23 +0200 | <talismanick> | Although, the impression I get from self-studying logic is that it would be helpful to first appreciate why FOL is taught first, due to the importance accorded by Lindstrom's theorem |
| 2022-07-12 02:57:33 +0200 | causal | (~user@50.35.83.177) |
| 2022-07-12 02:59:47 +0200 | <talismanick> | also, I misquoted - Wadler is far more eloquent |
| 2022-07-12 02:59:54 +0200 | reza[m] | (~rezaphone@2001:470:69fc:105::3eda) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 03:02:06 +0200 | thewaves | (~thewaves@2001:470:69fc:105::2:2eef) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 03:02:34 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 2022-07-12 03:03:26 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 03:04:46 +0200 | Yehoshua | (~yehoshua@2001:470:69fc:105::1:593f) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 03:07:20 +0200 | desophos | (~desophos@50.229.86.138) |
| 2022-07-12 03:07:30 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 240 seconds) |
| 2022-07-12 03:07:44 +0200 | desophos | (~desophos@50.229.86.138) (Client Quit) |
| 2022-07-12 03:08:10 +0200 | desophos | (~desophos@50.229.86.138) |
| 2022-07-12 03:10:35 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 2022-07-12 03:13:00 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 03:14:13 +0200 | sayola1 | (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) |
| 2022-07-12 03:14:48 +0200 | sayola | (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) (Ping timeout: 276 seconds) |
| 2022-07-12 03:15:33 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 03:16:43 +0200 | albet70 | (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2022-07-12 03:21:48 +0200 | <talismanick> | Also, logic is comparatively easy to study AFAICT (and I absolutely do not mean that as a flex) if you have the time to burn |
| 2022-07-12 03:22:03 +0200 | reza[m] | (~rezaphone@2001:470:69fc:105::3eda) |
| 2022-07-12 03:22:03 +0200 | Yehoshua | (~yehoshua@2001:470:69fc:105::1:593f) |
| 2022-07-12 03:22:03 +0200 | thewaves | (~thewaves@2001:470:69fc:105::2:2eef) |
| 2022-07-12 03:22:13 +0200 | <talismanick> | As in, it's not something which should be conceptually difficult for a lot of people, unlike, say, real analysis |
| 2022-07-12 03:22:53 +0200 | <talismanick> | maybe I just haven't run into the "hard parts" yet |
| 2022-07-12 03:23:22 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2022-07-12 03:26:12 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 276 seconds) |
| 2022-07-12 03:26:57 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 244 seconds) |
| 2022-07-12 03:28:31 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 03:29:01 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 03:29:40 +0200 | Cajun | (~Cajun@user/cajun) |
| 2022-07-12 03:35:51 +0200 | alexfmpe[m] | (~alexfmpem@2001:470:69fc:105::38ba) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 03:36:05 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds) |
| 2022-07-12 03:42:31 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) |
| 2022-07-12 03:49:03 +0200 | desophos | (~desophos@50.229.86.138) (Quit: Leaving) |
| 2022-07-12 03:49:05 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 2022-07-12 03:51:29 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 03:52:52 +0200 | Hash | stoned |
| 2022-07-12 03:53:53 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-07-12 04:00:35 +0200 | zaquest | (~notzaques@5.130.79.72) (Remote host closed the connection) |
| 2022-07-12 04:00:47 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 2022-07-12 04:00:47 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 2022-07-12 04:03:00 +0200 | zaquest | (~notzaques@5.130.79.72) |
| 2022-07-12 04:06:01 +0200 | nate4 | (~nate@98.45.169.16) |
| 2022-07-12 04:12:30 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 2022-07-12 04:13:17 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 04:14:48 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 04:16:24 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 2022-07-12 04:18:30 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 240 seconds) |
| 2022-07-12 04:19:56 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 2022-07-12 04:23:50 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 2022-07-12 04:26:09 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 04:28:54 +0200 | td_ | (~td@muedsl-82-207-238-180.citykom.de) (Ping timeout: 276 seconds) |
| 2022-07-12 04:30:15 +0200 | td_ | (~td@94.134.91.223) |
| 2022-07-12 04:34:38 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 244 seconds) |
| 2022-07-12 04:36:20 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-07-12 04:36:31 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 04:41:30 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 240 seconds) |
| 2022-07-12 04:42:51 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 04:44:23 +0200 | finn_elija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-07-12 04:44:23 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 2022-07-12 04:44:23 +0200 | finn_elija | FinnElija |
| 2022-07-12 04:47:38 +0200 | frost | (~frost@user/frost) |
| 2022-07-12 04:49:06 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 04:49:09 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 04:50:31 +0200 | jargon | (~jargon@184.101.188.251) |
| 2022-07-12 04:53:58 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2022-07-12 04:55:53 +0200 | nate4 | (~nate@98.45.169.16) (Ping timeout: 272 seconds) |
| 2022-07-12 05:02:13 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2022-07-12 05:14:52 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 2022-07-12 05:16:05 +0200 | bilegeek | (~bilegeek@2600:1008:b026:a23d:b3a1:a087:edc0:7dfb) |
| 2022-07-12 05:19:04 +0200 | seriously | (~seriously@ool-18bd55d4.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 2022-07-12 05:20:35 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 272 seconds) |
| 2022-07-12 05:22:14 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 05:22:31 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 05:40:16 +0200 | mvk | (~mvk@2607:fea8:5ce3:8500::909a) (Ping timeout: 244 seconds) |
| 2022-07-12 05:48:13 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 260 seconds) |
| 2022-07-12 05:55:15 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 05:55:40 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) |
| 2022-07-12 05:58:52 +0200 | m1dnight | (~christoph@78-22-0-121.access.telenet.be) (Ping timeout: 244 seconds) |
| 2022-07-12 06:00:46 +0200 | m1dnight | (~christoph@78-22-0-121.access.telenet.be) |
| 2022-07-12 06:01:15 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 2022-07-12 06:01:15 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2022-07-12 06:01:37 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
| 2022-07-12 06:02:18 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-07-12 06:03:10 +0200 | finsternis | (~X@23.226.237.192) (Remote host closed the connection) |
| 2022-07-12 06:05:06 +0200 | jargon | (~jargon@184.101.188.251) (Remote host closed the connection) |
| 2022-07-12 06:11:26 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 268 seconds) |
| 2022-07-12 06:11:52 +0200 | enthropy | (~enthropy@24-246-69-9.cable.teksavvy.com) (Ping timeout: 252 seconds) |
| 2022-07-12 06:12:05 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 06:14:18 +0200 | rembo10 | (~rembo10@main.remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-07-12 06:15:16 +0200 | rembo10 | (~rembo10@main.remulis.com) |
| 2022-07-12 06:23:48 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2022-07-12 06:26:08 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 260 seconds) |
| 2022-07-12 06:26:53 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2022-07-12 06:29:52 +0200 | noteness | (~noteness@user/noteness) (Remote host closed the connection) |
| 2022-07-12 06:30:14 +0200 | noteness | (~noteness@user/noteness) |
| 2022-07-12 06:36:39 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 06:43:49 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 244 seconds) |
| 2022-07-12 06:52:08 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-07-12 06:56:36 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 06:59:07 +0200 | mmhat | (~mmh@p200300f1c7090723ee086bfffe095315.dip0.t-ipconnect.de) |
| 2022-07-12 07:01:05 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) |
| 2022-07-12 07:06:56 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 268 seconds) |
| 2022-07-12 07:09:15 +0200 | cony_mony[m] | (~conymonym@2001:470:69fc:105::2:2ea2) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 07:10:16 +0200 | mbuf | (~Shakthi@122.165.55.71) |
| 2022-07-12 07:16:53 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 07:17:45 +0200 | merijn | (~merijn@c-001-001-003.client.esciencecenter.eduvpn.nl) (Ping timeout: 272 seconds) |
| 2022-07-12 07:18:03 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) (Ping timeout: 260 seconds) |
| 2022-07-12 07:19:42 +0200 | Cajun | (~Cajun@user/cajun) (Ping timeout: 252 seconds) |
| 2022-07-12 07:32:00 +0200 | vglfr | (~vglfr@88.155.25.62) |
| 2022-07-12 07:45:00 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) |
| 2022-07-12 07:46:04 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 07:47:48 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2022-07-12 07:52:00 +0200 | Midjak | (~Midjak@82.66.147.146) |
| 2022-07-12 07:52:40 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-07-12 07:58:00 +0200 | Franciman | (~Franciman@mx1.fracta.dev) (Max SendQ exceeded) |
| 2022-07-12 07:58:14 +0200 | Franciman | (~Franciman@mx1.fracta.dev) |
| 2022-07-12 08:02:16 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 2022-07-12 08:05:38 +0200 | gmg | (~user@user/gehmehgeh) |
| 2022-07-12 08:07:42 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 2022-07-12 08:16:24 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 260 seconds) |
| 2022-07-12 08:16:26 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2022-07-12 08:17:07 +0200 | gmg | (~user@user/gehmehgeh) |
| 2022-07-12 08:17:55 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 2022-07-12 08:18:12 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 08:19:08 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2022-07-12 08:19:18 +0200 | monaaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 260 seconds) |
| 2022-07-12 08:21:48 +0200 | polux8 | (~polux@51-15-169-172.rev.poneytelecom.eu) |
| 2022-07-12 08:22:01 +0200 | neightchan | (~nate@98.45.169.16) |
| 2022-07-12 08:22:08 +0200 | dostoevsky6 | (~5c42c5384@user/dostoevsky) |
| 2022-07-12 08:22:38 +0200 | danso_o | (danso@danso.ca) |
| 2022-07-12 08:22:47 +0200 | kraftwerk28_ | (~kraftwerk@178.62.210.83) |
| 2022-07-12 08:22:59 +0200 | ajb- | (~ajb@mimas.whatbox.ca) |
| 2022-07-12 08:23:05 +0200 | sndr | (~sander@user/sander) |
| 2022-07-12 08:23:05 +0200 | burning_crusade | (~asturias@2001:19f0:7001:638:5400:3ff:fef3:8725) |
| 2022-07-12 08:23:09 +0200 | rush | (~sloorush@52.187.184.81) |
| 2022-07-12 08:23:20 +0200 | shriekingnoise_ | (~shrieking@201.212.175.181) |
| 2022-07-12 08:23:45 +0200 | Furor | (~colere@about/linux/staff/sauvin) |
| 2022-07-12 08:23:51 +0200 | haskl[error] | (~haskl@user/haskl) |
| 2022-07-12 08:24:01 +0200 | Qudit | (~user@user/Qudit) (Remote host closed the connection) |
| 2022-07-12 08:24:01 +0200 | kraftwerk28 | (~kraftwerk@178.62.210.83) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-07-12 08:24:01 +0200 | ajb | (~ajb@mimas.whatbox.ca) (Quit: bye) |
| 2022-07-12 08:24:02 +0200 | natechan | (~nate@98.45.169.16) (Read error: Connection reset by peer) |
| 2022-07-12 08:24:02 +0200 | dostoevsky | (~5c42c5384@user/dostoevsky) (Quit: Ping timeout (120 seconds)) |
| 2022-07-12 08:24:02 +0200 | dumptruckman | (~dumptruck@23-239-13-163.ip.linodeusercontent.com) (Quit: ZNC - https://znc.in) |
| 2022-07-12 08:24:02 +0200 | danso | (~danso@danso.ca) (Quit: ZNC - https://znc.in) |
| 2022-07-12 08:24:03 +0200 | mzan | (~quassel@mail.asterisell.com) (Remote host closed the connection) |
| 2022-07-12 08:24:03 +0200 | auri_ | (~auri@fsf/member/auri) (Remote host closed the connection) |
| 2022-07-12 08:24:03 +0200 | carbolymer | (~carbolyme@dropacid.net) (Remote host closed the connection) |
| 2022-07-12 08:24:03 +0200 | dostoevsky6 | dostoevsky |
| 2022-07-12 08:24:04 +0200 | polux | (~polux@51-15-169-172.rev.poneytelecom.eu) (Quit: Ping timeout (120 seconds)) |
| 2022-07-12 08:24:04 +0200 | shriekingnoise | (~shrieking@201.212.175.181) (Quit: Quit) |
| 2022-07-12 08:24:04 +0200 | dwt_ | (~dwt_@c-98-198-103-176.hsd1.tx.comcast.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-07-12 08:24:04 +0200 | sloorush | (~sloorush@52.187.184.81) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2022-07-12 08:24:04 +0200 | noctux | (~noctux@user/noctux) (Read error: Connection reset by peer) |
| 2022-07-12 08:24:04 +0200 | sander | (~sander@user/sander) (Quit: So long! :)) |
| 2022-07-12 08:24:04 +0200 | haskl | (~haskl@user/haskl) (Quit: Uh oh... ZNC disconnected.) |
| 2022-07-12 08:24:04 +0200 | red-snail | (~snail@static.151.210.203.116.clients.your-server.de) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-07-12 08:24:04 +0200 | remedan | (~remedan@octo.cafe) (Quit: Bye!) |
| 2022-07-12 08:24:04 +0200 | nibelungen | (~asturias@45.77.27.149) (Quit: ZNC 1.8.2+deb1+focal2 - https://znc.in) |
| 2022-07-12 08:24:04 +0200 | Inoperable | (~PLAYER_1@fancydata.science) (Quit: All your buffer are belong to us!) |
| 2022-07-12 08:24:04 +0200 | JimL | (~quassel@89-162-2-132.fiber.signal.no) (Remote host closed the connection) |
| 2022-07-12 08:24:04 +0200 | wagle | (~wagle@quassel.wagle.io) (Remote host closed the connection) |
| 2022-07-12 08:24:04 +0200 | dcoutts_ | (~duncan@host86-176-29-6.range86-176.btcentralplus.com) (Remote host closed the connection) |
| 2022-07-12 08:24:04 +0200 | Colere | (~colere@about/linux/staff/sauvin) (Remote host closed the connection) |
| 2022-07-12 08:24:04 +0200 | brettgilio | (~brettgili@c9yh.net) (Quit: Ping timeout (120 seconds)) |
| 2022-07-12 08:24:04 +0200 | dcoutts_ | (~duncan@host86-176-29-6.range86-176.btcentralplus.com) |
| 2022-07-12 08:24:04 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2022-07-12 08:24:04 +0200 | red-snail1 | (~snail@static.151.210.203.116.clients.your-server.de) |
| 2022-07-12 08:24:04 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) (Quit: No Ping reply in 180 seconds.) |
| 2022-07-12 08:24:05 +0200 | polux8 | polux |
| 2022-07-12 08:24:11 +0200 | wolfshappen_ | (~waff@irc.furworks.de) (Read error: Connection reset by peer) |
| 2022-07-12 08:24:11 +0200 | sndr | sander |
| 2022-07-12 08:24:15 +0200 | brettgilio5 | (~brettgili@c9yh.net) |
| 2022-07-12 08:24:24 +0200 | Furor | (~colere@about/linux/staff/sauvin) (Max SendQ exceeded) |
| 2022-07-12 08:24:28 +0200 | auri | (~auri@fsf/member/auri) |
| 2022-07-12 08:24:30 +0200 | dumptruckman | (~dumptruck@23-239-13-163.ip.linodeusercontent.com) |
| 2022-07-12 08:24:31 +0200 | mzan | (~quassel@mail.asterisell.com) |
| 2022-07-12 08:24:31 +0200 | JimL | (~quassel@89-162-2-132.fiber.signal.no) |
| 2022-07-12 08:24:32 +0200 | carbolymer | (~carbolyme@dropacid.net) |
| 2022-07-12 08:24:32 +0200 | noctux | (~noctux@user/noctux) |
| 2022-07-12 08:24:38 +0200 | stefan-_ | (~cri@42dots.de) (Ping timeout: 240 seconds) |
| 2022-07-12 08:24:40 +0200 | wolfshappen | (~waff@irc.furworks.de) |
| 2022-07-12 08:24:42 +0200 | Clint | (~Clint@user/clint) (Ping timeout: 264 seconds) |
| 2022-07-12 08:24:42 +0200 | zer0bitz | (~zer0bitz@2001:2003:f748:2000:a9fb:fc4a:9560:a9be) (Ping timeout: 264 seconds) |
| 2022-07-12 08:24:46 +0200 | Furor | (~colere@about/linux/staff/sauvin) |
| 2022-07-12 08:24:52 +0200 | zer0bitz | (~zer0bitz@2001:2003:f748:2000:1a4:ed4b:5e9f:8674) |
| 2022-07-12 08:24:53 +0200 | vglfr | (~vglfr@88.155.25.62) (Ping timeout: 272 seconds) |
| 2022-07-12 08:24:53 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 272 seconds) |
| 2022-07-12 08:24:54 +0200 | nckx | (~nckx@tobias.gr) (Quit: Updating my Guix System <https://guix.gnu.org>) |
| 2022-07-12 08:24:56 +0200 | kritzefitz_ | (~kritzefit@debian/kritzefitz) |
| 2022-07-12 08:24:57 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2022-07-12 08:24:58 +0200 | heath | (~heath@user/heath) (Ping timeout: 240 seconds) |
| 2022-07-12 08:24:58 +0200 | hiredman | (~hiredman@frontier1.downey.family) (Ping timeout: 240 seconds) |
| 2022-07-12 08:25:01 +0200 | remedan | (~remedan@octo.cafe) |
| 2022-07-12 08:25:05 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 2022-07-12 08:25:13 +0200 | wagle | (~wagle@quassel.wagle.io) |
| 2022-07-12 08:25:14 +0200 | cross | (~cross@spitfire.i.gajendra.net) (Ping timeout: 268 seconds) |
| 2022-07-12 08:25:18 +0200 | AWizzArd | (~code@gehrels.uberspace.de) (Ping timeout: 264 seconds) |
| 2022-07-12 08:25:18 +0200 | triteraflops | (~triterafl@user/triteraflops) (Ping timeout: 264 seconds) |
| 2022-07-12 08:25:18 +0200 | dknite | (~dknite@49.37.45.188) (Ping timeout: 264 seconds) |
| 2022-07-12 08:25:18 +0200 | mjacob | (~mjacob@adrastea.uberspace.de) (Ping timeout: 264 seconds) |
| 2022-07-12 08:25:26 +0200 | kritzefitz | (~kritzefit@debian/kritzefitz) (Remote host closed the connection) |
| 2022-07-12 08:25:26 +0200 | Clint | (~Clint@user/clint) |
| 2022-07-12 08:25:34 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2022-07-12 08:25:37 +0200 | triteraflops | (~triterafl@user/triteraflops) |
| 2022-07-12 08:25:41 +0200 | dknite | (~dknite@49.37.45.188) |
| 2022-07-12 08:25:41 +0200 | cross | (~cross@spitfire.i.gajendra.net) |
| 2022-07-12 08:25:42 +0200 | nckx | (~nckx@tobias.gr) |
| 2022-07-12 08:25:48 +0200 | mjacob | (~mjacob@adrastea.uberspace.de) |
| 2022-07-12 08:25:56 +0200 | heath | (~heath@user/heath) |
| 2022-07-12 08:25:59 +0200 | hiredman | (~hiredman@frontier1.downey.family) |
| 2022-07-12 08:26:01 +0200 | AWizzArd | (~code@gehrels.uberspace.de) |
| 2022-07-12 08:26:18 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2022-07-12 08:26:30 +0200 | stefan-_ | (~cri@42dots.de) |
| 2022-07-12 08:27:27 +0200 | In0perable | (~PLAYER_1@fancydata.science) |
| 2022-07-12 08:29:48 +0200 | kritzefitz_ | kritzefitz |
| 2022-07-12 08:30:10 +0200 | Batzy | (~quassel@user/batzy) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2022-07-12 08:30:45 +0200 | dwt_ | (~dwt_@c-98-198-103-176.hsd1.tx.comcast.net) |
| 2022-07-12 08:30:52 +0200 | bilegeek | (~bilegeek@2600:1008:b026:a23d:b3a1:a087:edc0:7dfb) (Quit: Leaving) |
| 2022-07-12 08:31:15 +0200 | <tomsmeding> | talismanick: if you try in a french-language chat you'd have more success with linear logic, I think :p |
| 2022-07-12 08:31:17 +0200 | alexfmpe[m] | (~alexfmpem@2001:470:69fc:105::38ba) |
| 2022-07-12 08:31:17 +0200 | cony_mony[m] | (~conymonym@2001:470:69fc:105::2:2ea2) |
| 2022-07-12 08:32:06 +0200 | <tomsmeding> | It's almost a meme how french theoretical CS people explain everything in terms of linear logic, because they know that well, and the rest of the world doesn't really understand and does it their way |
| 2022-07-12 08:32:42 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 08:32:44 +0200 | Batzy | (~quassel@user/batzy) |
| 2022-07-12 08:32:46 +0200 | <tomsmeding> | They even try to explain differentiation using linear logic! |
| 2022-07-12 08:32:57 +0200 | <talismanick> | tomsmeding: Ah, that's too bad - I speak Spanish, but not French. Is it still so obscure that interest is restricted to Girard's native tongue? It feels like it has a far larger presence on the Internet than in "the real world". |
| 2022-07-12 08:33:32 +0200 | <talismanick> | and, I've heard of "differential linear logic", which... I presume is a differentiable programming interpretation? |
| 2022-07-12 08:33:38 +0200 | <tomsmeding> | Sure it has more presence, but actual research is mostly concentrated in France -- and as a side-effect, also general knowledge among theoreticians |
| 2022-07-12 08:33:49 +0200 | <tomsmeding> | Sort of :D |
| 2022-07-12 08:33:52 +0200 | <tomsmeding> | But it's weird |
| 2022-07-12 08:35:29 +0200 | <tomsmeding> | talismanick: I don't know, but it feels weird to me to capture linear functions in a 2-predicate |
| 2022-07-12 08:36:00 +0200 | <edwardk> | talismanick: https://github.com/ekmett/linear-logic might be fun for you to mine through |
| 2022-07-12 08:36:26 +0200 | <ski> | people often seem to conflate linearity with uniqueness |
| 2022-07-12 08:36:26 +0200 | <edwardk> | that is basically FILL encoded into haskell |
| 2022-07-12 08:36:27 +0200 | <tomsmeding> | Because the point of linear functions (or, at least, of resource-linear functions as in Linear Haskell / Rust / Clean / whatever) is to not only be interested in _what_ the function computes, but also _how_ it goes about doing that |
| 2022-07-12 08:36:32 +0200 | <edwardk> | ski: +1 |
| 2022-07-12 08:37:04 +0200 | <talismanick> | ski: That's the impression I got. Capturing state with linearity seems more... tricky. |
| 2022-07-12 08:37:52 +0200 | NaturalNumber | (~monadam@137.229.82.64) |
| 2022-07-12 08:37:56 +0200 | <edwardk> | linearity is a promise to not contract or weaken, uniqueness is a promise that nobody else has contracted (and hence trivially, also weakened it) yet. |
| 2022-07-12 08:38:08 +0200 | <ski> | "given a single \"world variable\", it's straightforward to model effects with function composition - the effect is whatever the function substituted in the world argument before returning it" -- doesn't seem to be the case for continuation effects (e.g.), no ? |
| 2022-07-12 08:39:05 +0200 | <edwardk> | a function that takes a linear world and gives back a linear world or one that takes a unique world and gives back a unique world both achieve the same goal, but the reasoning runs completely backwards, one preserves an invariant from output to input, the other from input to output |
| 2022-07-12 08:39:16 +0200 | <talismanick> | ski: Didn't Haskell used to do I/O with continuations before monads? It's messy in practice but straightforward theorywise, AFAICT. |
| 2022-07-12 08:39:37 +0200 | <tomsmeding> | Monads are continuations :p |
| 2022-07-12 08:39:45 +0200 | <tomsmeding> | :t (>>=) |
| 2022-07-12 08:39:46 +0200 | <lambdabot> | Monad m => m a -> (a -> m b) -> m b |
| 2022-07-12 08:39:46 +0200 | <edwardk> | talismanick: technically it never used continuations. it started with lazy streams of inputs to outputs |
| 2022-07-12 08:40:03 +0200 | <edwardk> | the continuation thing is an almost-happened step in between that and monads |
| 2022-07-12 08:40:09 +0200 | <tomsmeding> | :t interact |
| 2022-07-12 08:40:11 +0200 | <lambdabot> | (String -> String) -> IO () |
| 2022-07-12 08:40:14 +0200 | <talismanick> | ah, I see |
| 2022-07-12 08:41:01 +0200 | <ski> | ("no clue if the notion of variable modes appears in formal studies of logic" -- not much, that i know (although perhaps one could draw a parallel to inductive type indices vs. types defined by structural recursion) .. one can make declarative interpretations of modes (together with associated determinisms), though. one can do this for Mercury, e.g. .. translating to universal, existential, and unique |
| 2022-07-12 08:41:05 +0200 | <talismanick> | tomsmeding: I suppose it's more so that they can faithfully capture the concrete behavior of functions beyond the rivial case of "take a single world argument, return it modified"? |
| 2022-07-12 08:41:07 +0200 | <ski> | quantifiers) |
| 2022-07-12 08:41:39 +0200 | <talismanick> | (linear predicates) |
| 2022-07-12 08:41:41 +0200 | <ski> | ("on a related note, if categories are like groups... arrows are like homomorphisms?" -- arrows ? like the type class `Arrow' or ?) |
| 2022-07-12 08:41:56 +0200 | <talismanick> | ski: I meant in the formal, category-theoretic sense |
| 2022-07-12 08:42:01 +0200 | <talismanick> | I'm no algebra expert :) |
| 2022-07-12 08:42:06 +0200 | <tomsmeding> | ski: (->) |
| 2022-07-12 08:42:15 +0200 | <talismanick> | arrows are the same thing as morphisms, right? |
| 2022-07-12 08:42:22 +0200 | <tomsmeding> | In CT, yes |
| 2022-07-12 08:42:25 +0200 | <tomsmeding> | In Haskell, no |
| 2022-07-12 08:42:31 +0200 | <tomsmeding> | Unfortunate name clash |
| 2022-07-12 08:42:51 +0200 | <talismanick> | ugh |
| 2022-07-12 08:42:53 +0200 | wildsebastian | (~wildsebas@2001:470:69fc:105::1:14b1) |
| 2022-07-12 08:43:11 +0200 | <tomsmeding> | `Arrow` is a completely different think in Haskell |
| 2022-07-12 08:43:14 +0200 | <edwardk> | in haskell Arrow refers to a Freyd category, which is a godawful messy beasst |
| 2022-07-12 08:43:15 +0200 | <tomsmeding> | *thing |
| 2022-07-12 08:43:21 +0200 | schweers | (~user@2001:9e8:be64:4500:aaa1:59ff:fe3f:235c) |
| 2022-07-12 08:43:46 +0200 | <talismanick> | I figured something beyond my understanding was afoot when I came across the Arrow typeclass in descriptions of FRP and stateful automata |
| 2022-07-12 08:44:04 +0200 | <ski> | "is there a similar notion of \"in and out moding of 2-predicates\" in linear logic to represent sequential state transitions in a referentially-transparent-but-imperative fashion?" -- hm .. i haven't seen it. i have thought a little bit about wanting to talk about something like linearity of terms in Lolli (linear logic programming language, based on lambdaProlog) .. but i didn't really get that far |
| 2022-07-12 08:44:12 +0200 | <edwardk> | talismanick: if you walk away slowly and pretend you never saw the class, nothing of value will be lost =P |
| 2022-07-12 08:44:25 +0200 | <talismanick> | "I know 'Hask isn't a category', but isn't it that functions are arrows, type are objects in Hask?" |
| 2022-07-12 08:44:43 +0200 | <tomsmeding> | talismanick: you mean capturing yhe behaviour of a linear function without necessarily having the material in that representation to _prove_ that it conforms to the linearity restrictions? |
| 2022-07-12 08:44:46 +0200 | <ski> | edwardk : well, you pointed out that to me, initially :) |
| 2022-07-12 08:45:04 +0200 | <edwardk> | ski: hah. repeating it mostly for the crowd =) |
| 2022-07-12 08:45:34 +0200 | <edwardk> | i do wish uniqueness fit cleanly into QTT like the other modalities |
| 2022-07-12 08:45:38 +0200 | <talismanick> | tomsmeding: Well, isn't that the pipe dream of functional programming since Backus? To provide programs with declarative meaning and let the compiler figure out what that looks like on hardware |
| 2022-07-12 08:46:16 +0200 | <talismanick> | (if I understand what you're saying correctly) |
| 2022-07-12 08:46:31 +0200 | <tomsmeding> | talismanick: I mean, yes, but the point of adding resource-linear types to a _programming language_ is to shift that responsibility partway to the programmer |
| 2022-07-12 08:46:46 +0200 | <ski> | talismanick: "Didn't Haskell used to do I/O with continuations before monads?" -- yes. and the CPS was done to use the Dialogue-style I/O in a more principled (less brittle, more robust) way |
| 2022-07-12 08:47:23 +0200 | nerdypepper | aksnay |
| 2022-07-12 08:47:30 +0200 | aksnay | akshay |
| 2022-07-12 08:47:32 +0200 | <edwardk> | ski: re linear logic in logic programming, i did spend a fair bit of time playing around with a home-grown linear-LF using QTT, but i got too ambitious in terms of type inference and it kind of fell apart |
| 2022-07-12 08:47:38 +0200 | <tomsmeding> | To give the programmer control over specifying that certain things must be done sequentially -- and this sequentislity requirement becomes a guarantee that you can then use in the implementation to do something more efficient |
| 2022-07-12 08:48:13 +0200 | <edwardk> | the motivation is that having proper substructural types using QTT means i can then use it to reason using HOAS about languages that _themselves_ use some (possibly) coarser semiring choice of QTT. |
| 2022-07-12 08:48:25 +0200 | Furor | Colere |
| 2022-07-12 08:48:26 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2022-07-12 08:48:30 +0200 | <talismanick> | That's true. I wonder if there exists something akin to a "multilinear logic" with selective linearity on arguments |
| 2022-07-12 08:48:34 +0200 | <ski> | (Andrew Appel has a chapter that uses an opaque `Answer' type as the target type of CPS. this is pretty similar to the `type Dialogue = [Response] -> [Request]' stuff, except the latter is transparent) |
| 2022-07-12 08:48:55 +0200 | <talismanick> | (I came across work on a "tensorial logic", which seemed interesting in its own right, but it wasn't what I was looking for) |
| 2022-07-12 08:48:59 +0200 | <tomsmeding> | talismanick: like `f :: a %1-> b -> c` in linear haskell? :P |
| 2022-07-12 08:49:17 +0200 | <edwardk> | otherwise using an LF to reason about another type system, that uses quantitative types, linear types, etc. is a mess, because the whole selling point is that you get HOAS, but then HOAS falls apart or can't express all your envariables, and you are forced to use De Bruijn like a barbarian in a deliberately crippled language that makes that hard to pay for HOAS you can't use! |
| 2022-07-12 08:49:18 +0200 | <talismanick> | I suppose you do get it naturally out of currying... |
| 2022-07-12 08:49:30 +0200 | <tomsmeding> | Takes two arguments, the first linearly and the second non-linearly |
| 2022-07-12 08:49:51 +0200 | <edwardk> | talismanick: selective linearity and the work on "Quantitative Type Theory" are basically the same idea |
| 2022-07-12 08:49:59 +0200 | <tomsmeding> | edwardk: sorry, LF? |
| 2022-07-12 08:50:07 +0200 | <ski> | (er, Appel has a chapter with that, in his "Modern Compiler Implementation in (Java|C|ML)" in 1997,1998 at <https://www.cs.princeton.edu/~appel/modern/>) |
| 2022-07-12 08:50:08 +0200 | <edwardk> | LF = logical framework, like twelf |
| 2022-07-12 08:50:09 +0200 | <talismanick> | okay, that sounds like a new term for me to read up about |
| 2022-07-12 08:50:12 +0200 | <tomsmeding> | Thanks |
| 2022-07-12 08:50:13 +0200 | <talismanick> | thanks for the reference |
| 2022-07-12 08:50:35 +0200 | <edwardk> | a deliberately crippled notion of dependent types, where it is crippled enough that HOAS works. unlike in say, coq or agda |
| 2022-07-12 08:51:07 +0200 | <edwardk> | logical frameworks get used like typed prolog a lot. with modes, etc. |
| 2022-07-12 08:51:29 +0200 | <talismanick> | (I wondered at first, "is QTT an acronym for Cubical Type Theory, perhaps?") |
| 2022-07-12 08:51:33 +0200 | <tomsmeding> | I don't know anything about LFs :) |
| 2022-07-12 08:52:58 +0200 | <ski> | edwardk : hm, i think i may've downloaded some Linear version of Twelf at some point, but didn't get as far as playing around with it |
| 2022-07-12 08:53:19 +0200 | <tomsmeding> | talismanick: that would be 🧊TT |
| 2022-07-12 08:54:22 +0200 | <talismanick> | tomsmeding: your joke fails because it shows up as :ice-cube : (in plain text) in Emacs! |
| 2022-07-12 08:54:31 +0200 | <tomsmeding> | Lol |
| 2022-07-12 08:54:35 +0200 | <talismanick> | (I disabled emojis because Unicode is hanging it for some reason) |
| 2022-07-12 08:54:50 +0200 | <tomsmeding> | Sad that there is no plain cube in unicode |
| 2022-07-12 08:54:58 +0200 | <edwardk> | https://www.irccloud.com/pastebin/SZklR7W2/example.lf |
| 2022-07-12 08:55:00 +0200 | <talismanick> | or, some Unicode - it'd be nice if "everything broke" so I knew "Unicode is the problem" and could fix it |
| 2022-07-12 08:55:12 +0200 | <edwardk> | ^- there is a sketch of how you use an LF relative to a prolog or datalog program |
| 2022-07-12 08:55:30 +0200 | <edwardk> | the <- arrow is just that a flipped arrow |
| 2022-07-12 08:55:47 +0200 | <edwardk> | rule2 has an implicit pi type in its signature |
| 2022-07-12 08:56:01 +0200 | <talismanick> | edwardk: backwards implication, like in a Horn clause? |
| 2022-07-12 08:56:36 +0200 | <talismanick> | oh, definitely it - just looked |
| 2022-07-12 08:57:05 +0200 | <tomsmeding> | edwardk: so I could read rule1 as having type `parent X Y -> ancestor X Y`? |
| 2022-07-12 08:57:06 +0200 | <edwardk> | rule2 : Π X Y Z : name. parent X Y -> ancestor Y Z -> ancestor X Z |
| 2022-07-12 08:57:10 +0200 | <edwardk> | yep |
| 2022-07-12 08:57:12 +0200 | <tomsmeding> | Right |
| 2022-07-12 08:57:24 +0200 | <edwardk> | er with the right variables |
| 2022-07-12 08:57:31 +0200 | <edwardk> | X Y and Y Z |
| 2022-07-12 08:57:55 +0200 | <edwardk> | haskell-like n that using a variable (in upper case here) implicitly quantifies it |
| 2022-07-12 08:57:57 +0200 | <tomsmeding> | Both of our messages are correct, right? |
| 2022-07-12 08:58:03 +0200 | <edwardk> | yes |
| 2022-07-12 08:58:34 +0200 | <ski> | "envariables" ? |
| 2022-07-12 08:58:36 +0200 | <edwardk> | the convention is to write with the <- in LFs so it reads more like the :- in datalogg |
| 2022-07-12 08:58:38 +0200 | <tomsmeding> | So is this term search? |
| 2022-07-12 08:58:41 +0200 | <edwardk> | yeah |
| 2022-07-12 08:58:53 +0200 | <tomsmeding> | Cool |
| 2022-07-12 08:58:59 +0200 | <edwardk> | program synthesis as a 'proof-relevant' version of prolog |
| 2022-07-12 08:59:07 +0200 | <tomsmeding> | Neat |
| 2022-07-12 08:59:17 +0200 | <edwardk> | types as judgments, there's some neat reasoning you can do within this framework |
| 2022-07-12 08:59:35 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-07-12 08:59:35 +0200 | boxscape | (~boxscape@user/boxscape) (Quit: Client limit exceeded: 20000) |
| 2022-07-12 08:59:44 +0200 | <ski> | `fact1',`fact2',`rule1',`rule2' act like data constructors for `parent' and `ancestor' (just like `bob',`nancy' are for `name') -- you can match on them |
| 2022-07-12 08:59:54 +0200 | <edwardk> | whats interesting is you can just hallucinate whatever types you want into scope. like the equivalent of asserting data constructors with assumptions |
| 2022-07-12 08:59:58 +0200 | acidjnk | (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) |
| 2022-07-12 08:59:59 +0200 | boxscape | (~boxscape@user/boxscape) |
| 2022-07-12 09:00:12 +0200 | <edwardk> | matching is forbidden =) |
| 2022-07-12 09:00:27 +0200 | <edwardk> | the point of an LF is that it gives you no tools for pattern matching |
| 2022-07-12 09:00:31 +0200 | <edwardk> | so. HOAS is always valid |
| 2022-07-12 09:00:34 +0200 | <edwardk> | no exotic terms can exist |
| 2022-07-12 09:00:41 +0200 | <tomsmeding> | Yeah I was wondering what would happen if you'd allow matching on the proof here :p |
| 2022-07-12 09:01:10 +0200 | <edwardk> | the nice thing is you can write a lambda calculus with something like: tm : type; lam : (tm -> tm) -> tm; app : tm -> tm -> tm |
| 2022-07-12 09:01:18 +0200 | <edwardk> | and you get the 'var' case for free |
| 2022-07-12 09:01:20 +0200 | <ski> | yea, you can't match in terms (expressions). you can only match during search (of solutions / proof of a goal) |
| 2022-07-12 09:01:25 +0200 | <edwardk> | lam (\x -> x) |
| 2022-07-12 09:01:29 +0200 | <tomsmeding> | Right, funny thing is that when I was first explained HOAS in a lecture, first thing I did in the break was show the teacher what I now know is an exotic term, and ask how can this possibly work |
| 2022-07-12 09:02:03 +0200 | <edwardk> | because i can know that the function i hand in which is given an abstract 'tm' can't match on it in any way |
| 2022-07-12 09:02:13 +0200 | <tomsmeding> | Yeah that's nice about hoas |
| 2022-07-12 09:02:29 +0200 | <ski> | calling `parent bob X' is matching that goal with the clause (fact) `parent bob nancy', so that `X' becomes `nancy' |
| 2022-07-12 09:02:31 +0200 | <edwardk> | this makes reasoning about "meta-theory" in an LF very nice. because there i'm reasoning about an arbitrary LF program, not an arbitrary Coq program or the like |
| 2022-07-12 09:02:39 +0200 | <tomsmeding> | But it's godawful to work with if you want to do something to the terms you're representing in hoas form |
| 2022-07-12 09:02:53 +0200 | christiansen | (~christian@83-95-137-75-dynamic.dk.customer.tdc.net) |
| 2022-07-12 09:02:56 +0200 | <ski> | (and ditto for calling `ancestor', which calls `parent') |
| 2022-07-12 09:03:02 +0200 | <edwardk> | well, in dependent type land you are usually stuck with some phoas trick, which _is_ awful. |
| 2022-07-12 09:03:13 +0200 | <edwardk> | but in an LF you are usually able to stick in proper hoas. |
| 2022-07-12 09:03:33 +0200 | <edwardk> | and the benefit is that if you can express what you want using HOAS in LF you can't "fuck up the names" |
| 2022-07-12 09:03:36 +0200 | <talismanick> | phoas? |
| 2022-07-12 09:03:48 +0200 | <tomsmeding> | Try doing something like common subexpression elimination on a program represented in hoas form |
| 2022-07-12 09:03:51 +0200 | <edwardk> | phoas = parametric hoas. adam chlipala has a paper on it |
| 2022-07-12 09:03:56 +0200 | <edwardk> | tomsmeding: have, it sucks |
| 2022-07-12 09:04:03 +0200 | <tomsmeding> | :D |
| 2022-07-12 09:04:15 +0200 | <edwardk> | this is why i've been working towards an LF using egg |
| 2022-07-12 09:04:21 +0200 | <edwardk> | then i can just get it all by magic for free |
| 2022-07-12 09:04:47 +0200 | <edwardk> | CSE, optimization rules, whatever |
| 2022-07-12 09:05:11 +0200 | <tomsmeding> | @hackage egg |
| 2022-07-12 09:05:11 +0200 | <lambdabot> | https://hackage.haskell.org/package/egg |
| 2022-07-12 09:05:14 +0200 | <tomsmeding> | 404 |
| 2022-07-12 09:05:37 +0200 | <ski> | right, to be able to do variables in HOAS, using `tm', you need goal implication and goal universal quantification (which lambdaProlog also has, but Prolog doesn't really .. well, you can code a forall/2 predicate (which technically is implication, not universal quantification, while achieving the effect of both) .. but operationally it behaves differently. enumerating and testing, as opposed to conjuring up |
| 2022-07-12 09:05:39 +0200 | <edwardk> | if you look at https://github.com/philzook58/egglog0-talk/blob/main/out.pdf and try to do the same transformation from it to a LF that i sketched for prolog/datalog above you get the idea |
| 2022-07-12 09:05:39 +0200 | <tomsmeding> | Was it something something egraphs? |
| 2022-07-12 09:05:43 +0200 | <ski> | skolems and assuming clauses) |
| 2022-07-12 09:05:46 +0200 | <edwardk> | egg is egraphs-good, yeah |
| 2022-07-12 09:05:48 +0200 | <edwardk> | its in rust |
| 2022-07-12 09:06:11 +0200 | <edwardk> | spent the weekend trying to make a nice model of egraphs in haskell and generally failing |
| 2022-07-12 09:06:23 +0200 | <edwardk> | (i want a _nice_ API) |
| 2022-07-12 09:07:13 +0200 | <edwardk> | ski: my end-goal with an LF is to get to one that works in a more guanxi/kanren like fashion for the search than a traditional LF, so i can program usefully with those relations |
| 2022-07-12 09:07:37 +0200 | <edwardk> | twelf uses a prolog'ish, depth-first search |
| 2022-07-12 09:07:55 +0200 | <edwardk> | and so you find yourself with the usual limitations you'd expect from an untabled prolog |
| 2022-07-12 09:07:57 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 272 seconds) |
| 2022-07-12 09:08:13 +0200 | <edwardk> | easily bottoming out, needing but not having the equivalent of cut, etc. |
| 2022-07-12 09:09:41 +0200 | coot | (~coot@213.134.190.95) |
| 2022-07-12 09:09:52 +0200 | <edwardk> | for the record, i'm rather aggressively hiring on the egg/e-graph side of things at groq. |
| 2022-07-12 09:10:19 +0200 | <ski> | edwardk : hm, what's the specific guanxi/kanren part ? (haven't looked in detail at these) |
| 2022-07-12 09:10:23 +0200 | <edwardk> | the LFish bits above are more my own personal project though |
| 2022-07-12 09:10:35 +0200 | <ski> | being able to externally customize search in some way ? |
| 2022-07-12 09:10:40 +0200 | <edwardk> | kanren does a logict style search (it was why LogicT was invented) |
| 2022-07-12 09:10:58 +0200 | <edwardk> | logict has the benefit of offering a 'fairer' interleaving of goals. |
| 2022-07-12 09:11:03 +0200 | <edwardk> | the WAM is depth first |
| 2022-07-12 09:11:48 +0200 | <edwardk> | you can think of logict as offering a sort of 'divergence by halves'. if you give half of your attention to the first goal, and half of what remains to the next, and half of what remains to the next.. you get a sort of geometric series. so instead of diverging you just slow by 2x |
| 2022-07-12 09:12:04 +0200 | <edwardk> | so if there's a match to be found you'll still find it rather than bottom out hard |
| 2022-07-12 09:12:15 +0200 | <ski> | re cut, perhaps it could borrow some ideas from Mercury there (switch disjunctions, committed-choice nondeterminism) ? |
| 2022-07-12 09:12:19 +0200 | <edwardk> | guanxi is partially about refining that to distributions that don't look like strict powers of 2 |
| 2022-07-12 09:12:47 +0200 | <edwardk> | committed-choice is very much like cut in that it is a non-compositional reasoning tool. |
| 2022-07-12 09:13:05 +0200 | <edwardk> | i want thing that feel like programming with relations, where i glue two relations together and don't have to care about their guts |
| 2022-07-12 09:13:19 +0200 | <edwardk> | that is kanren's strength (and biggest weakness) |
| 2022-07-12 09:13:37 +0200 | <edwardk> | kanren doesn't do enough to cut the exponent in the search space down |
| 2022-07-12 09:13:43 +0200 | <edwardk> | that is why i went off and worked on guanxi |
| 2022-07-12 09:13:52 +0200 | <talismanick> | edwardk: akin to how power sets being of 2^n cardinality can be considered as a consequence of n binary probabilistic experiments? (set inclusion or exclusion) |
| 2022-07-12 09:14:53 +0200 | benin0 | (~benin@183.82.29.162) |
| 2022-07-12 09:15:05 +0200 | <Axman6> | Damn, I've missed a Kmettflood on cool stuff |
| 2022-07-12 09:15:07 +0200 | <ski> | well, committed-choice nondeterminism in Mercury is declarative. it's used when a goal has no output instantiations (e.g. because of existential quantification). in that case, the inner goal is called in a way to compute at most one solution |
| 2022-07-12 09:15:12 +0200 | <edwardk> | talismanick: well, it has implementation consequences in the WAM you can actually change variables mutably to point to their current bindings, and backtrack on the way out. but when you have, multiple logical threads being tracked, you need to carry the environment has an explicit substitution and pay for that in performance (this is how kanren works) |
| 2022-07-12 09:17:22 +0200 | <talismanick> | for the WAM (with which I am somewhat familiar with on a surface level), I've never understood why "tagging lvars with more info" (many-sorted logic) and partitioning search with that extra info couldn't be used to encapsulate and prune search spaces for more "usable" programming |
| 2022-07-12 09:17:27 +0200 | <ski> | (you can also use it to explicitly ask for just one solution, out of many possible, for `main'. and you can `promise' that a committed-choice nondet goal, at that point, has one / at most one solution, upto duplicates (which can involve nontrivially equivalent structures, in case of user-defined equality, iow quotients)) |
| 2022-07-12 09:17:56 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2022-07-12 09:18:05 +0200 | <talismanick> | (we reason in terms of types anyways, in programming and even in normal math - no one does stuff from FOL or ZFC - so why not in Prolog, too?) |
| 2022-07-12 09:18:34 +0200 | <edwardk> | talismanick: that is basically the guanxi approach. tracking propagators between variables, to reduce the exponent in the search space, then using a more kanren style search to avoid spuriously bottoming out, but adding (abstract) conflict-directed clause learning so it can learn about other worlds rather than brute force everything |
| 2022-07-12 09:18:59 +0200 | Cajun | (~Cajun@user/cajun) |
| 2022-07-12 09:19:18 +0200 | <edwardk> | ski: i don't hate the notion of a committed choice when the alternatives are indistinguishable |
| 2022-07-12 09:19:19 +0200 | <talismanick> | fascinating. Does it bear relation to categorical logic? Of all topics, that sounds like an obviously rich combo, but I'm a ways off from being ready to read about it |
| 2022-07-12 09:19:27 +0200 | <edwardk> | distinguishable committed choices are more concerning to me |
| 2022-07-12 09:20:10 +0200 | <talismanick> | (I imagine categorical logic deals in facts "hidden" behind products lifted into objects) |
| 2022-07-12 09:20:16 +0200 | <edwardk> | https://www.youtube.com/watch?v=D7rlJWc3474 is an intro to the ideas behind the guanxi project. though i got pulled away from it when i left MIRI |
| 2022-07-12 09:20:29 +0200 | <ski> | edwardk : i think pbone worked on sharing logic / "dataflow" variables between multiple threads of execution (both kinds of AND-parallelism, iirc) |
| 2022-07-12 09:20:37 +0200 | <edwardk> | the first video in that sequence is pretty self-contained. the other 3 get progressively more workshop like |
| 2022-07-12 09:21:48 +0200 | <edwardk> | talismanick: there's a lot of category theory involved in talking about the different adjunctions between various abstract interpretation domains, but no categorical logic per se |
| 2022-07-12 09:21:48 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 2022-07-12 09:22:45 +0200 | <edwardk> | my goal with this was to use it as an intermediate form for manipulating the half-compiled guts of a higher level language |
| 2022-07-12 09:22:58 +0200 | <edwardk> | e.g. i didn't want to write a full coda compiler in haskell, then have to bootstrap |
| 2022-07-12 09:23:02 +0200 | <ski> | ("and backtrack on the way out" -- reminds me of a simple prototype i did, which enabled "backtracking backtracking" (in arbitrary many steps), wrt having goal implications (better behaving than the forall/2 (or foreach/2) Prolog ones) .. of the generate&test rather than the conjure&assume variant. also involved flipping interpretation between skolems and logic variables) |
| 2022-07-12 09:23:13 +0200 | MajorBiscuit | (~MajorBisc@wlan-145-94-167-213.wlan.tudelft.nl) |
| 2022-07-12 09:23:37 +0200 | <edwardk> | i;d rather write a fancy logical framework in haskell, then compile down to the LF from the high level language, then just have to port the LF to the new language |
| 2022-07-12 09:24:12 +0200 | <ski> | talismanick : "lvars" as in "logic variables", or as in `lvish' ? |
| 2022-07-12 09:24:19 +0200 | <ski> | @hackage lvish |
| 2022-07-12 09:24:19 +0200 | <lambdabot> | https://hackage.haskell.org/package/lvish |
| 2022-07-12 09:24:53 +0200 | <edwardk> | ski: my approach is a little "cute" in that what i do is turn fair coinflips into arbitrary distributions using an arithmetic decoder. but then track the bitstrings i used. |
| 2022-07-12 09:25:20 +0200 | <edwardk> | the key is that when you backtrack and learn there's no solution in a space you need to mark off the space of bits that would encode to the same solution |
| 2022-07-12 09:25:22 +0200 | `2jt | (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) |
| 2022-07-12 09:25:35 +0200 | <ski> | edwardk : "distinguishable committed choices are more concerning to me" -- agreed |
| 2022-07-12 09:25:48 +0200 | JimL | (~quassel@89-162-2-132.fiber.signal.no) (Ping timeout: 260 seconds) |
| 2022-07-12 09:25:51 +0200 | chomwitt | (~chomwitt@2a02:587:dc0d:4a00:cff7:1232:6084:40) |
| 2022-07-12 09:25:53 +0200 | <ski> | (when i mention "comitted choice", i usually mean the latter) |
| 2022-07-12 09:26:12 +0200 | <edwardk> | the idea is then that if you go off and try things for a while, you get a tree of bits that collapses as you learn more, and if it collapses all the way you exhausted the space |
| 2022-07-12 09:26:19 +0200 | <ski> | (er, by latter i meant "when the alternatives are indistinguishable", sorry) |
| 2022-07-12 09:26:30 +0200 | <edwardk> | and you can go back to the start and start flipping coins again as a form of restarts |
| 2022-07-12 09:27:09 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 09:27:17 +0200 | <edwardk> | the arithmetic decoder turns coinflips into arbitrary distributions so you aren't stuck with paying some KL-divergence driven overhead relative to assuming the distribution looks like (0.5,0.25,0.125...) |
| 2022-07-12 09:27:48 +0200 | <edwardk> | which since that divergence is affecting the POWER in an exponential, is insane |
| 2022-07-12 09:27:51 +0200 | <talismanick> | ski: logic variables, because I needed to go to the bathroom :) |
| 2022-07-12 09:28:39 +0200 | <talismanick> | (barely enough time to type that out) |
| 2022-07-12 09:29:16 +0200 | <talismanick> | Now that I think about it, this whole discussion has me positively drained digging about my mind for relevant references |
| 2022-07-12 09:29:23 +0200 | <ski> | edwardk : hm, "collapse" here meaning ? |
| 2022-07-12 09:29:28 +0200 | <edwardk> | in any event you can basically just give an implementation a luby-style restart timer, where it tries random probes into the space that are single shot interleaved with ones that have exponentially longer and longer runtime, and that system above will find everything if the system is exhaustible, and by tracking and ruling out any place you've been before its not _that_ bad. |
| 2022-07-12 09:29:40 +0200 | lbseale | (~quassel@user/ep1ctetus) (Ping timeout: 244 seconds) |
| 2022-07-12 09:29:42 +0200 | <talismanick> | time for bed, I suppose |
| 2022-07-12 09:30:05 +0200 | <ski> | ("KL" ?) |
| 2022-07-12 09:30:09 +0200 | <edwardk> | consider if i flip and get 1 for the first bit, then try 10, and fail, and backtrack and try 11 and fail, then i can rule out all bitstrings that start with 1. |
| 2022-07-12 09:30:24 +0200 | <edwardk> | i don't need to store all the suffixes i tried |
| 2022-07-12 09:30:28 +0200 | <edwardk> | just that everything after 1* is dead |
| 2022-07-12 09:30:39 +0200 | <edwardk> | if i get down to * is dead i'm done, no solution exists |
| 2022-07-12 09:31:24 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 2022-07-12 09:31:39 +0200 | <edwardk> | but now consider if instead of choices that are binary i have something like a solution 0 that i want to give 90% of the time, and 1 that i want to try 10% of the time. the arithmetic code for that has lots of things that lead to trying 0 |
| 2022-07-12 09:31:41 +0200 | <ski> | i see .. what i thought, but wanted confirmation |
| 2022-07-12 09:32:06 +0200 | NaturalNumber | (~monadam@137.229.82.64) (Quit: Leaving) |
| 2022-07-12 09:32:36 +0200 | <ski> | (i'm reminded of one of Brouwer's three inference steps (i forget the name), wrt bar induction) |
| 2022-07-12 09:32:50 +0200 | <edwardk> | 0, 10, 110 all try the "0" solution, so we need to encode the fact that when i try any one of them that the entire interval of bitstrings that would yield 0 is masked off (lazily) in the bit tree. |
| 2022-07-12 09:33:23 +0200 | <edwardk> | er i should have had ... in there on the candidates for selecting 0 in the arithmetic decoder |
| 2022-07-12 09:33:39 +0200 | <edwardk> | or chosen something that did evenly break into binary =) |
| 2022-07-12 09:33:54 +0200 | Axman6 | is wondering how long until Ed starts designing a CPU with support for propagators in Clash |
| 2022-07-12 09:33:58 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 09:34:22 +0200 | <edwardk> | Axman6: i'm busy designing chips with support for ridiculous SIMD parallelism |
| 2022-07-12 09:34:34 +0200 | <edwardk> | propagators can sit on top of that =P |
| 2022-07-12 09:35:09 +0200 | <edwardk> | propagators don't seem to need any real hardware support from my view |
| 2022-07-12 09:35:13 +0200 | <Axman6> | need a SIMP processor |
| 2022-07-12 09:35:19 +0200 | <edwardk> | =P |
| 2022-07-12 09:35:41 +0200 | <Axman6> | Groq needs better duckduckgo SEO |
| 2022-07-12 09:35:52 +0200 | dostoevsky | (~5c42c5384@user/dostoevsky) (Quit: Ping timeout (120 seconds)) |
| 2022-07-12 09:36:05 +0200 | <edwardk> | http://pkamath.com/publications/papers/tsp-isca20.pdf <- is the best summary of the v1 chip's architecture |
| 2022-07-12 09:36:11 +0200 | <Axman6> | It's a shame your jobs are all US based, I'd be interested |
| 2022-07-12 09:36:23 +0200 | dostoevsky | (~5c42c5384@user/dostoevsky) |
| 2022-07-12 09:36:27 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) (Ping timeout: 272 seconds) |
| 2022-07-12 09:36:27 +0200 | chomwitt | (~chomwitt@2a02:587:dc0d:4a00:cff7:1232:6084:40) (Ping timeout: 272 seconds) |
| 2022-07-12 09:37:34 +0200 | <ski> | edwardk : if every path through the (possibly infinite) tree, via the `00' branch from the root, and via the `10' branch, can be detected to be barred, then every path through `0' can be detected to be barred |
| 2022-07-12 09:37:47 +0200 | <edwardk> | https://www.youtube.com/watch?v=upljocX5mrk and https://www.youtube.com/watch?v=kPUxl00xys4 cover the way we compile and the way we do determinstic networking to turn lots of fully deterministic chips into a big deterministic cluster |
| 2022-07-12 09:37:53 +0200 | <ski> | (iiuc your bit indexing correctly) |
| 2022-07-12 09:38:05 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-07-12 09:38:15 +0200 | ski | tried finding a source listing the inference rules to check, failed for the moment |
| 2022-07-12 09:38:42 +0200 | <Axman6> | edwardk: I just promised my psychologist that I'd stop staying up late watching YouTube videos, thanks for ruining that for me :P |
| 2022-07-12 09:38:55 +0200 | <edwardk> | Axman6: we have some folks in the UK and a _lot_ in canada, but aussie timezones are a bit of a stretch for us logistically |
| 2022-07-12 09:39:06 +0200 | <ski> | "Groq" ? |
| 2022-07-12 09:39:14 +0200 | <Axman6> | Can;t handle people too far in the future, I understand that |
| 2022-07-12 09:39:16 +0200 | <edwardk> | tell them some crazy guy on the internet made you do it |
| 2022-07-12 09:39:56 +0200 | <edwardk> | ski: groq is a company i work for as their head of software, we build AI accelerator chips. |
| 2022-07-12 09:40:05 +0200 | <Axman6> | edwardk: only vaugely relatedm but are you familliar with the Mill CPU work? |
| 2022-07-12 09:40:22 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2022-07-12 09:40:25 +0200 | <Axman6> | Groq is a Google (Alphabet?) thing right/ |
| 2022-07-12 09:40:27 +0200 | <Axman6> | ?* |
| 2022-07-12 09:40:27 +0200 | <lambdabot> | Maybe you meant: v @ ? . |
| 2022-07-12 09:40:30 +0200 | <edwardk> | if you are familiar at all with Google's TPUs, the guy who designed those (in BlueSpec, a dialect of haskell no less!) is Jonathan Ross, now the CEO of Groq. |
| 2022-07-12 09:41:07 +0200 | <edwardk> | groq is not alphabet related. its more part of the google diaspora of folks who left and decided to do things while keeping a sort of googlish culture. |
| 2022-07-12 09:41:28 +0200 | <edwardk> | i'm familiar with the pain and mess that is mill ;) |
| 2022-07-12 09:41:32 +0200 | <Axman6> | Right, fair enough - is there a similar company making Google's hardware? |
| 2022-07-12 09:41:42 +0200 | <edwardk> | yeah, its called google. |
| 2022-07-12 09:42:04 +0200 | <Axman6> | Hmm, I thought they had a spinout, but maybe I was just thinking of Groq |
| 2022-07-12 09:43:18 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2022-07-12 09:44:16 +0200 | <edwardk> | TPUs still exist. Groq's notion is basically just to double down on what makes them good. When Jonathan originally proposed the TPU project and Jeff Dean accepted, he somehow overpromised that he'd use like 70% of the theoretical efficiency of the LUTs and DSPs on the FPGAs he was using at the time, 35% is generally what folks expect. |
| 2022-07-12 09:44:32 +0200 | mc47 | (~mc47@xmonad/TheMC47) |
| 2022-07-12 09:45:07 +0200 | <edwardk> | he managed to deliver it by using lots of crazy bluespec-like chicanery. then they brought in traditional hardware folks, because it was becoming the next big thing at google and they wanted in... and it dropped right back down to the 'expected' result |
| 2022-07-12 09:45:51 +0200 | <edwardk> | so sometime after TPUs went from an FPGA project to a bit more than half of all the cycles spent by all of google, he left to form groq. that was a bit over 5 years ago. |
| 2022-07-12 09:46:51 +0200 | <edwardk> | i'm here because i happen to strongly believe that i want a large SIMD-like execution core for many problems of interest to me. and Groq is the only chip in the AI accelerator space taking the massive single core SIMD strategy. |
| 2022-07-12 09:47:17 +0200 | <Axman6> | So when you say SIMD, how wide are we talking? |
| 2022-07-12 09:47:46 +0200 | <Axman6> | (I'm watching your first video at the same time, and just got to the "what it actually looks like" but) |
| 2022-07-12 09:48:20 +0200 | <edwardk> | we use a 320 _byte_ wide SIMD unit, and can pipeline and retire 4 320x320 matrix-vector multiplies, every clock. |
| 2022-07-12 09:48:31 +0200 | <edwardk> | per chip |
| 2022-07-12 09:48:45 +0200 | <Axman6> | that's... quite a lot |
| 2022-07-12 09:48:56 +0200 | <edwardk> | the v1 chip was the first single core chip to do a petaflop |
| 2022-07-12 09:48:58 +0200 | <Axman6> | what's the latency? |
| 2022-07-12 09:49:02 +0200 | <tomsmeding> | uint8 matrices? |
| 2022-07-12 09:49:06 +0200 | <Axman6> | wow, ok then |
| 2022-07-12 09:49:09 +0200 | <edwardk> | (technically we're a bit lower than a petaflop in practice) |
| 2022-07-12 09:49:20 +0200 | <edwardk> | like 750 TFLOPs for the parts we typically sell |
| 2022-07-12 09:49:37 +0200 | <edwardk> | tomsmeding: yeah, we can do a bit lower fp16 with "truepoint" |
| 2022-07-12 09:49:50 +0200 | <edwardk> | but int8 (on v1) is our workhorse |
| 2022-07-12 09:50:01 +0200 | <tomsmeding> | Just like the tpus |
| 2022-07-12 09:50:13 +0200 | <tomsmeding> | edwardk: is the egg paper a good read? |
| 2022-07-12 09:50:41 +0200 | <edwardk> | truepoint is a bit differentiated with respect to TPUs, basically we do FP16 but with _no_ intermediate rounding error. |
| 2022-07-12 09:51:19 +0200 | <edwardk> | tomsmeding: i think the egg writeup is good, but i think it is better if you've watched the old equality saturation talk from ross tate first, which is very short and is a compelling intro to the problem |
| 2022-07-12 09:51:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 09:51:47 +0200 | <Axman6> | in ML, is int8 really just a fixed point type? or used to represent valued between zero and one? |
| 2022-07-12 09:51:51 +0200 | <edwardk> | https://www.youtube.com/watch?v=hL2MARuBCzw |
| 2022-07-12 09:52:07 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 2022-07-12 09:52:51 +0200 | <edwardk> | Axman6: typically what you'd do in ML is train with bigger floats, then take your model and quantize it down to int8 by doing a scaling pass before the layers using post-training quantization or quantization-aware training to get your accuracy back |
| 2022-07-12 09:53:37 +0200 | <edwardk> | there's a pretty healthy ecosystem around int8 training today because its the workhorse for both the tpu side and the nvidia side |
| 2022-07-12 09:53:43 +0200 | <tomsmeding> | edwardk: I've read this blog post first https://blog.sigplan.org/2021/04/06/equality-saturation-with-egg/ |
| 2022-07-12 09:54:11 +0200 | yauhsien | (~yauhsien@61-231-21-122.dynamic-ip.hinet.net) |
| 2022-07-12 09:54:18 +0200 | <tomsmeding> | But thanks! |
| 2022-07-12 09:54:44 +0200 | <edwardk> | tomsmeding: basically i've been a huge proponent of equality saturation since tate's original presentation. (i used to use RETE to pull it off), egg changed the asymptotics around in a practical way that made it _way_ easier to implement |
| 2022-07-12 09:55:02 +0200 | <edwardk> | and practically improved it from a theoretical toy to a day-to-day workhorse |
| 2022-07-12 09:55:22 +0200 | <tomsmeding> | I know very little about this space, so I'm interested |
| 2022-07-12 09:55:35 +0200 | <tomsmeding> | Will look at the paper a bit |
| 2022-07-12 09:55:36 +0200 | <edwardk> | one of my goals over the next year or so it to start using it much more aggressively inside of groq |
| 2022-07-12 09:55:57 +0200 | <edwardk> | we use it today for post-training quantization and quantization-aware training, rewriting ONNX models into better models |
| 2022-07-12 09:56:02 +0200 | <tomsmeding> | Your problems making a nice haskell interface were around internal mutation, I expect? |
| 2022-07-12 09:56:05 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2022-07-12 09:56:17 +0200 | <edwardk> | ddarius implemented that stuff for us in a shockingly compact amount of rust, like 200 lines. |
| 2022-07-12 09:56:37 +0200 | <edwardk> | yeah. i want e-nodes to be a nice haskell type with hashconsing and i can have that. |
| 2022-07-12 09:56:40 +0200 | kuribas | (~user@silversquare.silversquare.eu) |
| 2022-07-12 09:57:08 +0200 | <edwardk> | but the egg notion of rebuilding the egraph would morally change the hash codes of all the e-nodes in the graph, because each e-class gets the hash code of its root e-node |
| 2022-07-12 09:57:44 +0200 | <edwardk> | so i have to choose between doing evil mutable things (and breaking), not having expressive enough types, having too much memory utilization, or having a hard to use api |
| 2022-07-12 09:57:55 +0200 | <edwardk> | and i'm trying to thread the needle between all those different concerns |
| 2022-07-12 09:59:07 +0200 | <edwardk> | what i'd like is that the user inserts things into the graph by just working with syntax-tree like constructions, asserts them into the graph, and then i give them some template-haskell like splices to describe the matching behaviors |
| 2022-07-12 09:59:31 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2022-07-12 09:59:55 +0200 | jpds1 | (~jpds@gateway/tor-sasl/jpds) |
| 2022-07-12 10:00:25 +0200 | <edwardk> | basically i'd like to have the hash-consing behavior handled by something like the Merkle construction i give in https://github.com/ekmett/keep |
| 2022-07-12 10:00:33 +0200 | <edwardk> | but without the redis weirdness |
| 2022-07-12 10:02:37 +0200 | <edwardk> | my current approach involves building up a big messy hash table full of heterogeneous types for hash consing, using finalizers to strip things out from user-facing roots so that hash consing cleans itself up, but then needing to migrate from one cache to another to rebuild, and having the ability to ask if an AST node is present in a given egraph and/or assert it into the egraph getting a new node out |
| 2022-07-12 10:03:20 +0200 | <edwardk> | since i use stablenames as the identities in the egraph it comes down to inserting it into one hashtable by structural hashconsing key and another by stablename |
| 2022-07-12 10:04:18 +0200 | <edwardk> | and when you go to look for a key in the egraph, you check if the stablename is present and if so you're done, otherwise recurse into the syntactic subterms, until you find something that is present and built up from there asserting as you go |
| 2022-07-12 10:04:32 +0200 | <edwardk> | that way i can keep most of the subterm sharing across egraphs |
| 2022-07-12 10:04:56 +0200 | <edwardk> | and even keep the larger stablenames since the stablename for the term would remain er.. stable |
| 2022-07-12 10:05:20 +0200 | hsman | (~hsman@80.95.197.227) |
| 2022-07-12 10:05:28 +0200 | <edwardk> | so when i migrate from one egraph to the rebuilt one, only terms that actually had their contents changed would actually change and have to be rebuilt |
| 2022-07-12 10:05:39 +0200 | <edwardk> | the others would port over as the existing object |
| 2022-07-12 10:05:52 +0200 | <edwardk> | not sure how articulate that was |
| 2022-07-12 10:07:50 +0200 | <edwardk> | the thing i'm really trying to figure out is the right way to manipulate these from generation to generation, it feels like there's two options, one is you can just assert things into the egraph, and that does lots of unions on union-find structures for each match you find, just dump more data in, then fix up congruence closure on the backswing, which is the egg story. another story involves staging all that up front, which is |
| 2022-07-12 10:07:50 +0200 | <edwardk> | objectively worse. |
| 2022-07-12 10:08:07 +0200 | <edwardk> | where what you do is gather all the changes you want to make, then make them all at once. |
| 2022-07-12 10:08:36 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 10:08:54 +0200 | <edwardk> | the egg-like "mutably change things in place in ways that are visible to subsequent matches but congruence closure isn't yet satisified until you rebuild" story matches onto something like gauss-seidel iteration for me. you can see part way into the current step. |
| 2022-07-12 10:09:44 +0200 | <tomsmeding> | I don't know enough of egraphs yet to say something useful about the tradeoffs involved |
| 2022-07-12 10:09:59 +0200 | <tomsmeding> | But yeah this sounds non-trivial, in api design |
| 2022-07-12 10:10:06 +0200 | <edwardk> | and in practice Gauss-Seidel is faster than a more deterministic Jacobi method for iteratively solving constraints, even if the result is a lot more dependent on the order of constraints |
| 2022-07-12 10:10:11 +0200 | <turlando> | Noob question (I guess): I have the following function «exponential g lambda = (\x -> - log x / lambda) <$> (uniformFloatPositive01M g)» with signature «exponential :: StatefulGen g m => g -> Float -> m Float». From the REPL I do «g = mkStdGen 23» and then «exponential g 0.1», but I get «No instance for (StatefulGen System.Random.Internal.StdGen m0) arising from a use of ‘it’». What am I missing? |
| 2022-07-12 10:10:12 +0200 | hsman | (~hsman@80.95.197.227) (Ping timeout: 252 seconds) |
| 2022-07-12 10:10:47 +0200 | <edwardk> | here ideally your matches are deterministic in that if you iterate this process to a fixed point you get the same graph, but that is an emergent phenomenon of how you _use_ egg, rather than a property of egg itself. |
| 2022-07-12 10:11:19 +0200 | <tomsmeding> | edwardk: there is no theoretical guarantee that you do end up in a fixpoint, right? |
| 2022-07-12 10:11:41 +0200 | <tomsmeding> | turlando: what would you expect that m to be instantiated to? |
| 2022-07-12 10:11:44 +0200 | chele | (~chele@user/chele) |
| 2022-07-12 10:12:27 +0200 | <edwardk> | tomsmeding: well, this comes down to whether your rewrite rules are 'nice' in some sense. you can come up with lots of classes of them that will hit that guarantee, lots of sufficient conditions, few descriptions of necessary ones |
| 2022-07-12 10:12:28 +0200 | <turlando> | tomsmeding: Not sure actually. I guess it should be the context of the RNG? |
| 2022-07-12 10:12:44 +0200 | <tomsmeding> | edwardk: I see, makes sense |
| 2022-07-12 10:12:58 +0200 | <tomsmeding> | turlando: if you don't know, how is ghc supposed to know? :P |
| 2022-07-12 10:13:04 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 10:13:11 +0200 | <turlando> | Good point |
| 2022-07-12 10:13:16 +0200 | <tomsmeding> | That's the error -- ghc has no clue what to instantiate m with |
| 2022-07-12 10:13:35 +0200 | <edwardk> | usually you'd use some kind of runFoo function to pick the right m. |
| 2022-07-12 10:13:43 +0200 | <turlando> | Maybe I don't need an m at all? It's the first time I'm using System.Random |
| 2022-07-12 10:14:52 +0200 | <tomsmeding> | turlando: I suggest you use System.Random first, before going to System.Random.Stateful |
| 2022-07-12 10:15:29 +0200 | <turlando> | I will, thanks for the suggestion |
| 2022-07-12 10:15:31 +0200 | <edwardk> | there's a bunch of monad transformers in there for different ways to plumb around the StdGen |
| 2022-07-12 10:16:05 +0200 | <edwardk> | carrying it in a shared atomic, in a ReaderT style IORef, etc. |
| 2022-07-12 10:16:10 +0200 | <turlando> | I still feel pretty unfomfortable when moving into the monad transformer territory |
| 2022-07-12 10:16:24 +0200 | <edwardk> | StateGenM, AtomicGenM, IOGenM, STGenM and TGenM |
| 2022-07-12 10:16:49 +0200 | <tomsmeding> | turlando: just put the StdGen in a state monad or however you want to pass it around, and use the uniform* family of functions |
| 2022-07-12 10:16:56 +0200 | <tomsmeding> | Works fine, no monad transformers required |
| 2022-07-12 10:17:08 +0200 | <edwardk> | then i'd go down to the basic System.Random machinery for now and ignore the monad transformers that exposes |
| 2022-07-12 10:17:12 +0200 | <tomsmeding> | You can always decide later to go to the stateful version |
| 2022-07-12 10:17:17 +0200 | <edwardk> | +1 |
| 2022-07-12 10:18:25 +0200 | <turlando> | Thanks again for the suggestions, I will try |
| 2022-07-12 10:19:25 +0200 | ccntrq | (~Thunderbi@2a01:c23:8c77:3a00:6188:64f1:5d2d:a884) |
| 2022-07-12 10:23:46 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) |
| 2022-07-12 10:26:51 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-07-12 10:27:04 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 10:27:55 +0200 | <edwardk> | i do want to say one nice thing about the hashconsing story is that you can really quickly compute catamorphisms over them. just build the memotable of the hashes you've seen so far, since everything is well-founded this terminates and gets to use a nice memoization scheme |
| 2022-07-12 10:28:14 +0200 | <edwardk> | and you can keep the memotable for subsequent invocations later on |
| 2022-07-12 10:28:32 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2022-07-12 10:28:53 +0200 | hsman | (~hsman@80.95.197.227) |
| 2022-07-12 10:29:39 +0200 | <edwardk> | this is basically the e-analysis pass for egg, or the same kind of idea as is used by lean to perform folds over hashconsed trees |
| 2022-07-12 10:30:02 +0200 | <edwardk> | but holy hell is it a booster shot in the arm for performance for a lot of passes |
| 2022-07-12 10:31:25 +0200 | <edwardk> | i'd like to get to where i can use it with something like https://www.schoolofhaskell.com/user/edwardk/conquering-folds |
| 2022-07-12 10:38:10 +0200 | <schweers> | I have a problem with Conduit and the types () and Void. When I try to pass a value of type ConduitT () () IO () to runConduit (which has type Monad m => ConduitT () Void m r -> m r) I get an error about () and Data.Void.Void not matching. Am I missing something obvious? |
| 2022-07-12 10:45:11 +0200 | <[exa]> | schweers: how did you create the value of type ConduitT () () IO () ? |
| 2022-07-12 10:46:11 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Read error: Connection reset by peer) |
| 2022-07-12 10:47:04 +0200 | vglfr | (~vglfr@88.155.25.62) |
| 2022-07-12 10:47:06 +0200 | Vajb | (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) |
| 2022-07-12 10:47:32 +0200 | <schweers> | I used yield and chained the result with other ConduitT values. I also tried using something different, but it seems no matter what I do, it always comes back to this same problem. |
| 2022-07-12 10:48:13 +0200 | <schweers> | The weird thing is that I use runConduit somewhere else and that works just fine. There the last part of the pipeline is sinkHandle. |
| 2022-07-12 10:48:14 +0200 | Vajb | (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 2022-07-12 10:48:39 +0200 | Vajb | (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) |
| 2022-07-12 10:53:13 +0200 | <schweers> | To give some more details: the function I’m working on takes (among other arguments) a value of type ConduitT () T.Text IO (). This is then chained with a function from the csv-conduit package and a ConduitT of my own to insert csv rows into a database. Said last ConduitT is of type ConduitT (Row T.Text) () IO (). |
| 2022-07-12 10:53:19 +0200 | <schweers> | [exa]: ^ |
| 2022-07-12 10:53:44 +0200 | doomfume[m] | (~doomfumeh@2001:470:69fc:105::2:2a62) (Quit: You have been kicked for being idle) |
| 2022-07-12 10:53:44 +0200 | doomfume[m]1 | (~doomfumem@2001:470:69fc:105::2:2a64) (Quit: You have been kicked for being idle) |
| 2022-07-12 10:57:43 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 2022-07-12 11:02:09 +0200 | <[exa]> | schweers: I only used that thing once but it looks like it requires you to explicitly say there's a sink at the end of the pipeline |
| 2022-07-12 11:02:15 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-07-12 11:06:29 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2022-07-12 11:06:45 +0200 | img | (~img@user/img) |
| 2022-07-12 11:09:38 +0200 | <[exa]> | schweers: yeah it seems like your type should not specify the output (), instead allow anything in there (just like the type of sinkHandle) |
| 2022-07-12 11:09:58 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 2022-07-12 11:10:37 +0200 | Cajun | (~Cajun@user/cajun) (Quit: Client closed) |
| 2022-07-12 11:12:17 +0200 | <schweers> | [exa]: hmm, that might be the case. Thanks for the pointer, I’ll see what I can find. |
| 2022-07-12 11:13:44 +0200 | maroloccio | (~marolocci@151.73.134.175) |
| 2022-07-12 11:13:55 +0200 | <[exa]> | what's the last thing in the problematic conduit here? |
| 2022-07-12 11:14:22 +0200 | hsman | (~hsman@80.95.197.227) (Ping timeout: 252 seconds) |
| 2022-07-12 11:16:04 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 2022-07-12 11:20:28 +0200 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2022-07-12 11:23:05 +0200 | <schweers> | The last is one I’ve written myself. The goal is to consume the first element of its input stream to create a table in a database, then consume each following element and issue insert statements. As I’m not at all experienced with Conduit I might as well made some mistakes there. |
| 2022-07-12 11:24:08 +0200 | shriekingnoise_ | (~shrieking@201.212.175.181) (Quit: Quit) |
| 2022-07-12 11:24:36 +0200 | <schweers> | https://pastebin.com/qwe8ag93 |
| 2022-07-12 11:28:13 +0200 | <[exa]> | schweers: what happens if you replace the first () on line 20 with `a` ? |
| 2022-07-12 11:28:41 +0200 | <[exa]> | I see no output -> no reason to push () |
| 2022-07-12 11:29:16 +0200 | JSharp | (sid4580@id-4580.lymington.irccloud.com) () |
| 2022-07-12 11:29:41 +0200 | JSharp | (sid4580@id-4580.lymington.irccloud.com) |
| 2022-07-12 11:29:44 +0200 | <schweers> | Couldn't match type ‘a1’ with ‘()’ |
| 2022-07-12 11:30:03 +0200 | <schweers> | and that a1 is a rigid type variable bound by the signature for processRows. |
| 2022-07-12 11:30:22 +0200 | <schweers> | So I get an additional compiler error |
| 2022-07-12 11:31:24 +0200 | jmorris | (uid537181@id-537181.uxbridge.irccloud.com) |
| 2022-07-12 11:31:48 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 11:35:12 +0200 | mmhat | (~mmh@p200300f1c7090723ee086bfffe095315.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2022-07-12 11:37:08 +0200 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2022-07-12 11:43:27 +0200 | <[exa]> | ah maybe the `pipeline` shouldn't get () too |
| 2022-07-12 11:43:34 +0200 | <[exa]> | (line 28) |
| 2022-07-12 11:44:22 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 11:46:15 +0200 | phma | (phma@2001:5b0:215d:e008:5054:f1a6:ecb8:df53) (Read error: Connection reset by peer) |
| 2022-07-12 11:47:11 +0200 | phma | (~phma@host-67-44-208-203.hnremote.net) |
| 2022-07-12 11:48:38 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 11:49:38 +0200 | mmhat | (~mmh@p200300f1c7090757ee086bfffe095315.dip0.t-ipconnect.de) |
| 2022-07-12 11:51:17 +0200 | <schweers> | [exa]: I’m afraid that doesn’t fix it. I have to leave for now, I’ll hopefully be back in about an hour. Thank you so far for your help! |
| 2022-07-12 11:52:41 +0200 | __monty__ | (~toonn@user/toonn) |
| 2022-07-12 11:59:39 +0200 | <kuribas> | edwardk: are you writing a egraph library for haskell? |
| 2022-07-12 11:59:58 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 12:01:51 +0200 | dschrempf | (~dominik@mobiledyn-62-240-134-33.mrsn.at) |
| 2022-07-12 12:02:14 +0200 | dschrempf | (~dominik@mobiledyn-62-240-134-33.mrsn.at) (Client Quit) |
| 2022-07-12 12:10:28 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 12:15:25 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 2022-07-12 12:16:15 +0200 | <gurkenglas> | *googles egraph* kuribas: why not just store a function from the type on which you wish to define an equivalence relation to the set of equivalence classes? |
| 2022-07-12 12:16:53 +0200 | biberu\ | (~biberu@user/biberu) |
| 2022-07-12 12:17:33 +0200 | biberu | (~biberu@user/biberu) (Ping timeout: 256 seconds) |
| 2022-07-12 12:18:29 +0200 | biberu\ | biberu |
| 2022-07-12 12:18:33 +0200 | notzmv | (~zmv@user/notzmv) (Ping timeout: 276 seconds) |
| 2022-07-12 12:19:30 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 240 seconds) |
| 2022-07-12 12:20:18 +0200 | <gurkenglas> | ...oh i guess because you want a fast preimage operation. though i suspect that in many cases you don't actually need that |
| 2022-07-12 12:24:23 +0200 | <gurkenglas> | *actually reads wikipedia article* are you hoping to use it for an automated theorem prover or compiler? :) |
| 2022-07-12 12:27:48 +0200 | Guest45 | (~Guest45@bras-base-okvlon5405w-grc-53-70-30-46-127.dsl.bell.ca) (Quit: Client closed) |
| 2022-07-12 12:28:26 +0200 | Lears | (~Leary]@122-58-224-198-vdsl.sparkbb.co.nz) (Ping timeout: 255 seconds) |
| 2022-07-12 12:28:53 +0200 | <gurkenglas> | though i suppose the library also generally deserves to exist - in a sense every time you store a function, the structure of an egraph ought to be in easy reach |
| 2022-07-12 12:35:18 +0200 | <gurkenglas> | Does an egraph provide *all* the operations one can reasonably provide for a stored function? |
| 2022-07-12 12:36:17 +0200 | PiDelport | (uid25146@id-25146.lymington.irccloud.com) |
| 2022-07-12 12:47:52 +0200 | wenjie | (~nut@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) (Quit: WeeChat 3.5) |
| 2022-07-12 12:55:08 +0200 | CiaoSen | (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) |
| 2022-07-12 12:58:39 +0200 | <radhika> | Hi.. I get error messages like “ No instance for (Num String) arising from use of ‘+’ in expression …. In an equation for … |
| 2022-07-12 12:58:57 +0200 | <radhika> | What does “instance “ mean in all these messages? |
| 2022-07-12 12:59:16 +0200 | <radhika> | Also what is “it” refer to? |
| 2022-07-12 12:59:19 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) |
| 2022-07-12 12:59:34 +0200 | <radhika> | What does “it” refer to?? |
| 2022-07-12 13:04:33 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 13:05:47 +0200 | CiaoSen | (~Jura@p200300c9570ffb002a3a4dfffe84dbd5.dip0.t-ipconnect.de) (Quit: CiaoSen) |
| 2022-07-12 13:06:22 +0200 | xff0x | (~xff0x@2405:6580:b080:900:9e06:cb70:78ee:9dbc) |
| 2022-07-12 13:06:57 +0200 | <[exa]> | radhika: you probably tried to add a String to something? |
| 2022-07-12 13:07:28 +0200 | <[exa]> | radhika: "No instance for (Constraint Type) ..." means basically "I don't know how Type can satisfy a Constraint" |
| 2022-07-12 13:07:52 +0200 | <[exa]> | in your case, the compiler tells you that it doesn't know how to make String a numeric object (in class Num) |
| 2022-07-12 13:08:10 +0200 | <[exa]> | (btw strings are concatenated with ++, if that helps) |
| 2022-07-12 13:09:27 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2022-07-12 13:09:28 +0200 | allbery_b | (~geekosaur@xmonad/geekosaur) |
| 2022-07-12 13:09:31 +0200 | allbery_b | geekosaur |
| 2022-07-12 13:13:38 +0200 | <[exa]> | and re "instance", instance is a part of the typeclass construction. You declare typeclasses (e.g., Num for all numeric things or Ord for all stuff that can be ordered, i.e. has < ), then you add instances of the types that actually fit into the classes (i.e., you write a Num instance for Int and Float and Complex, and Ord instance for Int and Float and Char), and then you can enjoy the typeclass |
| 2022-07-12 13:13:44 +0200 | <[exa]> | polymorphism and the nice overloading. |
| 2022-07-12 13:15:01 +0200 | frost | (~frost@user/frost) (Quit: Client closed) |
| 2022-07-12 13:16:44 +0200 | frost | (~frost@user/frost) |
| 2022-07-12 13:17:53 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-07-12 13:21:49 +0200 | Philonous_ | (~Philonous@user/philonous) (Quit: ZNC - https://znc.in) |
| 2022-07-12 13:22:19 +0200 | Philonous | (~Philonous@user/philonous) |
| 2022-07-12 13:23:12 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) (Ping timeout: 244 seconds) |
| 2022-07-12 13:23:14 +0200 | mc47 | (~mc47@xmonad/TheMC47) (Remote host closed the connection) |
| 2022-07-12 13:23:32 +0200 | frost | (~frost@user/frost) (Quit: Client closed) |
| 2022-07-12 13:31:31 +0200 | AlexZenon | (~alzenon@178.34.160.206) (Quit: ;-) |
| 2022-07-12 13:31:56 +0200 | Alex_test | (~al_test@178.34.160.206) (Quit: ;-) |
| 2022-07-12 13:32:14 +0200 | AlexNoo | (~AlexNoo@178.34.160.206) (Quit: Leaving) |
| 2022-07-12 13:34:52 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 13:38:22 +0200 | <schweers> | [exa]: I’m not sure that it really solves my problem, as my tests fail, but changing runConduit pipeline to runConduit $ pipeline .| sinkNull at least makes the compiler happy. |
| 2022-07-12 13:39:34 +0200 | kjak | (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) |
| 2022-07-12 13:39:54 +0200 | <[exa]> | yes, that makes sense. The last thing in your pipeline isn't a proper Sink (it produces ()'s), so it can't be run. |
| 2022-07-12 13:40:56 +0200 | <[exa]> | what was the error when you fix the type annotations to have `a` in output instead of ()? |
| 2022-07-12 13:41:29 +0200 | bontaq | (~user@ool-45779fe5.dyn.optonline.net) |
| 2022-07-12 13:41:43 +0200 | <[exa]> | (also not sure if it wouldn't be better to move them into toplevel definitions -- there may be a very undesirable interplay of typesystem features in local scopes) |
| 2022-07-12 13:43:41 +0200 | <kuribas> | gurkenglas: I was just exploring the page, I haven't even thought of usecases :) |
| 2022-07-12 13:43:50 +0200 | <schweers> | You mean changing the type of pipeline to ConduitT a b IO ()? |
| 2022-07-12 13:44:04 +0200 | <kuribas> | gurkenglas: but the given applications look pretty cool, like improving herbie performance for example. |
| 2022-07-12 13:44:11 +0200 | <schweers> | That gives me • Couldn't match type ‘a1’ with ‘()’ |
| 2022-07-12 13:44:49 +0200 | <[exa]> | rather `ConduitT () a IO ()` |
| 2022-07-12 13:45:26 +0200 | <[exa]> | looks to me like the input is set by the type you get with csvInput |
| 2022-07-12 13:47:02 +0200 | AlexNoo | (~AlexNoo@178.34.160.206) |
| 2022-07-12 13:47:12 +0200 | AlexZenon | (~alzenon@178.34.160.206) |
| 2022-07-12 13:49:19 +0200 | <schweers> | `ConduitT () a IO ()` gives me the same error. |
| 2022-07-12 13:50:38 +0200 | Alex_test | (~al_test@178.34.160.206) |
| 2022-07-12 13:53:54 +0200 | <[exa]> | in both changed places? |
| 2022-07-12 13:54:08 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) (Ping timeout: 260 seconds) |
| 2022-07-12 13:54:16 +0200 | hsman | (~hsman@80.95.197.227) |
| 2022-07-12 13:55:57 +0200 | <schweers> | Unless I’m completely missing something, then yes. |
| 2022-07-12 13:58:02 +0200 | <[exa]> | that's weird because it should be okay-ish in one of the places because the outputs changed together |
| 2022-07-12 13:58:20 +0200 | kimjetwav | (~user@2607:fea8:2340:fe00:730c:be2f:be5e:3847) (Ping timeout: 244 seconds) |
| 2022-07-12 13:58:26 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) (Ping timeout: 255 seconds) |
| 2022-07-12 13:59:49 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 2022-07-12 14:02:21 +0200 | [Leary] | (~Leary]@122-58-224-198-vdsl.sparkbb.co.nz) |
| 2022-07-12 14:02:48 +0200 | <[exa]> | can you paste your error after changing l20 to `ConduitT (Row T.Text) o IO ()` and l28 to `...::ConduitT () o IO ()` ? (Also, you don't have any extensions like ScopedAnything enabled, right?) |
| 2022-07-12 14:06:15 +0200 | hsman | (~hsman@80.95.197.227) (Quit: Client closed) |
| 2022-07-12 14:08:08 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 260 seconds) |
| 2022-07-12 14:12:38 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 14:17:39 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 2022-07-12 14:17:52 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) |
| 2022-07-12 14:26:10 +0200 | notzmv | (~zmv@user/notzmv) |
| 2022-07-12 14:34:49 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2022-07-12 14:35:06 +0200 | <radhika> | [exa]: thanks.. my apologies for the delayed reply.. we had a power outage.. |
| 2022-07-12 14:35:42 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 276 seconds) |
| 2022-07-12 14:38:33 +0200 | hsman | (~hsman@80.95.197.227) |
| 2022-07-12 14:39:20 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-07-12 14:40:31 +0200 | {-d0t-} | (~q_q@user/-d0t-/x-7915216) |
| 2022-07-12 14:40:57 +0200 | <{-d0t-}> | hello! What is the easiest way to log both request and reply in a WAI app? |
| 2022-07-12 14:44:02 +0200 | <[exa]> | radhika: np, take care. :D |
| 2022-07-12 14:45:56 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-07-12 14:46:37 +0200 | jao | (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2022-07-12 14:47:37 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 14:48:40 +0200 | <[exa]> | {-d0t-}: you can log the request simply by showing the input of your Application or Middleware. For logging responses you need to stash something to the parameter of Application. I'd just smash traceShow in there. :] |
| 2022-07-12 14:49:40 +0200 | <{-d0t-}> | [exa]: the thing is, I want to log them as a single string and send that to Grafana |
| 2022-07-12 14:50:32 +0200 | <[exa]> | ah so. That might require some slightly more advanced Middleware but I guess it will still be representable as a Middleware |
| 2022-07-12 14:50:44 +0200 | <{-d0t-}> | [exa]: for requests, Warp accepts a logger parameter via Settings, but it only logs response code and not any other part. |
| 2022-07-12 14:51:53 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2022-07-12 14:52:21 +0200 | <[exa]> | like: withLogs :: Middleware; withLogs app req respond = do { logRequest req; app (\x -> logResponse x >> respond x) } |
| 2022-07-12 14:52:34 +0200 | <[exa]> | logRequest and logResponse can do IO so you should be able to send it there |
| 2022-07-12 14:53:05 +0200 | <[exa]> | uh wait you want to catch the response data, which are not in ResponseReceived |
| 2022-07-12 14:53:16 +0200 | <{-d0t-}> | Yeah, that :( |
| 2022-07-12 14:53:40 +0200 | <{-d0t-}> | https://hackage.haskell.org/package/wai-log-0.2.0.0/docs/Network-Wai-Log.html |
| 2022-07-12 14:53:45 +0200 | <[exa]> | that's generally impossible with WAI because response gets streamed out right at the point it's available |
| 2022-07-12 14:53:50 +0200 | <{-d0t-}> | This seems like something I c)ould use |
| 2022-07-12 14:54:09 +0200 | <[exa]> | but yeah this seems to connect to the right bits |
| 2022-07-12 14:54:17 +0200 | <{-d0t-}> | [exa]: what if I force evaluate it to some buffer? |
| 2022-07-12 14:54:44 +0200 | <{-d0t-}> | This seems like an thing that would be obvious and shouldn't be hard to impelement, hence I'm a bit puzzled |
| 2022-07-12 14:55:34 +0200 | <[exa]> | ah wait no I confused myself |
| 2022-07-12 14:55:47 +0200 | <[exa]> | Response is perfectly okay and loggable. :D |
| 2022-07-12 14:56:05 +0200 | <[exa]> | if you dig into the source in the Log there, they do more or less the same thing as `withLogs` above |
| 2022-07-12 14:56:31 +0200 | <[exa]> | here https://hackage.haskell.org/package/wai-log-0.2.0.0/docs/src/Network.Wai.Log.Internal.html#logRequ… |
| 2022-07-12 14:56:51 +0200 | AlexZenon | (~alzenon@178.34.160.206) (Quit: ;-) |
| 2022-07-12 14:57:12 +0200 | <{-d0t-}> | oh cool cool! Then this is about what I need. |
| 2022-07-12 14:57:14 +0200 | <{-d0t-}> | Thanks! |
| 2022-07-12 14:57:14 +0200 | Alex_test | (~al_test@178.34.160.206) (Quit: ;-) |
| 2022-07-12 14:58:25 +0200 | <[exa]> | the "Source" links on hackage are magick |
| 2022-07-12 14:59:45 +0200 | <{-d0t-}> | indeed they are! |
| 2022-07-12 15:00:03 +0200 | AlexNoo | (~AlexNoo@178.34.160.206) (Quit: Leaving) |
| 2022-07-12 15:00:33 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) |
| 2022-07-12 15:02:52 +0200 | dknite | (~dknite@49.37.45.188) (Read error: Connection reset by peer) |
| 2022-07-12 15:05:27 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 268 seconds) |
| 2022-07-12 15:06:12 +0200 | frost | (~frost@user/frost) |
| 2022-07-12 15:07:00 +0200 | AlexNoo | (~AlexNoo@178.34.160.206) |
| 2022-07-12 15:07:03 +0200 | Pickchea | (~private@user/pickchea) (Ping timeout: 272 seconds) |
| 2022-07-12 15:07:03 +0200 | AlexZenon | (~alzenon@178.34.160.206) |
| 2022-07-12 15:07:37 +0200 | <gurkenglas> | kuribas: exploring what page? |
| 2022-07-12 15:07:57 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 15:08:06 +0200 | <kuribas> | gurkenglas: https://egraphs-good.github.io/ |
| 2022-07-12 15:09:25 +0200 | Alex_test | (~al_test@178.34.160.206) |
| 2022-07-12 15:11:28 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 2022-07-12 15:12:27 +0200 | pmarg | (~pmarg@2a01:799:159f:9b00:692:26ff:fec4:d342) |
| 2022-07-12 15:12:31 +0200 | Fxmuhrwawz | (~Fxmuhrwaw@191-214-26-24.user.veloxzone.com.br) |
| 2022-07-12 15:13:31 +0200 | <gurkenglas> | ...I badly misunderstood e-graphs. I thought it stores an equivalence relation over nodes of the graph. |
| 2022-07-12 15:16:20 +0200 | k60`` | (~user@94.25.174.91) (Ping timeout: 244 seconds) |
| 2022-07-12 15:17:47 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-07-12 15:17:53 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 15:18:47 +0200 | Fxmuhrwawz | (~Fxmuhrwaw@191-214-26-24.user.veloxzone.com.br) (Remote host closed the connection) |
| 2022-07-12 15:19:56 +0200 | jpds1 | jpds |
| 2022-07-12 15:22:52 +0200 | ubert1 | (~Thunderbi@91.141.39.36.wireless.dyn.drei.com) |
| 2022-07-12 15:24:34 +0200 | ubert | (~Thunderbi@178.165.177.173.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 2022-07-12 15:24:34 +0200 | ubert1 | ubert |
| 2022-07-12 15:27:26 +0200 | <shapr> | gurkenglas: what does it actually do? |
| 2022-07-12 15:28:22 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-07-12 15:28:52 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 15:29:55 +0200 | <gurkenglas> | Stores an equivalence relation over terms of a language. Which happens to be an equivalence relation over nodes of a graph, but that's not the point. I thought it was just supposed to take an arbitrary equivalence relation on a set, then use a graph to efficiently allow operations you might want to do to such a relation. |
| 2022-07-12 15:31:26 +0200 | <gurkenglas> | (and "arbitrary equivalent relation on a set" is in a sense another word for "function", which is why that seemed general enough to deserve a library) |
| 2022-07-12 15:31:44 +0200 | <gurkenglas> | s/equivalent/equivalence/ |
| 2022-07-12 15:33:23 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 15:35:14 +0200 | shapr | tries to understand the difference |
| 2022-07-12 15:35:22 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2022-07-12 15:36:02 +0200 | shapr | reads the tutorial |
| 2022-07-12 15:39:17 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 2022-07-12 15:41:55 +0200 | <edwardk> | kuribas: i was writing some code that wanted to use egraphs, and was debating about ways to get it to be nice, one way would be to turn it into a library, yes |
| 2022-07-12 15:42:32 +0200 | <kuribas> | +1 to make it into a library :) |
| 2022-07-12 15:42:52 +0200 | brettgilio5 | brettgilio |
| 2022-07-12 15:42:59 +0200 | kuribas | wonders if you can ffi into rust... |
| 2022-07-12 15:43:28 +0200 | <shapr> | I thought there was an inline-rust package at some point |
| 2022-07-12 15:44:18 +0200 | <shapr> | https://github.com/harpocrates/inline-rust ? |
| 2022-07-12 15:45:19 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 15:46:16 +0200 | <shapr> | this is an interesting read: https://docs.rs/egg/0.9.0/egg/tutorials/ |
| 2022-07-12 15:46:19 +0200 | {-d0t-} | (~q_q@user/-d0t-/x-7915216) (Ping timeout: 272 seconds) |
| 2022-07-12 15:48:37 +0200 | acidjnk | (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2022-07-12 15:49:36 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2022-07-12 15:50:25 +0200 | {-d0t-} | (~q_q@user/-d0t-/x-7915216) |
| 2022-07-12 15:53:22 +0200 | <tomsmeding> | shapr: I found this to be a good intro as well https://blog.sigplan.org/2021/04/06/equality-saturation-with-egg/ |
| 2022-07-12 15:53:33 +0200 | <shapr> | thanks! |
| 2022-07-12 15:53:51 +0200 | <tomsmeding> | But maybe tutorial part 1 covers that? Not sure, I skipped part 1 after having read the blogpost |
| 2022-07-12 15:54:53 +0200 | motherfsck | (~motherfsc@user/motherfsck) (Ping timeout: 260 seconds) |
| 2022-07-12 15:57:43 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 272 seconds) |
| 2022-07-12 15:59:21 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 2022-07-12 15:59:30 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 16:01:57 +0200 | <mrianbloom> | Is it possible to make a type family that is part of a typeclass also injective? |
| 2022-07-12 16:04:03 +0200 | {-d0t-} | (~q_q@user/-d0t-/x-7915216) (Ping timeout: 272 seconds) |
| 2022-07-12 16:04:48 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2022-07-12 16:09:04 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2022-07-12 16:09:32 +0200 | frost | (~frost@user/frost) (Ping timeout: 252 seconds) |
| 2022-07-12 16:11:18 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 16:17:46 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) |
| 2022-07-12 16:19:58 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) |
| 2022-07-12 16:22:50 +0200 | toluene | (~toluene@user/toulene) (Ping timeout: 240 seconds) |
| 2022-07-12 16:23:08 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2022-07-12 16:24:28 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-07-12 16:24:51 +0200 | toluene | (~toluene@user/toulene) |
| 2022-07-12 16:30:52 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2022-07-12 16:31:18 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-07-12 16:33:47 +0200 | merijn | (~merijn@86-86-29-250.fixed.kpn.net) |
| 2022-07-12 16:37:42 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 16:39:48 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 268 seconds) |
| 2022-07-12 16:41:21 +0200 | <ski> | % class Foo a where type Bar a = r | r -> a -- mrianbloom ? |
| 2022-07-12 16:41:21 +0200 | <yahb2> | <no output> |
| 2022-07-12 16:41:36 +0200 | acidjnk | (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) |
| 2022-07-12 16:41:50 +0200 | <mrianbloom> | ski: Is wasn't sure if that syntax works? |
| 2022-07-12 16:42:08 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2022-07-12 16:43:51 +0200 | <mrianbloom> | Ah, I think it does. You just need TypeFamilyDependencies enabled. |
| 2022-07-12 16:43:57 +0200 | <mrianbloom> | Thank you |
| 2022-07-12 16:44:47 +0200 | indigo_ibs | (~user@31.124.106.79) |
| 2022-07-12 16:45:14 +0200 | <ski> | np |
| 2022-07-12 16:47:19 +0200 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-07-12 16:49:39 +0200 | schweers | (~user@2001:9e8:be64:4500:aaa1:59ff:fe3f:235c) (Ping timeout: 272 seconds) |
| 2022-07-12 16:50:22 +0200 | shriekingnoise | (~shrieking@201.212.175.181) |
| 2022-07-12 16:51:10 +0200 | benin09 | (~benin@156.146.51.131) |
| 2022-07-12 16:51:37 +0200 | jmorris | (uid537181@id-537181.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-07-12 16:52:04 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) (Remote host closed the connection) |
| 2022-07-12 16:52:22 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 16:52:49 +0200 | benin0 | (~benin@183.82.29.162) (Ping timeout: 272 seconds) |
| 2022-07-12 16:52:49 +0200 | benin09 | benin0 |
| 2022-07-12 16:54:28 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 2022-07-12 16:55:34 +0200 | pmarg | (~pmarg@2a01:799:159f:9b00:692:26ff:fec4:d342) (Remote host closed the connection) |
| 2022-07-12 16:59:51 +0200 | dextaa | (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 2022-07-12 17:01:51 +0200 | benin09 | (~benin@183.82.29.162) |
| 2022-07-12 17:02:05 +0200 | dextaa | (~DV@user/dextaa) |
| 2022-07-12 17:02:53 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-07-12 17:04:04 +0200 | dextaa | (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 2022-07-12 17:04:13 +0200 | benin0 | (~benin@156.146.51.131) (Ping timeout: 272 seconds) |
| 2022-07-12 17:04:13 +0200 | benin09 | benin0 |
| 2022-07-12 17:05:58 +0200 | dextaa | (~DV@user/dextaa) |
| 2022-07-12 17:06:17 +0200 | dextaa | (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 2022-07-12 17:06:53 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) |
| 2022-07-12 17:08:19 +0200 | dextaa | (~DV@user/dextaa) |
| 2022-07-12 17:08:42 +0200 | dextaa | (~DV@user/dextaa) (Read error: Connection reset by peer) |
| 2022-07-12 17:10:48 +0200 | dextaa | (~DV@user/dextaa) |
| 2022-07-12 17:12:54 +0200 | pmarg | (~pmarg@2a01:799:159f:9b00:36a6:c77c:6059:5758) |
| 2022-07-12 17:12:59 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 17:14:04 +0200 | zebrag | (~chris@user/zebrag) |
| 2022-07-12 17:15:09 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 17:18:09 +0200 | ski | (~ski@ext-1-468.eduroam.chalmers.se) (Ping timeout: 272 seconds) |
| 2022-07-12 17:20:03 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 2022-07-12 17:20:13 +0200 | maroloccio | (~marolocci@151.73.134.175) (Quit: WeeChat 3.0) |
| 2022-07-12 17:20:58 +0200 | slack1256 | (~slack1256@191.126.99.206) |
| 2022-07-12 17:24:49 +0200 | econo | (uid147250@user/econo) |
| 2022-07-12 17:27:23 +0200 | <edwardk> | kuribas: that was one thought, but i kind of want the nice haskelly version |
| 2022-07-12 17:27:45 +0200 | <edwardk> | kuribas: i will admit my maximum likelihood scenario at this moment is just going over to write the code i want in rust instead of haskell |
| 2022-07-12 17:29:15 +0200 | <edwardk> | i do wish injective type families let me say things like: type Foo x y = z | z x -> y -- having PolyKinds makes the crippled current version of injectivity really bad |
| 2022-07-12 17:31:03 +0200 | alexhandy | (~trace@user/trace) (Read error: Connection reset by peer) |
| 2022-07-12 17:31:04 +0200 | Vajb | (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) (Read error: Connection reset by peer) |
| 2022-07-12 17:31:14 +0200 | alexhandy | (~trace@user/trace) |
| 2022-07-12 17:31:57 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) |
| 2022-07-12 17:32:06 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 17:32:45 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Ping timeout: 244 seconds) |
| 2022-07-12 17:34:17 +0200 | alexhandy2 | (~trace@user/trace) |
| 2022-07-12 17:34:53 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 3.5) |
| 2022-07-12 17:35:37 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 2022-07-12 17:35:48 +0200 | alexhandy | (~trace@user/trace) (Ping timeout: 260 seconds) |
| 2022-07-12 17:36:21 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 17:41:30 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 17:46:17 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2022-07-12 17:49:03 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-07-12 17:49:49 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 272 seconds) |
| 2022-07-12 17:50:01 +0200 | jakalx | (~jakalx@base.jakalx.net) () |
| 2022-07-12 17:50:10 +0200 | <dextaa> | Can someone help me out understanding this compiler error message? https://paste.tomsmeding.com/Wae5P1sR |
| 2022-07-12 17:53:01 +0200 | <edwardk> | dextaa: guessing buildinEnv is just a value not an m (something)? |
| 2022-07-12 17:53:16 +0200 | <edwardk> | does |
| 2022-07-12 17:53:23 +0200 | <edwardk> | initInterpreterState = InterpreterState builtinEnv <$> newIORef Seq.empty |
| 2022-07-12 17:53:24 +0200 | <edwardk> | work? |
| 2022-07-12 17:53:31 +0200 | <kuribas> | dextaa: InterpreterState has only one argument? |
| 2022-07-12 17:53:43 +0200 | vglfr | (~vglfr@88.155.25.62) (Remote host closed the connection) |
| 2022-07-12 17:54:02 +0200 | <edwardk> | and if not what are the types of builtinEnv and InterpreterState ? |
| 2022-07-12 17:54:04 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-07-12 17:54:24 +0200 | <kuribas> | data InterpreterState = InterpreterState { isEnv :: Env } |
| 2022-07-12 17:54:24 +0200 | vglfr | (~vglfr@88.155.25.62) |
| 2022-07-12 17:54:34 +0200 | <kuribas> | initInterpreterState = InterpreterState <$> builtinEnv <*> newIORef Seq.empty |
| 2022-07-12 17:55:04 +0200 | <edwardk> | oh interpreterState doesn't carry around any IORef at all |
| 2022-07-12 17:55:13 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 17:55:24 +0200 | <kuribas> | I think he forgot to add it... |
| 2022-07-12 17:55:31 +0200 | <geekosaur> | yes, this appears very confused |
| 2022-07-12 17:55:39 +0200 | vglfr | (~vglfr@88.155.25.62) (Remote host closed the connection) |
| 2022-07-12 17:55:46 +0200 | <edwardk> | builtinEnv :: IO Env; builtinEnv = return Map.empty -- seems pretty heavy, why bother requiring that to be in IO? |
| 2022-07-12 17:55:54 +0200 | vglfr | (~vglfr@88.155.25.62) |
| 2022-07-12 17:56:02 +0200 | <edwardk> | it may have had to be when there was some sequence in there and what not |
| 2022-07-12 17:56:06 +0200 | <edwardk> | but not any more |
| 2022-07-12 17:56:08 +0200 | <dextaa> | kuribas: right, removed it. I'm very confused indeed. following the crafting interpreters book but the env stuff i'm shopping around tutorials :P |
| 2022-07-12 17:56:13 +0200 | <edwardk> | guessing this code was partially refactored and never finished |
| 2022-07-12 17:56:15 +0200 | <dextaa> | from here https://abhinavsarkar.net/posts/implementing-co-2/#running-a-program |
| 2022-07-12 17:57:57 +0200 | <edwardk> | ExceptT RuntimeExcept (ContT (Either RuntimeExcept ()) (StateT InterpreterState IO)) a -- is quite complex. |
| 2022-07-12 17:58:12 +0200 | <maerwald[m]> | edwardk: how do you like rust? |
| 2022-07-12 17:58:15 +0200 | emergence | (emergence@2607:5300:60:5910:dcad:beff:feef:5bc) |
| 2022-07-12 17:58:25 +0200 | <edwardk> | maerwald[m]: i hate it, i love it, some times both at the same time |
| 2022-07-12 17:58:32 +0200 | <kuribas> | dextaa: there are some greyed out code lines... |
| 2022-07-12 17:59:50 +0200 | <maerwald[m]> | edwardk: simple things sometimes need extraordinary ceremony. Like... a for loop :p |
| 2022-07-12 18:00:21 +0200 | <kuribas> | maerwald[m]: so... like haskell? :-O |
| 2022-07-12 18:00:45 +0200 | <dextaa> | kuribas: in that blog article? The toy language I am building is different to it, I was just using the blog article as reference for the saving environment state part, but yes It's a bit over complicated for my beginner mind |
| 2022-07-12 18:02:26 +0200 | <maerwald[m]> | kuribas: i think on average, rust is more verbose than haskell. By a lot |
| 2022-07-12 18:02:40 +0200 | <kuribas> | maerwald[m]: I don't think haskell is verbose. |
| 2022-07-12 18:02:55 +0200 | <kuribas> | In my experience it's even less verbose than clojure, with types and all. |
| 2022-07-12 18:03:16 +0200 | <kuribas> | People just see a lot of types, and think it's verbose. |
| 2022-07-12 18:03:42 +0200 | indigo_ibs | (~user@31.124.106.79) (Ping timeout: 276 seconds) |
| 2022-07-12 18:03:43 +0200 | <kuribas> | Because they think the types are redundant, while they aren't. |
| 2022-07-12 18:04:29 +0200 | <maerwald[m]> | I didn't say Haskell is verbose |
| 2022-07-12 18:05:07 +0200 | <kuribas> | maerwald[m]: right. |
| 2022-07-12 18:05:21 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 18:05:51 +0200 | <geekosaur> | that could actually be taken that way, but it'd be distinguished by tone of voice. which doesn't get conveyed over irc (or slack, discord, etc.) well |
| 2022-07-12 18:06:08 +0200 | <kuribas> | maerwald[m]: someone explained parsers in rust to me, i wasn't impressed :) But then I think the goals of haskell and rust are different. |
| 2022-07-12 18:06:24 +0200 | <maerwald[m]> | I do think rust is a safer bet business wise or for hiring. I also enjoyed it a couple years ago. But it never quite felt at home |
| 2022-07-12 18:06:32 +0200 | <geekosaur> | I think rust is trying to be a better C, not a worse Haskell |
| 2022-07-12 18:07:00 +0200 | <kuribas> | indeed |
| 2022-07-12 18:07:31 +0200 | <maerwald[m]> | geekosaur: there are certainly competing forces in the rust ecosystem. But maybe less than in Haskell |
| 2022-07-12 18:08:01 +0200 | <maerwald[m]> | It seems to be more focussed on becoming a serious compiler |
| 2022-07-12 18:08:13 +0200 | <kuribas> | ocaml, f#, idris? |
| 2022-07-12 18:08:26 +0200 | <edwardk> | maerwald[m]: i like traits, fun fact, they even consulted me when implementing them, because they wanted feedback based on my old 'typeclasses vs. the world' talk. it sure as hell beats SFINAE and C++'s story which is a ratsnest of problems. i am kind of okay with the borrowing ceremony. its tedious, and it rarely catches problems _for me_ but for a team? i could see it helping a lot pin down contracts. |
| 2022-07-12 18:08:47 +0200 | <edwardk> | maerwald[m]: i find the macro import and namespacing story horrid. its just a bad design. i really miss C++ variadic templates |
| 2022-07-12 18:09:50 +0200 | <edwardk> | on the other hand, they have a compiler that gets cross-platform right from day 1. wasm as a first class citizen, so many backends, the best damn thought through graphics pipeline set anywhere |
| 2022-07-12 18:10:17 +0200 | <edwardk> | when i look at makepad and compare it to what the haskell equivalent would look like, i cry |
| 2022-07-12 18:10:48 +0200 | <maerwald[m]> | 9.6 is getting wasm |
| 2022-07-12 18:10:55 +0200 | <dextaa> | isn't rust just using LLVM so they get those backends for free anyway? |
| 2022-07-12 18:11:03 +0200 | <edwardk> | yeah but at a _tiny_ bit of overhead relative to rust ;) |
| 2022-07-12 18:11:22 +0200 | <maerwald[m]> | It may be usable in 5 years from now :p |
| 2022-07-12 18:12:17 +0200 | <edwardk> | dextaa: free is relative. there's been a lot of work put into handling wasm well, handling compiling for spir-v for shaders. |
| 2022-07-12 18:12:17 +0200 | <kuribas> | I am hoping idris will be a more efficient haskell for some targets, due to being strict.... |
| 2022-07-12 18:12:21 +0200 | <kuribas> | like javascript. |
| 2022-07-12 18:12:32 +0200 | <kuribas> | or wasm |
| 2022-07-12 18:12:34 +0200 | <maerwald[m]> | dextaa: GHC can do that too... the first M1 support release used that trick |
| 2022-07-12 18:12:34 +0200 | <Rembane> | Purescript is quite good in that regard. |
| 2022-07-12 18:12:35 +0200 | <edwardk> | ghc can use llvm on the backend for large chunks of itself, but will never run in spir-v |
| 2022-07-12 18:13:02 +0200 | <dextaa> | edwardk: ah ok |
| 2022-07-12 18:13:59 +0200 | <edwardk> | i mention spir-v because for makepad it means they write the front end, _and_ all the shaders in rust, making a very unified experience, where doing so in haskell i'd be writing a ton of EDSLs, or maybe using compiling to categories badly |
| 2022-07-12 18:14:54 +0200 | danso_o | danso |
| 2022-07-12 18:14:56 +0200 | alexhandy2 | (~trace@user/trace) (Read error: Connection reset by peer) |
| 2022-07-12 18:15:15 +0200 | alexhandy | (~trace@user/trace) |
| 2022-07-12 18:16:14 +0200 | ccntrq | (~Thunderbi@2a01:c23:8c77:3a00:6188:64f1:5d2d:a884) (Remote host closed the connection) |
| 2022-07-12 18:17:56 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-07-12 18:21:31 +0200 | mbuf | (~Shakthi@122.165.55.71) (Quit: Leaving) |
| 2022-07-12 18:22:20 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2022-07-12 18:23:12 +0200 | Guest34 | (~Guest34@2605:a601:a615:f600:b98b:a0a1:7db6:362) |
| 2022-07-12 18:25:40 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 2022-07-12 18:26:40 +0200 | zxx7529 | (~Thunderbi@user/zxx7529) (Quit: zxx7529) |
| 2022-07-12 18:28:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 18:32:32 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 18:33:02 +0200 | kuribas | (~user@silversquare.silversquare.eu) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2022-07-12 18:33:25 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2022-07-12 18:34:22 +0200 | lbseale | (~quassel@user/ep1ctetus) |
| 2022-07-12 18:34:50 +0200 | <Guest34> | Can anyone explain to me what is the role of `Functor1` in `Representable` 's `cotraverse1` ? |
| 2022-07-12 18:34:50 +0200 | <Guest34> | ( `cotraverse1 :: (Representable m, Functor1 w) => (w Identity -> a) -> w m -> m a` ) |
| 2022-07-12 18:34:51 +0200 | <Guest34> | ( `class Functor1 w where map1 :: (forall a. f a -> g a) -> w f -> w g` ) |
| 2022-07-12 18:35:06 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2022-07-12 18:37:18 +0200 | MajorBiscuit | (~MajorBisc@wlan-145-94-167-213.wlan.tudelft.nl) (Ping timeout: 240 seconds) |
| 2022-07-12 18:37:33 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2022-07-12 18:37:34 +0200 | Cajun | (~Cajun@user/cajun) |
| 2022-07-12 18:44:38 +0200 | vglfr | (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 2022-07-12 18:47:12 +0200 | <c_wraith> | Guest34: it's a higher-order version of Functor. |
| 2022-07-12 18:48:59 +0200 | dostoevsky | (~5c42c5384@user/dostoevsky) (Quit: Ping timeout (120 seconds)) |
| 2022-07-12 18:49:28 +0200 | dostoevsky | (~5c42c5384@user/dostoevsky) |
| 2022-07-12 18:51:37 +0200 | <c_wraith> | Functor is a class over types with kind (Type -> Type). Functor1 is class over types with kind (Type -> Type) -> Type |
| 2022-07-12 18:53:58 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 2022-07-12 18:55:49 +0200 | waleee | (~waleee@2001:9b0:213:7200:cc36:a556:b1e8:b340) |
| 2022-07-12 18:58:53 +0200 | kenran | (~kenran@200116b82b758c00ea3f33dad92dd6ae.dip.versatel-1u1.de) |
| 2022-07-12 18:59:44 +0200 | <Guest34> | Thanks, that's a good explanation of Functor1. Do you know why it's necessary for defining efficient operations that evaluate a Representable functor at multiple indices? |
| 2022-07-12 18:59:48 +0200 | kenran | (~kenran@200116b82b758c00ea3f33dad92dd6ae.dip.versatel-1u1.de) (Client Quit) |
| 2022-07-12 19:04:13 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 19:05:03 +0200 | benin0 | (~benin@183.82.29.162) (Quit: The Lounge - https://thelounge.chat) |
| 2022-07-12 19:05:37 +0200 | jespada | (~jespada@cpc121022-nmal24-2-0-cust171.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 2022-07-12 19:05:49 +0200 | <edwardk> | Guest34: i can maybe speak to that |
| 2022-07-12 19:06:02 +0200 | PiDelport | (uid25146@id-25146.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2022-07-12 19:06:11 +0200 | <edwardk> | Guest34: i'm not sure which version of Representable you took that from |
| 2022-07-12 19:07:18 +0200 | Vajb | (~Vajb@hag-jnsbng11-58c3ad-40.dhcp.inet.fi) (Ping timeout: 240 seconds) |
| 2022-07-12 19:07:18 +0200 | <edwardk> | but the short version is, having that notion rather than just tabulate and index allows things like 'Moore' machines to avoid having to walk all the way in and out of the functor. and it allows types where you use the type parameter at multiple 'f's to common up shapes. |
| 2022-07-12 19:07:44 +0200 | <edwardk> | data Moore a b = Moore b (a -> Moore a b) -- is a representable functor, it is represented by [a] |
| 2022-07-12 19:07:58 +0200 | Vajb | (~Vajb@n1zigc3rgo9mpde2w-1.v6.elisa-mobile.fi) |
| 2022-07-12 19:08:10 +0200 | <edwardk> | but if you have to use tabulate and index, it corresponds to giving up and starting over from the original machine feeding it a's until you select out a b. |
| 2022-07-12 19:08:19 +0200 | <edwardk> | this is asymptotically less efficient than walking down one level at a time |
| 2022-07-12 19:08:35 +0200 | <edwardk> | which scatter or cotraverse1 or whatever its called in that version does |
| 2022-07-12 19:08:43 +0200 | <edwardk> | now consider something like |
| 2022-07-12 19:09:06 +0200 | <edwardk> | newtype Person f = Person { age :: f Int, name :: f String } |
| 2022-07-12 19:09:23 +0200 | <edwardk> | without that its quite difficult to automatically generate the instance that does the right thing, pulling the 'f's out of Person |
| 2022-07-12 19:09:38 +0200 | <edwardk> | you want to take Person f -> f (Person ???) where ??? gets filled in with Identity |
| 2022-07-12 19:10:11 +0200 | <edwardk> | and you can see that as exploiting the fact that 'f' is representable to know it has a common shape for all occurrences, despite what arguments are packed into it |
| 2022-07-12 19:10:22 +0200 | dknite | (~dknite@49.37.45.188) |
| 2022-07-12 19:10:53 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 260 seconds) |
| 2022-07-12 19:10:57 +0200 | <Guest34> | Oh, that's nice. So then you get a structure that can represent the data directly, or a diff, or even a database access, and you can manipulate them all in a consistent way. |
| 2022-07-12 19:10:59 +0200 | <edwardk> | this is important, because without this Functor1 version of things, you don't get just from the distributive law a canonical implementation of index/tabulate. you have to bolt them on by hand, but _with_ this operation you can define tabulate and index once and for all for all representable functors |
| 2022-07-12 19:11:19 +0200 | <edwardk> | and you can use it to derive Applicative, the reader-like Monad instance, MonadFix, all the things |
| 2022-07-12 19:12:12 +0200 | <edwardk> | https://github.com/ekmett/distributive/blob/main/src/Data/Rep/Internal.hs#L156 is my preferred version of this idea |
| 2022-07-12 19:12:28 +0200 | <edwardk> | the class you gave above is actually pretty bad, because it doesn't work with GeneralizedNewtypeDeriving |
| 2022-07-12 19:12:36 +0200 | <edwardk> | the version with scatter that i showed does |
| 2022-07-12 19:13:21 +0200 | <edwardk> | but using the data type i define as Dist f a here: https://github.com/ekmett/distributive/blob/main/src/Data/Rep/Internal.hs#L590 you can derive a crapload of instances for free for any representable functor and they get efficient implementations using scatter. |
| 2022-07-12 19:14:06 +0200 | <Guest34> | OK, I was looking in your adjunctions repo. This one directly gives a lot more information about the type. |
| 2022-07-12 19:14:14 +0200 | <edwardk> | https://github.com/ekmett/distributive/blob/main/src/Data/Machine/Moore.hs#L42 |
| 2022-07-12 19:14:21 +0200 | vglfr | (~vglfr@88.155.25.62) |
| 2022-07-12 19:14:26 +0200 | <edwardk> | shows a bunch of instances being defined just from Dist using DerivingVia |
| 2022-07-12 19:14:49 +0200 | <edwardk> | my goal is/was to go through and refactor the entire package hierarchy i have on top of this new version of Distributive |
| 2022-07-12 19:15:19 +0200 | <edwardk> | because it shows that Distributive built off of Functor1 is powerful enough to replicate Representable |
| 2022-07-12 19:16:07 +0200 | <edwardk> | and then i go through and use generics to derive nice versions of this that either use simple counters like Fin n to index the type or use generics when there's infinite cases or use whatever you wrote by hand for tabulate and index while still offering a fast generic scatter |
| 2022-07-12 19:16:34 +0200 | <Guest34> | Very cool. This seems a lot more satisfying. |
| 2022-07-12 19:16:57 +0200 | <edwardk> | the refactored HKD package offers an F1 data type that lets GHC.Generics define the rest of this stuff |
| 2022-07-12 19:17:09 +0200 | <edwardk> | https://github.com/ekmett/hkd |
| 2022-07-12 19:17:18 +0200 | <edwardk> | you'd need to build off repos though |
| 2022-07-12 19:17:37 +0200 | <edwardk> | as its not on hackage and i'll confess i've yet to refactor the top of my package hierarchy to be compatible |
| 2022-07-12 19:17:43 +0200 | <edwardk> | i need to take a week or and just code or something |
| 2022-07-12 19:18:26 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) |
| 2022-07-12 19:19:38 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2022-07-12 19:20:53 +0200 | <Guest34> | Thanks, I'll take a look and try to understand how it all fits together. |
| 2022-07-12 19:21:24 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) |
| 2022-07-12 19:22:51 +0200 | <edwardk> | let me know if you have questions. it is a bit of a rube goldberg machine |
| 2022-07-12 19:23:09 +0200 | <edwardk> | the major selling points are the Record type which lets you generically write |
| 2022-07-12 19:23:30 +0200 | <edwardk> | Record '[Int,String] f -- and builds a vector backed version of Person above. |
| 2022-07-12 19:23:56 +0200 | <edwardk> | and the usecases for it for me are mostly around turning row-stores into column stores. because Person f -- for a representable f is a column store, and f (Person Id) is a row store |
| 2022-07-12 19:24:24 +0200 | <edwardk> | in Person f we have a functor full of ages and one full of names and we have to zip the parts we want |
| 2022-07-12 19:24:34 +0200 | <edwardk> | in f (Person Id) we're fully zipped with everything, whether we want it or not |
| 2022-07-12 19:25:20 +0200 | <edwardk> | it does do some evil evil things to get unpackable Fin's and Variants. |
| 2022-07-12 19:26:23 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) |
| 2022-07-12 19:26:23 +0200 | <edwardk> | my intention when i go to finish it is to package up the modified profunctor package, and then rebuild the remaining packages i have on top of the changed over base, the problem is it commutes a _lot_ of my dependencies, so its a big major version bump across the entire ecosystem |
| 2022-07-12 19:27:24 +0200 | <Guest34> | How much of this applies to representable profunctors? |
| 2022-07-12 19:27:32 +0200 | <edwardk> | yes |
| 2022-07-12 19:27:35 +0200 | <edwardk> | =) |
| 2022-07-12 19:27:40 +0200 | <edwardk> | thats also part of the refactor |
| 2022-07-12 19:27:59 +0200 | <edwardk> | part of the profunctors package including all the closed stuff move into distributive in the refactor |
| 2022-07-12 19:28:39 +0200 | <edwardk> | representability for profunctors is a bit trickier though, because the basis 'a' is part of the p type so you don't get to use it much |
| 2022-07-12 19:28:52 +0200 | <edwardk> | you do get to use it in closed profunctors though |
| 2022-07-12 19:29:06 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) (Remote host closed the connection) |
| 2022-07-12 19:29:30 +0200 | <edwardk> | right now it gives p a b -> p (x -> a) (x -> b) -- but the x -> can be turned into a representable functor with representation x |
| 2022-07-12 19:29:35 +0200 | azimut | (~azimut@gateway/tor-sasl/azimut) |
| 2022-07-12 19:29:39 +0200 | <edwardk> | then we can look at doing the same trick |
| 2022-07-12 19:30:49 +0200 | abhixec | (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) |
| 2022-07-12 19:30:59 +0200 | <edwardk> | e.g. can we turn something like p (u Id) (u Id) -> p (u f) (u f) ? -- for Functor1 u, Representable f? |
| 2022-07-12 19:31:04 +0200 | <Guest34> | Like the Rep-based Reader? The new type would be `p a b -> m a -. m b` ? |
| 2022-07-12 19:31:05 +0200 | <edwardk> | afk a bit |
| 2022-07-12 19:31:18 +0200 | <Guest34> | Got it, thanks again |
| 2022-07-12 19:31:48 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 2022-07-12 19:33:13 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2022-07-12 19:34:50 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 2022-07-12 19:36:26 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 19:37:29 +0200 | raehik | (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2022-07-12 19:38:28 +0200 | phma | (~phma@host-67-44-208-203.hnremote.net) (Read error: Connection reset by peer) |
| 2022-07-12 19:39:27 +0200 | phma | (phma@2001:5b0:211c:eca8:4705:335b:2d2:d9c2) |
| 2022-07-12 19:44:43 +0200 | kjak | (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 2022-07-12 19:45:00 +0200 | kjak | (~kjak@pool-108-31-68-111.washdc.fios.verizon.net) |
| 2022-07-12 19:46:28 +0200 | abhixec | (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 2022-07-12 19:47:20 +0200 | codaraxis | (~codaraxis@user/codaraxis) |
| 2022-07-12 19:47:43 +0200 | abhixec | (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) |
| 2022-07-12 19:49:16 +0200 | <Profpatsch> | Is a ~ [Int] the only way to “let bind” a type? |
| 2022-07-12 19:49:30 +0200 | <monochrom> | I think yes. |
| 2022-07-12 19:49:50 +0200 | <Profpatsch> | I’m thinking about having the return type of a postgresql query *above* the SELECT |
| 2022-07-12 19:49:58 +0200 | <monochrom> | Haha |
| 2022-07-12 19:50:00 +0200 | <Profpatsch> | So that it’s obvious what the binding is |
| 2022-07-12 19:50:18 +0200 | <monochrom> | I don't think of ~ as type-level let binding, but it does have that effect in retrospect. |
| 2022-07-12 19:50:20 +0200 | <Profpatsch> | But naively binding it against a proxy (my first idea) is not the best |
| 2022-07-12 19:50:33 +0200 | <monochrom> | People usually write type synonyms instead. |
| 2022-07-12 19:51:14 +0200 | <Profpatsch> | monochrom: Haskell is a very good functional language with a very questionable relational language tucked to the side of it |
| 2022-07-12 19:51:31 +0200 | <Bulby[m]> | what is a relational language |
| 2022-07-12 19:51:48 +0200 | <Profpatsch> | Bulby[m]: prolog for example |
| 2022-07-12 19:51:53 +0200 | <geekosaur[m]> | Anyone remember Quel? |
| 2022-07-12 19:51:59 +0200 | <Bulby[m]> | i don't write prolog |
| 2022-07-12 19:54:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 19:54:38 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 2022-07-12 19:55:26 +0200 | <Profpatsch> | but there’s no way if I have a (Proxy a) in hand to “pass” the a to another binding? |
| 2022-07-12 19:55:35 +0200 | <Profpatsch> | apart from doing the ~ in the function sig |
| 2022-07-12 19:55:37 +0200 | <heath> | [exa]: re: package definining algebraic structures and how "efficient"... "should be able to deal with matrix dimensions in the 100s or 1000s |
| 2022-07-12 19:55:49 +0200 | <heath> | "I've started using hmatrix and so far i'm pretty happy with it. Another option i found was the package linear, but it seems like it was aimed at low dimensional (3 or 4) stuff ?" |
| 2022-07-12 19:56:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 20:01:02 +0200 | <[exa]> | yeah linear is a bit more towards the 3d graphics math |
| 2022-07-12 20:01:16 +0200 | dsp | (~dsp@cpc152107-haye27-2-0-cust227.17-4.cable.virginm.net) (Quit: Leaving) |
| 2022-07-12 20:05:53 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 2022-07-12 20:07:10 +0200 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 240 seconds) |
| 2022-07-12 20:07:34 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 20:07:56 +0200 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 2022-07-12 20:08:35 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 20:11:01 +0200 | ski | (~ski@ext-1-468.eduroam.chalmers.se) |
| 2022-07-12 20:16:12 +0200 | dsrt | (~dsrt@96-91-148-113-static.hfc.comcastbusiness.net) (Remote host closed the connection) |
| 2022-07-12 20:17:23 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) (Ping timeout: 272 seconds) |
| 2022-07-12 20:17:32 +0200 | lottaquestions | (~nick@S0106a84e3f794893.ca.shawcable.net) |
| 2022-07-12 20:25:43 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 20:28:54 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) (Ping timeout: 264 seconds) |
| 2022-07-12 20:29:57 +0200 | <amonowy> | Hi! I'm looking for someone to review my first Haskell project. I was learning while working on it. It has 1700 loc and is simple Trello terminal client. If you want to do few iterations with me I'll be happy to pay 50$/h. You can check it here https://gitlab.com/amonowy/haskello/-/tree/cursor-refactor |
| 2022-07-12 20:34:07 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 20:37:13 +0200 | <dextaa> | Could someone help out with my (subsequent) compile error? :P https://paste.tomsmeding.com/0MsmLb3t |
| 2022-07-12 20:38:50 +0200 | <[exa]> | amonowy: looks cool tbh, pretty clean & understandable as far as I click (randomly) |
| 2022-07-12 20:39:33 +0200 | <geekosaur> | dextaa, your defineVarEnv is in InterpreterEnv, but it needs to be in IO for you to use newIORef |
| 2022-07-12 20:39:41 +0200 | <ski> | dextaa : `valueRef <- liftIO (newIORef val)' ? |
| 2022-07-12 20:40:03 +0200 | <[exa]> | amonowy: anything specific for feedback? I noticed you manage the state manually, could be interesting to try out actual monadic State and lenses; it gives much simpler updates :] |
| 2022-07-12 20:40:17 +0200 | enthropy | (~enthropy@24-246-69-9.cable.teksavvy.com) |
| 2022-07-12 20:41:02 +0200 | <[exa]> | amonowy: also try running hlint on the source, it has good hints. (e.g. this https://gitlab.com/amonowy/haskello/-/blob/cursor-refactor/src/State/AppState.hs#L92 might be concatMap if I get it right) |
| 2022-07-12 20:42:37 +0200 | <dextaa> | geekosaur, ski : thanks. Don't see how the code i'm basing mine off compiled without that but oh well ¯\_(ツ)_/¯ |
| 2022-07-12 20:43:23 +0200 | <geekosaur> | mm, didn't you say earlier you'd taken that part from blog posts? those may simply have been in IO with the state in an IORef or something |
| 2022-07-12 20:44:00 +0200 | <geekosaur> | which is not a preferred way of writing things, but would work at least if you were going for a more procedural feel |
| 2022-07-12 20:44:40 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 20:46:00 +0200 | <dextaa> | Seems the same https://abhinavsarkar.net/code/co-interpreter.html |
| 2022-07-12 20:46:01 +0200 | <amonowy> | Thanks [exa] ! I tried to use simplest constructs to understand it better. Will give it a try with your suggestions! There is this io func that is crucial to sync with server. I use recursive monadic bind. Wonder if there is typeclas I can use to make it terser https://gitlab.com/amonowy/haskello/-/blob/cursor-refactor/src/Event.hs#L407 |
| 2022-07-12 20:46:06 +0200 | <[exa]> | amonowy: outright lens sploier: addCards cs = listCards %~ (cs++) |
| 2022-07-12 20:46:20 +0200 | <[exa]> | hm lemme check |
| 2022-07-12 20:47:22 +0200 | <[exa]> | yeah you literally have almost State in there already. `Control.Monad.State` represents the `state -> (result,state)` as a convention for you. |
| 2022-07-12 20:48:53 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2022-07-12 20:49:29 +0200 | <[exa]> | (like, don't get me wrong, this is probably the best way you could do it without jumping to more advanced haskell :] ) |
| 2022-07-12 20:49:39 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-07-12 20:49:43 +0200 | <amonowy> | I was trying to use it but couldn't find how to iterate until hit end condition |
| 2022-07-12 20:49:46 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 20:49:58 +0200 | <amonowy> | Like monad transformers? |
| 2022-07-12 20:51:09 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) (Ping timeout: 244 seconds) |
| 2022-07-12 20:51:17 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) (Remote host closed the connection) |
| 2022-07-12 20:51:20 +0200 | <[exa]> | yeah transformers combine the monadic stuff, that your type you have there would be equivalent to `StateT AppState IO Bool` |
| 2022-07-12 20:51:31 +0200 | [itchyjunk] | (~itchyjunk@user/itchyjunk/x-7353470) |
| 2022-07-12 20:51:52 +0200 | <[exa]> | you know about how functors work? |
| 2022-07-12 20:52:56 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-07-12 20:53:05 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2022-07-12 20:53:50 +0200 | gmg | (~user@user/gehmehgeh) |
| 2022-07-12 20:54:57 +0200 | <[exa]> | amonowy: btw there's this https://hackage.haskell.org/package/extra-1.7.10/docs/Control-Monad-Extra.html#v:whileM (and a few other helpful combinators-- I guess one of them would fit into your saveStateToServer?) |
| 2022-07-12 20:54:58 +0200 | slack1256 | (~slack1256@191.126.99.206) (Read error: Connection reset by peer) |
| 2022-07-12 20:55:38 +0200 | <amonowy> | I think I do although I'm not sure if enough |
| 2022-07-12 20:55:42 +0200 | slack1256 | (~slack1256@186.11.84.89) |
| 2022-07-12 20:55:51 +0200 | <Guest34> | It's good to understand state transformers, but sometimes it's more flexible to just use `withFoo` bracketing functions directly, no monads except IO. |
| 2022-07-12 20:55:54 +0200 | <amonowy> | Thanks will check that as well |
| 2022-07-12 20:56:41 +0200 | pmarg | (~pmarg@2a01:799:159f:9b00:36a6:c77c:6059:5758) (Remote host closed the connection) |
| 2022-07-12 20:56:41 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 20:56:46 +0200 | <[exa]> | amonowy: btw where's the recursion in that funciton? (not sure if I spotted it) |
| 2022-07-12 20:58:21 +0200 | <amonowy> | Sorry it in function called by saveStateToServer https://gitlab.com/amonowy/haskello/-/blob/cursor-refactor/src/Event.hs#L437 |
| 2022-07-12 20:59:23 +0200 | vglfr | (~vglfr@88.155.25.62) (Ping timeout: 260 seconds) |
| 2022-07-12 21:01:51 +0200 | <[exa]> | amonowy: you could probably simplify that a bit -- you're passing it a (trivial) IO action that just returns the SyncedChanges, but I guess there's no reason because it can live just with the data |
| 2022-07-12 21:01:55 +0200 | <[exa]> | lemme try |
| 2022-07-12 21:05:30 +0200 | nschoe | (~quassel@2a01:e0a:8e:a190:5f4c:d84e:12c7:8ba) |
| 2022-07-12 21:05:37 +0200 | <[exa]> | amonowy: https://paste.tomsmeding.com/iV2T83MZ |
| 2022-07-12 21:05:53 +0200 | <[exa]> | (no guarantees, I just wrote it) |
| 2022-07-12 21:06:13 +0200 | <[exa]> | (ie right should be Right... :D ) |
| 2022-07-12 21:08:41 +0200 | mikoto-chan | (~mikoto-ch@dzw9kf47j-sy--ghcbk-4.rev.dnainternet.fi) |
| 2022-07-12 21:12:11 +0200 | <amonowy> | Awesome, nice one. I like how you get rid of superfluous 'return' calls |
| 2022-07-12 21:13:23 +0200 | Everything | (~Everythin@37.115.210.35) |
| 2022-07-12 21:15:01 +0200 | coot | (~coot@213.134.190.95) |
| 2022-07-12 21:19:59 +0200 | seriously | (~seriously@ool-18bd55d4.dyn.optonline.net) |
| 2022-07-12 21:20:09 +0200 | <seriously> | hey gentleman... |
| 2022-07-12 21:20:39 +0200 | <seriously> | Working on histogram problem in cis194 ... |
| 2022-07-12 21:21:11 +0200 | <seriously> | just about finished... it it possible to use a variable within a list comprehension? |
| 2022-07-12 21:21:29 +0200 | <seriously> | e.g. [maxOccurs..(-1)] |
| 2022-07-12 21:21:57 +0200 | <geekosaur> | sure |
| 2022-07-12 21:22:12 +0200 | machinedgod | (~machinedg@184.68.124.102) |
| 2022-07-12 21:22:13 +0200 | <geekosaur> | but if you intend that to count down, you have to say that |
| 2022-07-12 21:22:23 +0200 | Everything | (~Everythin@37.115.210.35) () |
| 2022-07-12 21:22:44 +0200 | <geekosaur> | [maxOccurs, maxOccurs - 1 .. -1] |
| 2022-07-12 21:22:52 +0200 | <geekosaur> | otherwise it counts up |
| 2022-07-12 21:23:02 +0200 | <seriously> | ok so yeah im trying to countdown from this dynamic variable to -1 |
| 2022-07-12 21:23:10 +0200 | <ski> | seriously : fwiw, that's an enumeration, not a list comprehension |
| 2022-07-12 21:23:26 +0200 | <geekosaur> | enumerations expand to normal functions, btw |
| 2022-07-12 21:23:26 +0200 | <ski> | > [9 .. 0] |
| 2022-07-12 21:23:28 +0200 | <lambdabot> | [] |
| 2022-07-12 21:23:31 +0200 | <ski> | > [9,8 .. 0] |
| 2022-07-12 21:23:33 +0200 | <lambdabot> | [9,8,7,6,5,4,3,2,1,0] |
| 2022-07-12 21:23:51 +0200 | <geekosaur> | enumFrom, enumFromTo, enumFromThenTo |
| 2022-07-12 21:23:51 +0200 | <seriously> | yes thats what im seeing now ski geekosaur |
| 2022-07-12 21:24:15 +0200 | <ski> | `[9,8 .. 0]' is desugared to `enumFromThenTo 9 8 0' |
| 2022-07-12 21:24:57 +0200 | <ski> | (there's also `enumFromThen') |
| 2022-07-12 21:24:57 +0200 | <seriously> | that worked! thx |
| 2022-07-12 21:25:20 +0200 | <ski> | @src Enum |
| 2022-07-12 21:25:20 +0200 | <lambdabot> | class Enum a where |
| 2022-07-12 21:25:20 +0200 | <lambdabot> | succ, pred :: a -> a |
| 2022-07-12 21:25:20 +0200 | <lambdabot> | toEnum :: Int -> a |
| 2022-07-12 21:25:20 +0200 | <lambdabot> | fromEnum :: a -> Int |
| 2022-07-12 21:25:20 +0200 | <lambdabot> | enumFrom :: a -> [a] |
| 2022-07-12 21:25:22 +0200 | <lambdabot> | enumFromThen, enumFromTo :: a -> a -> [a] |
| 2022-07-12 21:25:24 +0200 | <lambdabot> | enumFromThenTo :: a -> a -> a -> [a] |
| 2022-07-12 21:27:30 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2022-07-12 21:29:45 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-07-12 21:30:07 +0200 | <EvanR> | Enum. how quaint |
| 2022-07-12 21:30:19 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) (Quit: The Lounge - https://thelounge.chat) |
| 2022-07-12 21:30:31 +0200 | <EvanR> | and they said a -> a was impossible! |
| 2022-07-12 21:30:42 +0200 | <tomsmeding> | :t id |
| 2022-07-12 21:30:43 +0200 | <EvanR> | oops that was a -> b |
| 2022-07-12 21:30:43 +0200 | <lambdabot> | a -> a |
| 2022-07-12 21:31:08 +0200 | <tomsmeding> | :t fix id :: a -> b |
| 2022-07-12 21:31:09 +0200 | <lambdabot> | a -> b |
| 2022-07-12 21:31:14 +0200 | <EvanR> | that's cheating |
| 2022-07-12 21:31:25 +0200 | tomsmeding | whistles innocently |
| 2022-07-12 21:32:00 +0200 | <tomsmeding> | % import Data.Coerce |
| 2022-07-12 21:32:00 +0200 | <yahb2> | <no output> |
| 2022-07-12 21:32:07 +0200 | <tomsmeding> | % :info Coercible |
| 2022-07-12 21:32:07 +0200 | <yahb2> | {- ; Coercible is a special constraint with custom solving rules. ; It is not a class. ; Please see section `The Coercible constraint` ; of the user's guide for details. ; -} ; type role Coercible ... |
| 2022-07-12 21:32:13 +0200 | <int-e> | :t Unsafe.Coerce.unsafeCoerce |
| 2022-07-12 21:32:14 +0200 | <tomsmeding> | Sad |
| 2022-07-12 21:32:15 +0200 | <lambdabot> | a -> b |
| 2022-07-12 21:32:37 +0200 | <int-e> | :t Data.Coerce.coerce |
| 2022-07-12 21:32:38 +0200 | <lambdabot> | Coercible a b => a -> b |
| 2022-07-12 21:33:19 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) |
| 2022-07-12 21:35:47 +0200 | <ski> | @type cast |
| 2022-07-12 21:35:48 +0200 | <lambdabot> | (Typeable a, Typeable b) => a -> Maybe b |
| 2022-07-12 21:37:07 +0200 | <Guest34> | > let foo _ = Nothing |
| 2022-07-12 21:37:09 +0200 | <lambdabot> | <no location info>: error: not an expression: ‘let foo _ = Nothing’ |
| 2022-07-12 21:37:22 +0200 | <Guest34> | :t const Nothing |
| 2022-07-12 21:37:24 +0200 | <lambdabot> | b -> Maybe a |
| 2022-07-12 21:43:08 +0200 | pavonia | (~user@user/siracusa) |
| 2022-07-12 21:45:46 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) (Quit: The Lounge - https://thelounge.chat) |
| 2022-07-12 21:47:06 +0200 | acidjnk_new | (~acidjnk@p200300d6e7058634ccce5b583b17b980.dip0.t-ipconnect.de) |
| 2022-07-12 21:47:17 +0200 | chomwitt | (~chomwitt@2a02:587:dc0d:4a00:ae09:5cbc:3a9a:5a89) |
| 2022-07-12 21:47:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 21:48:28 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) |
| 2022-07-12 21:48:35 +0200 | acidjnk | (~acidjnk@p200300d6e7058634bd1cff6d17bc0490.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2022-07-12 21:49:18 +0200 | christiansen | (~christian@83-95-137-75-dynamic.dk.customer.tdc.net) (Ping timeout: 240 seconds) |
| 2022-07-12 21:50:14 +0200 | Pickchea | (~private@user/pickchea) |
| 2022-07-12 21:50:34 +0200 | jgeerds | (~jgeerds@55d437cf.access.ecotel.net) |
| 2022-07-12 21:51:06 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 21:52:22 +0200 | <ski> | > let foo _ = Nothing in foo "Guest34" |
| 2022-07-12 21:52:23 +0200 | <lambdabot> | Nothing |
| 2022-07-12 21:54:15 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) (Quit: The Lounge - https://thelounge.chat) |
| 2022-07-12 21:56:58 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) |
| 2022-07-12 21:59:21 +0200 | machinedgod | (~machinedg@184.68.124.102) (Ping timeout: 272 seconds) |
| 2022-07-12 21:59:33 +0200 | vglfr | (~vglfr@46.96.135.38) |
| 2022-07-12 22:00:20 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-07-12 22:01:24 +0200 | slac35555 | (~slack1256@191.125.99.206) |
| 2022-07-12 22:03:33 +0200 | slack1256 | (~slack1256@186.11.84.89) (Ping timeout: 260 seconds) |
| 2022-07-12 22:03:40 +0200 | coot | (~coot@213.134.190.95) |
| 2022-07-12 22:03:58 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 22:06:16 +0200 | <dextaa> | Could someone help me with this subsequent (subsequent) build error https://paste.tomsmeding.com/oA8Vs0B2 ? |
| 2022-07-12 22:06:32 +0200 | _ht | (~quassel@231-169-21-31.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2022-07-12 22:08:07 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 22:08:44 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 22:08:58 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 22:09:02 +0200 | <ski> | i'd call that a type error, not a build error |
| 2022-07-12 22:09:13 +0200 | <ski> | dextaa : and the solution, again, is `liftIO' |
| 2022-07-12 22:09:19 +0200 | <geekosaur> | that's going to be the same issue as with the earlier readIORef, namely … that |
| 2022-07-12 22:10:21 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-07-12 22:10:22 +0200 | <ski> | .. >>= liftIO . flip writeIORef value |
| 2022-07-12 22:10:41 +0200 | talismanick | (~talismani@campus-117-212.ucdavis.edu) |
| 2022-07-12 22:10:47 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 22:10:58 +0200 | <dextaa> | ah thanks |
| 2022-07-12 22:11:10 +0200 | <dextaa> | I was trying to use liftIO but in the wrong places apparently :P |
| 2022-07-12 22:11:38 +0200 | <ski> | not writing in pointless style, at least to begin with, might help there |
| 2022-07-12 22:11:49 +0200 | Cajun | (~Cajun@user/cajun) (Quit: Client closed) |
| 2022-07-12 22:12:03 +0200 | <dextaa> | true |
| 2022-07-12 22:18:00 +0200 | Topsi | (~Topsi@host-88-217-154-179.customer.m-online.net) |
| 2022-07-12 22:18:07 +0200 | Topsi | (~Topsi@host-88-217-154-179.customer.m-online.net) (Client Quit) |
| 2022-07-12 22:20:07 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 22:20:53 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 272 seconds) |
| 2022-07-12 22:21:38 +0200 | Sgeo_ | (~Sgeo@user/sgeo) |
| 2022-07-12 22:21:42 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Remote host closed the connection) |
| 2022-07-12 22:21:58 +0200 | codaraxis__ | (~codaraxis@user/codaraxis) |
| 2022-07-12 22:22:17 +0200 | allbery_b | (~geekosaur@xmonad/geekosaur) |
| 2022-07-12 22:22:17 +0200 | geekosaur | (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2022-07-12 22:22:19 +0200 | mncheckm | (~mncheck@193.224.205.254) |
| 2022-07-12 22:22:20 +0200 | allbery_b | geekosaur |
| 2022-07-12 22:22:27 +0200 | abhixec | (~abhinav@c-67-169-139-16.hsd1.ca.comcast.net) (Quit: leaving) |
| 2022-07-12 22:22:47 +0200 | sayola | (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) |
| 2022-07-12 22:23:11 +0200 | bontaq` | (~user@ool-45779fe5.dyn.optonline.net) |
| 2022-07-12 22:23:11 +0200 | EsoAlgo9 | (~EsoAlgo@129.146.136.145) |
| 2022-07-12 22:23:23 +0200 | elkcl_ | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 2022-07-12 22:23:45 +0200 | sloorush | (~sloorush@52.187.184.81) |
| 2022-07-12 22:24:04 +0200 | sndr | (~sander@user/sander) |
| 2022-07-12 22:25:00 +0200 | lottaquestions_ | (~nick@S0106a84e3f794893.ca.shawcable.net) |
| 2022-07-12 22:25:59 +0200 | cosimone` | (~user@2001:b07:ae5:db26:57c7:21a5:6e1c:6b81) |
| 2022-07-12 22:26:04 +0200 | triteraf1ops | (~triterafl@user/triteraflops) |
| 2022-07-12 22:26:30 +0200 | gurkengl1s | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) |
| 2022-07-12 22:26:33 +0200 | pretty_d1 | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2022-07-12 22:26:36 +0200 | dextaa8 | (~DV@user/dextaa) |
| 2022-07-12 22:26:49 +0200 | kritzefitz_ | (~kritzefit@debian/kritzefitz) |
| 2022-07-12 22:28:31 +0200 | kritzefitz__ | (~kritzefit@212.86.56.80) |
| 2022-07-12 22:28:35 +0200 | kritzefitz__ | (~kritzefit@212.86.56.80) () |
| 2022-07-12 22:28:44 +0200 | Alex_test_ | (~al_test@178.34.160.206) |
| 2022-07-12 22:29:50 +0200 | kritzefitz | (~kritzefit@debian/kritzefitz) (Killed (NickServ (GHOST command used by kritzefitz_))) |
| 2022-07-12 22:29:57 +0200 | kritzefitz_ | kritzefitz |
| 2022-07-12 22:30:16 +0200 | Guest34 | (~Guest34@2605:a601:a615:f600:b98b:a0a1:7db6:362) (Quit: Client closed) |
| 2022-07-12 22:30:31 +0200 | elkcl__ | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) |
| 2022-07-12 22:30:51 +0200 | elkcl_ | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (Ping timeout: 276 seconds) |
| 2022-07-12 22:31:00 +0200 | alexhandy | (~trace@user/trace) (Read error: Connection reset by peer) |
| 2022-07-12 22:31:14 +0200 | seriously | (~seriously@ool-18bd55d4.dyn.optonline.net) (Ping timeout: 252 seconds) |
| 2022-07-12 22:31:15 +0200 | EsoAlgo | (~EsoAlgo@129.146.136.145) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | lottaquestions | (~nick@S0106a84e3f794893.ca.shawcable.net) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | elkcl | (~elkcl@broadband-37-110-156-162.ip.moscow.rt.ru) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | gurkenglas | (~gurkengla@dslb-002-203-144-112.002.203.pools.vodafone-ip.de) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | codaraxis | (~codaraxis@user/codaraxis) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | dextaa | (~DV@user/dextaa) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | shriekingnoise | (~shrieking@201.212.175.181) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | Sgeo | (~Sgeo@user/sgeo) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | Alex_test | (~al_test@178.34.160.206) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | bontaq | (~user@ool-45779fe5.dyn.optonline.net) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | pretty_dumm_guy | (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | `2jt | (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | hiredman | (~hiredman@frontier1.downey.family) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | triteraflops | (~triterafl@user/triteraflops) (*.net *.split) |
| 2022-07-12 22:31:15 +0200 | wagle | (~wagle@quassel.wagle.io) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | mzan | (~quassel@mail.asterisell.com) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | brettgilio | (~brettgili@c9yh.net) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | In0perable | (~PLAYER_1@fancydata.science) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | rush | (~sloorush@52.187.184.81) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | sander | (~sander@user/sander) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | neightchan | (~nate@98.45.169.16) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | zaquest | (~notzaques@5.130.79.72) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | sayola1 | (~sayola@dslb-088-078-152-210.088.078.pools.vodafone-ip.de) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | cosimone | (~user@93-44-186-171.ip98.fastwebnet.it) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | sagax | (~sagax_nb@user/sagax) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | mjs2600 | (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | foul_owl | (~kerry@23.82.194.109) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | mncheck | (~mncheck@193.224.205.254) (*.net *.split) |
| 2022-07-12 22:31:16 +0200 | EsoAlgo9 | EsoAlgo |
| 2022-07-12 22:31:16 +0200 | sndr | sander |
| 2022-07-12 22:31:17 +0200 | elkcl__ | elkcl |
| 2022-07-12 22:32:14 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2022-07-12 22:32:15 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 22:32:34 +0200 | califax | (~califax@user/califx) |
| 2022-07-12 22:33:04 +0200 | machinedgod | (~machinedg@d172-219-86-154.abhsia.telus.net) |
| 2022-07-12 22:34:54 +0200 | rustisafungus | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 22:34:54 +0200 | tzh | (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2022-07-12 22:34:54 +0200 | troydm | (~troydm@host-176-37-124-197.b025.la.net.ua) |
| 2022-07-12 22:34:54 +0200 | shriekingnoise | (~shrieking@201.212.175.181) |
| 2022-07-12 22:34:54 +0200 | `2jt | (~jtomas@141.red-88-17-65.dynamicip.rima-tde.net) |
| 2022-07-12 22:34:54 +0200 | In0perable | (~PLAYER_1@fancydata.science) |
| 2022-07-12 22:34:54 +0200 | hiredman | (~hiredman@frontier1.downey.family) |
| 2022-07-12 22:34:54 +0200 | wagle | (~wagle@quassel.wagle.io) |
| 2022-07-12 22:34:54 +0200 | mzan | (~quassel@mail.asterisell.com) |
| 2022-07-12 22:34:54 +0200 | brettgilio | (~brettgili@c9yh.net) |
| 2022-07-12 22:34:54 +0200 | neightchan | (~nate@98.45.169.16) |
| 2022-07-12 22:34:54 +0200 | mjs2600 | (~mjs2600@c-24-91-3-49.hsd1.vt.comcast.net) |
| 2022-07-12 22:35:07 +0200 | In0perable | (~PLAYER_1@fancydata.science) (Max SendQ exceeded) |
| 2022-07-12 22:35:59 +0200 | wenjie | (~nut@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
| 2022-07-12 22:36:04 +0200 | mikoto-chan | (~mikoto-ch@dzw9kf47j-sy--ghcbk-4.rev.dnainternet.fi) (Read error: Connection reset by peer) |
| 2022-07-12 22:36:18 +0200 | <wenjie> | anyone familiar with brick tui library? anyway to make a txt widget scrollable? |
| 2022-07-12 22:36:23 +0200 | Inoperable | (~PLAYER_1@fancydata.science) |
| 2022-07-12 22:36:40 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 22:36:50 +0200 | zaquest | (~notzaques@5.130.79.72) |
| 2022-07-12 22:37:36 +0200 | Katarushisu | (~Katarushi@cpc147334-finc20-2-0-cust27.4-2.cable.virginm.net) |
| 2022-07-12 22:37:44 +0200 | vglfr | (~vglfr@46.96.135.38) (Ping timeout: 255 seconds) |
| 2022-07-12 22:38:00 +0200 | nschoe | (~quassel@2a01:e0a:8e:a190:5f4c:d84e:12c7:8ba) (Ping timeout: 276 seconds) |
| 2022-07-12 22:39:54 +0200 | Qudit | (~user@user/Qudit) |
| 2022-07-12 22:40:21 +0200 | foul_owl | (~kerry@23.82.194.109) |
| 2022-07-12 22:40:28 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-97.elisa-laajakaista.fi) |
| 2022-07-12 22:41:09 +0200 | biberu | (~biberu@user/biberu) (Ping timeout: 272 seconds) |
| 2022-07-12 22:43:24 +0200 | Guest|38 | (~Guest|38@89.253.138.59) |
| 2022-07-12 22:44:35 +0200 | econo | (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 2022-07-12 22:45:22 +0200 | pmarg | (~pmarg@2a01:799:159f:9b00:64d8:8354:ad7c:2411) |
| 2022-07-12 22:48:12 +0200 | biberu | (~biberu@user/biberu) |
| 2022-07-12 22:49:15 +0200 | sagax | (~sagax_nb@213.138.71.146) |
| 2022-07-12 22:50:14 +0200 | alexhandy | (~trace@user/trace) |
| 2022-07-12 22:51:56 +0200 | Midjak | (~Midjak@82.66.147.146) (Quit: This computer has gone to sleep) |
| 2022-07-12 22:51:59 +0200 | econo | (uid147250@user/econo) |
| 2022-07-12 22:52:19 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Remote host closed the connection) |
| 2022-07-12 22:52:23 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 22:53:14 +0200 | geschwindingskei | (~John_Ivan@user/john-ivan/x-1515935) |
| 2022-07-12 22:54:53 +0200 | <geschwindingskei> | hello haskell community. I'm looking for the equivalent of objects/structs/classes in haskell for describing a model. there's a few concepts here I came across.... Records, DataTypes and Type Classes. I presume these aren't what I'm looking for? |
| 2022-07-12 22:55:25 +0200 | <Rembane> | geschwindingskei: They are, tell us more about what you're trying to model. |
| 2022-07-12 22:55:49 +0200 | <Rembane> | geschwindingskei: Having functions that take records as arguments and produce more records is a quite useful set of tools. |
| 2022-07-12 22:56:35 +0200 | talismanick | (~talismani@campus-117-212.ucdavis.edu) (Ping timeout: 268 seconds) |
| 2022-07-12 22:56:38 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) (Ping timeout: 255 seconds) |
| 2022-07-12 22:56:40 +0200 | <geschwindingskei> | Rembane, well, since I'm comparing with models in imperative, I guess I'll start simple. A class Car containing various fields, say Colour and Size, of type "string" and "int". And a function to drive(); |
| 2022-07-12 22:56:52 +0200 | <geschwindingskei> | is what I'm trying to see the equivalent of in Haskell |
| 2022-07-12 22:58:43 +0200 | mon_aaraj | (~MonAaraj@user/mon-aaraj/x-4416475) |
| 2022-07-12 22:59:38 +0200 | lottaquestions_ | (~nick@S0106a84e3f794893.ca.shawcable.net) (Ping timeout: 240 seconds) |
| 2022-07-12 22:59:39 +0200 | <Guest|38> | Hi guys I ran powershell command in GHCup the page, but it seems not to add stack or ghcup to path |
| 2022-07-12 23:00:02 +0200 | <Rembane> | geschwindingskei: Something like this: data Car = Car String Int; |
| 2022-07-12 23:00:06 +0200 | <Rembane> | geschwindingskei: How would you drive that car? |
| 2022-07-12 23:00:21 +0200 | <Rembane> | geschwindingskei: It has no notion of position, velocity or acceleration. |
| 2022-07-12 23:00:26 +0200 | nosewings | (~ngpc@cpe-76-186-194-45.tx.res.rr.com) |
| 2022-07-12 23:01:05 +0200 | <geschwindingskei> | Rembane, just the association of the model/class' function as a private or public member for the function drive(). implementation is not important or any of the sort. I'm just trying to do some comparison. |
| 2022-07-12 23:01:33 +0200 | <geschwindingskei> | Rembane, is that a record? |
| 2022-07-12 23:01:48 +0200 | coot | (~coot@213.134.190.95) (Quit: coot) |
| 2022-07-12 23:02:14 +0200 | <Rembane> | geschwindingskei: Fair enough. We can use my new (patent pending) function: shrink :: Car -> Car; shrink (Car c size) = Car c (div size 2) |
| 2022-07-12 23:02:57 +0200 | <Rembane> | geschwindingskei: That's not a record, I took a shortcut and made it a datatype without accessor functions. Here's an example of the same thing as a record: data Car = Car { colour :: String, size :: Int } |
| 2022-07-12 23:04:31 +0200 | <geschwindingskei> | Rembane, reading. I'll ask questions in a moment, trying to figure thing sout. |
| 2022-07-12 23:04:34 +0200 | <geschwindingskei> | thank you. |
| 2022-07-12 23:05:42 +0200 | <Rembane> | geschwindingskei: No worries. :) |
| 2022-07-12 23:05:47 +0200 | Alex_test_ | Alex_test |
| 2022-07-12 23:06:39 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 23:07:30 +0200 | <geschwindingskei> | Rembane, what kind of assignment is that under the datatype? |
| 2022-07-12 23:08:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 23:10:59 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 255 seconds) |
| 2022-07-12 23:12:14 +0200 | Pickchea | (~private@user/pickchea) (Quit: Leaving) |
| 2022-07-12 23:12:16 +0200 | <Rembane> | geschwindingskei: It's the syntax for creating a datatype, it's slightly strange but quite useful. |
| 2022-07-12 23:16:19 +0200 | <geschwindingskei> | Rembane, I see. so, ```Car = Car String Int``` - where and how would one define a constructor for this? |
| 2022-07-12 23:16:31 +0200 | <Rembane> | geschwindingskei: Somewhere in a module. |
| 2022-07-12 23:16:55 +0200 | <geschwindingskei> | So this would be more of a structure than a class. |
| 2022-07-12 23:17:10 +0200 | cosimone` | (~user@2001:b07:ae5:db26:57c7:21a5:6e1c:6b81) (Ping timeout: 260 seconds) |
| 2022-07-12 23:18:25 +0200 | <Rembane> | geschwindingskei: What's the difference between a structure and a class? |
| 2022-07-12 23:18:49 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2022-07-12 23:19:12 +0200 | <geschwindingskei> | Rembane, accessors, mutators, methods, constructors/destructors and inheritance/oop paradigms. |
| 2022-07-12 23:19:22 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2022-07-12 23:19:23 +0200 | <geschwindingskei> | structures are merely blobs of data. |
| 2022-07-12 23:19:30 +0200 | <geschwindingskei> | classes are more complex. |
| 2022-07-12 23:19:39 +0200 | lottaquestions_ | (~nick@S0106a84e3f794893.ca.shawcable.net) |
| 2022-07-12 23:19:57 +0200 | <darkling> | And the accessors, mutators, methods, contructors and destructors are just functions that take a structure as a parameter. |
| 2022-07-12 23:19:58 +0200 | rustisafungus | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 260 seconds) |
| 2022-07-12 23:20:01 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2022-07-12 23:20:05 +0200 | fserucas | (~fserucas@12.64.114.89.rev.vodafone.pt) (Quit: Leaving) |
| 2022-07-12 23:20:16 +0200 | <geschwindingskei> | darkling, the "self" you mean? |
| 2022-07-12 23:20:41 +0200 | <darkling> | Exactly. |
| 2022-07-12 23:21:00 +0200 | <Rembane> | geschwindingskei: Okay, so how would you implement my shrink function in an OOP language? |
| 2022-07-12 23:21:03 +0200 | chomwitt | (~chomwitt@2a02:587:dc0d:4a00:ae09:5cbc:3a9a:5a89) (Ping timeout: 272 seconds) |
| 2022-07-12 23:21:37 +0200 | <geschwindingskei> | but there's no sugar syntax to keep/show that this structure strictly has methods associated with it. |
| 2022-07-12 23:21:53 +0200 | <geschwindingskei> | in other words, I'm asking if there's some sort of "." dot operator to access a class' associated data. |
| 2022-07-12 23:21:55 +0200 | <geschwindingskei> | \methods |
| 2022-07-12 23:22:04 +0200 | <geschwindingskei> | is this correct? |
| 2022-07-12 23:22:26 +0200 | <Rembane> | None at all. |
| 2022-07-12 23:22:53 +0200 | <geschwindingskei> | right. so let me guess. I would have to append "Car" as the first parameter in all my associated functions |
| 2022-07-12 23:23:03 +0200 | <geschwindingskei> | ok. got it. |
| 2022-07-12 23:23:14 +0200 | <darkling> | You've got type declarations on the functions that will tell you if it works on objects of the structure, of course. |
| 2022-07-12 23:23:59 +0200 | <Rembane> | geschwindingskei: Yes, all functions that should do something with a Car needs to take Car as a parameter. |
| 2022-07-12 23:24:00 +0200 | <darkling> | You wouldn't necessarily use the first parameter in all cases -- sometimes it makes sense to put a different parameter first (because of currying and partial application of functions) |
| 2022-07-12 23:24:25 +0200 | <geschwindingskei> | I understood. |
| 2022-07-12 23:24:48 +0200 | <geschwindingskei> | Okay, and in respect to Records - what kind of assignment is that? I recall there being a particular name for it. |
| 2022-07-12 23:24:57 +0200 | <geschwindingskei> | Something to do with order of declaration defining parametrization. |
| 2022-07-12 23:25:38 +0200 | talismanick | (~talismani@2601:200:c100:3850::dd64) |
| 2022-07-12 23:26:20 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2022-07-12 23:27:10 +0200 | <Rembane> | There's something about it here: https://wiki.haskell.org/Parameter_order |
| 2022-07-12 23:28:21 +0200 | indigo_ibs | (~user@31.124.106.79) |
| 2022-07-12 23:29:55 +0200 | jakalx | (~jakalx@base.jakalx.net) (Error from remote client) |
| 2022-07-12 23:30:00 +0200 | dtman34 | (~dtman34@c-73-62-246-247.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 2022-07-12 23:32:15 +0200 | dtman34 | (~dtman34@2601:446:4400:2ad9:50de:fed7:560f:d711) |
| 2022-07-12 23:34:11 +0200 | <geschwindingskei> | Rembane, not what I'm looking for. I'll post the link here once I come across it. |
| 2022-07-12 23:34:55 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2022-07-12 23:37:54 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 23:39:30 +0200 | Guest|38 | (~Guest|38@89.253.138.59) (Ping timeout: 240 seconds) |
| 2022-07-12 23:39:59 +0200 | jakalx | (~jakalx@base.jakalx.net) |
| 2022-07-12 23:40:03 +0200 | hpc | (~juzz@ip98-169-32-242.dc.dc.cox.net) (Ping timeout: 272 seconds) |
| 2022-07-12 23:41:04 +0200 | mmhat | (~mmh@p200300f1c7090757ee086bfffe095315.dip0.t-ipconnect.de) (Quit: WeeChat 3.5) |
| 2022-07-12 23:41:10 +0200 | <geschwindingskei> | Rembane, https://en.wikipedia.org/wiki/Structural_type_system |
| 2022-07-12 23:41:12 +0200 | <geschwindingskei> | found it. |
| 2022-07-12 23:41:18 +0200 | Guest|38 | (~Guest|38@89.253.138.59) |
| 2022-07-12 23:41:24 +0200 | <geschwindingskei> | I suppose this applies more to OCaml than Haskell though. I think. |
| 2022-07-12 23:41:43 +0200 | Guest|38 | (~Guest|38@89.253.138.59) (Client Quit) |
| 2022-07-12 23:42:10 +0200 | matthewmosior | (~matthewmo@173.170.253.91) (Ping timeout: 244 seconds) |
| 2022-07-12 23:45:25 +0200 | matthewmosior | (~matthewmo@173.170.253.91) |
| 2022-07-12 23:46:18 +0200 | indigo_ibs | (~user@31.124.106.79) (Ping timeout: 244 seconds) |
| 2022-07-12 23:50:15 +0200 | <Rembane> | geschwindingskei: Haskell has a structural type system |
| 2022-07-12 23:50:46 +0200 | <geschwindingskei> | Rembane, I see. Then that answers a lot about that datatype's definition. |
| 2022-07-12 23:50:56 +0200 | <geschwindingskei> | Car that is. |
| 2022-07-12 23:51:20 +0200 | <Rembane> | geschwindingskei: Yes. |
| 2022-07-12 23:51:30 +0200 | <geschwindingskei> | Then I can take it from here. |
| 2022-07-12 23:51:31 +0200 | <geschwindingskei> | thanks. |
| 2022-07-12 23:52:31 +0200 | <Rembane> | No worries. Good luck! :) |
| 2022-07-12 23:52:49 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) |
| 2022-07-12 23:52:55 +0200 | hsman | (~hsman@80.95.197.227) (Quit: Client closed) |
| 2022-07-12 23:55:02 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) |
| 2022-07-12 23:55:07 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2022-07-12 23:56:23 +0200 | sagax | (~sagax_nb@213.138.71.146) (Read error: Connection reset by peer) |
| 2022-07-12 23:57:47 +0200 | eggplantade | (~Eggplanta@2600:1700:bef1:5e10:9851:a856:681c:da1a) (Ping timeout: 272 seconds) |
| 2022-07-12 23:58:38 +0200 | shapr | (~user@2600:4040:2d31:7100:101e:d56a:4512:22d5) (Ping timeout: 240 seconds) |
| 2022-07-12 23:59:38 +0200 | segfaultfizzbuzz | (~segfaultf@157-131-253-58.fiber.dynamic.sonic.net) (Ping timeout: 255 seconds) |
| 2022-07-12 23:59:41 +0200 | enthropy | (~enthropy@24-246-69-9.cable.teksavvy.com) (Quit: Client closed) |