Logs: freenode/#haskell
| 2020-11-25 10:05:44 | <lambdabot> | Tonalude displayShow :: Show a => a -> Utf8Builder |
| 2020-11-25 10:05:56 | <ER> | @hoogle Utf8Builder |
| 2020-11-25 10:05:57 | <lambdabot> | RIO newtype Utf8Builder |
| 2020-11-25 10:05:57 | <lambdabot> | RIO Utf8Builder :: Builder -> Utf8Builder |
| 2020-11-25 10:05:57 | <lambdabot> | Text.Printer newtype Utf8Builder |
| 2020-11-25 10:06:23 | ← | f-a parts (~f-a@151.36.219.202) () |
| 2020-11-25 10:06:56 | × | rprije quits (~rprije@123-243-139-165.tpgi.com.au) (Quit: Leaving) |
| 2020-11-25 10:08:09 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2020-11-25 10:08:35 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2020-11-25 10:09:50 | × | n0042 quits (d055ed89@208.85.237.137) (Remote host closed the connection) |
| 2020-11-25 10:11:05 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Quit: WeeChat 2.9) |
| 2020-11-25 10:12:25 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 2020-11-25 10:15:39 | × | guest112` quits (~user@49.5.6.87) (Quit: ERC (IRC client for Emacs 27.1)) |
| 2020-11-25 10:15:45 | → | mpereira joins (~mpereira@2a02:810d:f40:d96:f587:a442:5e3:1e55) |
| 2020-11-25 10:16:05 | × | shatriff quits (~vitaliish@176.52.219.10) (Remote host closed the connection) |
| 2020-11-25 10:16:18 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 2020-11-25 10:18:25 | × | czwartyeon quits (~czwartyeo@77-45-55-99.sta.asta-net.com.pl) (Ping timeout: 240 seconds) |
| 2020-11-25 10:20:26 | × | mpereira quits (~mpereira@2a02:810d:f40:d96:f587:a442:5e3:1e55) (Ping timeout: 264 seconds) |
| 2020-11-25 10:21:10 | × | adm_ quits (~adm@43.229.88.197) (Remote host closed the connection) |
| 2020-11-25 10:25:10 | → | czwartyeon joins (~czwartyeo@77-45-55-99.sta.asta-net.com.pl) |
| 2020-11-25 10:25:13 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Remote host closed the connection) |
| 2020-11-25 10:25:36 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 2020-11-25 10:25:54 | → | Fractalis joins (~Fractalis@2601:987:280:8d40:eda9:f9e1:2072:cea7) |
| 2020-11-25 10:27:07 | → | robotadam1 joins (~robotadam@s91904426.blix.com) |
| 2020-11-25 10:29:55 | → | adm joins (~adm@43.229.88.197) |
| 2020-11-25 10:31:22 | → | alp joins (~alp@2a01:e0a:58b:4920:c9e7:a101:608d:5391) |
| 2020-11-25 10:39:53 | <trcc> | [exa]: I have a program (c-like, but with objects) Y that uses an object X. X has a certain api. I want to verify that the given program Y does not violate the API of X. And I was hoping to code-generate the program to a model checker and have the model checker verify this. |
| 2020-11-25 10:41:31 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 2020-11-25 10:41:58 | × | andos quits (~dan@69-165-210-185.cable.teksavvy.com) (Ping timeout: 246 seconds) |
| 2020-11-25 10:42:12 | <johnnyboy[m]> | sounds interesting! |
| 2020-11-25 10:42:48 | <johnnyboy[m]> | I wrote an LTL theory generator for my model checking project in Haskell and it was fun! |
| 2020-11-25 10:42:59 | × | mwalter quits (473b8f3e@c-71-59-143-62.hsd1.or.comcast.net) (Remote host closed the connection) |
| 2020-11-25 10:44:08 | <johnnyboy[m]> | haskell seems to be a great tool for parsing and generating code |
| 2020-11-25 10:44:59 | → | CMCDragonkai1 joins (~Thunderbi@124.19.3.250) |
| 2020-11-25 10:49:00 | × | Jonkimi727406120 quits (~Jonkimi@113.87.161.66) (Ping timeout: 256 seconds) |
| 2020-11-25 10:49:39 | → | pjb joins (~t@2a01cb04063ec500710c4d3951adc2aa.ipv6.abo.wanadoo.fr) |
| 2020-11-25 10:54:41 | × | CMCDragonkai1 quits (~Thunderbi@124.19.3.250) (Remote host closed the connection) |
| 2020-11-25 10:55:14 | × | adm quits (~adm@43.229.88.197) (Remote host closed the connection) |
| 2020-11-25 10:57:10 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 2020-11-25 10:57:53 | → | adm joins (~adm@43.229.88.197) |
| 2020-11-25 10:58:26 | × | adm quits (~adm@43.229.88.197) (Remote host closed the connection) |
| 2020-11-25 10:58:34 | Digit | table flips attempting to install Euterpea (cabal v1-install --allow-newer Euterpea # didnt work either) ... goes afk to calm down, and to dispell angry defeatist thoughts he'll never get coding his music in functional programming. |
| 2020-11-25 10:59:42 | → | adm joins (~adm@43.229.88.197) |
| 2020-11-25 11:00:09 | <tomsmeding> | Digit: with what ghc version did you try that? |
| 2020-11-25 11:00:35 | <tomsmeding> | I found this issue, which you probably also found (https://github.com/Euterpea/Euterpea2/issues/35), that suggests using ghc 8.6.5 |
| 2020-11-25 11:01:03 | × | mputz quits (~Thunderbi@dslb-084-058-211-084.084.058.pools.vodafone-ip.de) (Ping timeout: 256 seconds) |
| 2020-11-25 11:01:09 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 2020-11-25 11:02:14 | <Uniaika> | hi tomsmeding :) |
| 2020-11-25 11:02:46 | tomsmeding | wonders if you know me from somewhere outside #haskell |
| 2020-11-25 11:02:59 | <[exa]> | trcc: I'm usually going the other direction, write a DSL where breaking the model is non-representable and then generate the C program from that... |
| 2020-11-25 11:03:30 | <Uniaika> | tomsmeding: nope, not at all! :D |
| 2020-11-25 11:03:41 | <tomsmeding> | also hi, then :) |
| 2020-11-25 11:04:13 | × | adm quits (~adm@43.229.88.197) (Ping timeout: 260 seconds) |
| 2020-11-25 11:05:53 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds) |
| 2020-11-25 11:09:37 | × | cads quits (~cads@ip-64-72-99-232.lasvegas.net) (Ping timeout: 246 seconds) |
| 2020-11-25 11:11:58 | → | caecilius joins (~caecilius@pool-108-46-151-95.nycmny.fios.verizon.net) |
| 2020-11-25 11:19:03 | <ski> | triteraflops : Clean also has some monadic operations, because they're useful at times (avoiding tedious boilerplate code), even with uniqueness |
| 2020-11-25 11:19:45 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2020-11-25 11:20:25 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2020-11-25 11:20:47 | → | carlomagno1 joins (~cararell@148.87.23.6) |
| 2020-11-25 11:20:56 | <ski> | the Clean approach to I/O requires tracking uniqueness statically. (Mercury also uses the same approach, although it doesn't put the uniqueness in the types, but in separate mode declarations of functions and predicates). since Haskell doesn't have uniqueness, it has to use a different approach |
| 2020-11-25 11:22:45 | × | carlomagno quits (~cararell@148.87.23.7) (Ping timeout: 240 seconds) |
| 2020-11-25 11:22:51 | → | Jonkimi727406120 joins (~Jonkimi@113.87.161.66) |
| 2020-11-25 11:23:50 | <ski> | in the past (before monadic I/O), Haskell has used two other approaches to (side-effect free) I/O, modelling I/O declaratively. first, you can model a program as a function from program inputs (standard input) to program outputs (standard output), both being `String's. the standard Haskell function `interact :: (String -> String) -> IO ()' can be used to convert from that input-string-to-output-string model |
| 2020-11-25 11:23:56 | <ski> | to the current monadic I/O model, so that you can write programs in this style |
| 2020-11-25 11:24:46 | → | whald joins (~trem@2a02:810a:8100:11a6:7427:ad4:8a1e:146d) |
| 2020-11-25 11:25:01 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 2020-11-25 11:25:38 | <ski> | however, this doesn't scale to doing other operations that transforming a single standard input character stream to a single standard output character stream. e.g. you might also want to emit some output on the standard error stream. or you might want to open named files, to read from them, or write to them. or do other effectful operations, like communicating over a network |
| 2020-11-25 11:26:08 | × | ER quits (5fa448e7@95.164.72.231) (Remote host closed the connection) |
| 2020-11-25 11:27:29 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2020-11-25 11:27:46 | × | Jonkimi727406120 quits (~Jonkimi@113.87.161.66) (Ping timeout: 272 seconds) |
| 2020-11-25 11:27:48 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Client Quit) |
| 2020-11-25 11:31:04 | <ski> | so, instead of mapping lists/streams of input characters to lists/streams of output characters, we could generalize to mapping lists of OS responses to lists of OS requests (yes, in that order, not in the opposite order). you can imagine `data Request = HPutChar Handle Char | HGetChar Handle | OpenFile FilePath IOMode | HClose Handle ...' and `data Response = HCharPut | HCharGot Char | FileOpened Handle | |
| 2020-11-25 11:31:10 | <ski> | Closed | Error IOError | ...' |
| 2020-11-25 11:31:35 | → | cads joins (~cads@ip-64-72-99-232.lasvegas.net) |
| 2020-11-25 11:32:26 | <ski> | and then a program doing I/O would be modelled as a function of type `[Response] -> [Request]'. the idea is that the function starts by producing a `Request' in the output stream, and only after that does it look at the corresponding `Response' in the input stream, which will contain the reply from the OS to the given request |
| 2020-11-25 11:33:02 | <ski> | you could define a function for outputting a `String' as follows |
| 2020-11-25 11:33:21 | <ski> | hPutStr :: String -> [Response] -> [Request] |
| 2020-11-25 11:33:52 | → | Jonkimi727406120 joins (~Jonkimi@113.87.161.66) |
| 2020-11-25 11:34:41 | <ski> | hPutStr [ ] resps0 = [] |
| 2020-11-25 11:35:11 | <ski> | hPutStr (c:s) resps0 = HPutChar h c |
| 2020-11-25 11:35:21 | <Digit> | thanks tomsmeding. that was helpful. i have a 8.8.4 which i've been getting "further" with than my 8.6.5 which chokes straight away, offering "cabal: failed to parse output of 'ghc-pkg dump'". with my 8.8.4 i at least get to the https://dpaste.com/78CNMNNAU (& attempting to get alsa's -dev where i have the 8.6.5 errors out too). ~ am currently working through the errors i got, getting the parts, on a fresh start with another 8.6.5 (i |
| 2020-11-25 11:35:21 | <Digit> | hope). |
| 2020-11-25 11:35:31 | <ski> | : case resps0 of |
| 2020-11-25 11:35:48 | <dminuoso> | I do wonder how error prone pre-monadic IO really was. Forget to pop a response, pop twice.. |
| 2020-11-25 11:35:55 | <trcc> | [exa]: yes, I have thought of that. Unfortunately it is not really a possibility here... |
| 2020-11-25 11:36:08 | <ski> | HCharPut:resps -> hPutStr h c resps |
| 2020-11-25 11:36:11 | <dminuoso> | The interface seems incredibly awkward |
| 2020-11-25 11:36:33 | <ski> | (oh, there should of course also be a `Handle' argument to `hPutStr') |
| 2020-11-25 11:37:20 | <ski> | it's awkward yes to have to do local `case' in order to only check the corresponding response after the request has been given. one can use an irrefutable/lazy pattern, in order to make this a little nicer |
| 2020-11-25 11:37:43 | <ski> | hPutStr (c:s) ~(HCharPut:resps) = HPutChar h c : hPutStr h c resps |
| 2020-11-25 11:37:54 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2020-11-25 11:38:00 | <dminuoso> | Did that mechanism support things like forkIO? |
| 2020-11-25 11:38:23 | <dminuoso> | Though.. |
| 2020-11-25 11:38:43 | <dminuoso> | I guess that'd just be `forkIO :: ([Request] -> [Response]) -> [Request] -> [Response]` |
| 2020-11-25 11:38:52 | <dminuoso> | The rest is just an implementation |
| 2020-11-25 11:38:53 | <ski> | also, `hPutStr', as written above, is not composable. if one wants to output one `String' after another (and not by first concatenating them), one can't do it directly with `hPutStr'. we need to generalize it to take an additional parameter, a continuation, for what to do after the output of the given `String' : |
| 2020-11-25 11:39:03 | × | chaosmasttter quits (~chaosmast@p200300c4a7107e01f51a90bd3c8201d7.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2020-11-25 11:39:10 | <ski> | hPutStr :: Handle -> String -> ([Response] -> [Request]) -> [Response] -> [Request] |
| 2020-11-25 11:39:13 | <ski> | or, using |
All times are in UTC.