Logs on 2021-01-28 (freenode/#haskell)
| 00:00:41 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Quit: Leaving) |
| 00:00:53 | → | i_like_parmesan joins (811fa9e1@dyn1169-225.insecure.ic.ac.uk) |
| 00:01:05 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 00:01:33 | × | MVQq quits (~anja@198.254.199.42) (Quit: q) |
| 00:02:09 | → | MarcelineVQ joins (~anja@198.254.199.42) |
| 00:02:18 | × | i_like_parmesan quits (811fa9e1@dyn1169-225.insecure.ic.ac.uk) (Client Quit) |
| 00:02:20 | × | ep1ctetus quits (~epictetus@ip184-187-162-163.sb.sd.cox.net) (Ping timeout: 265 seconds) |
| 00:03:35 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 00:03:45 | × | luigy quits (~luigy@104.236.106.229) (Ping timeout: 240 seconds) |
| 00:03:54 | → | luigy_ joins (~luigy@104.236.106.229) |
| 00:04:36 | × | conal quits (~conal@64.71.133.70) (Ping timeout: 244 seconds) |
| 00:04:50 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 00:05:13 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 00:05:13 | → | ep1ctetus joins (~epictetus@ip184-187-162-163.sb.sd.cox.net) |
| 00:05:39 | × | obihann quits (~jhann@142.177.168.17) (Remote host closed the connection) |
| 00:05:56 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 240 seconds) |
| 00:06:31 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 00:06:40 | × | mputz quits (~Thunderbi@dslb-088-064-063-125.088.064.pools.vodafone-ip.de) (Ping timeout: 244 seconds) |
| 00:08:13 | × | hyperisco_ quits (~hyperisco@104-195-141-253.cpe.teksavvy.com) (Ping timeout: 260 seconds) |
| 00:08:27 | × | metreo quits (Thunderbir@gateway/vpn/mullvad/metreo) (Quit: metreo) |
| 00:08:57 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 00:09:55 | → | conal joins (~conal@66.115.157.10) |
| 00:10:07 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 272 seconds) |
| 00:10:46 | × | ep1ctetus quits (~epictetus@ip184-187-162-163.sb.sd.cox.net) (Ping timeout: 258 seconds) |
| 00:11:36 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 00:12:51 | → | sakirious5 joins (~sakirious@c-71-197-191-137.hsd1.wa.comcast.net) |
| 00:13:18 | × | sakirious quits (~sakirious@c-71-197-191-137.hsd1.wa.comcast.net) (Read error: Connection reset by peer) |
| 00:13:18 | sakirious5 | is now known as sakirious |
| 00:13:20 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 00:15:25 | × | quicksilver quits (~jules@roobarb.crazydogs.org) (Ping timeout: 240 seconds) |
| 00:16:35 | → | quicksilver joins (~jules@roobarb.crazydogs.org) |
| 00:17:27 | → | ep1ctetus joins (~epictetus@ip184-187-162-163.sb.sd.cox.net) |
| 00:18:04 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 240 seconds) |
| 00:18:10 | × | reaverb quits (~reaverb@071-008-105-088.res.spectrum.com) (Read error: Connection reset by peer) |
| 00:18:24 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 00:18:33 | → | reaverb joins (~reaverb@071-008-105-088.res.spectrum.com) |
| 00:21:47 | → | tsrt^ joins (tsrt@ip98-184-89-2.mc.at.cox.net) |
| 00:22:37 | × | sagax quits (~sagax_nb@213.138.71.146) (Ping timeout: 256 seconds) |
| 00:22:50 | × | usr25 quits (~usr25@unaffiliated/usr25) (Ping timeout: 265 seconds) |
| 00:25:44 | × | aveltras quits (uid364989@gateway/web/irccloud.com/x-nodggmoarekevuax) (Quit: Connection closed for inactivity) |
| 00:27:00 | → | metreo joins (Thunderbir@gateway/vpn/mullvad/metreo) |
| 00:28:23 | × | sm2n quits (~sm2n@bras-base-hmtnon1497w-grc-43-64-231-95-247.dsl.bell.ca) (Read error: Connection reset by peer) |
| 00:29:00 | → | sm2n joins (~sm2n@bras-base-hmtnon1497w-grc-43-64-231-95-247.dsl.bell.ca) |
| 00:30:22 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 260 seconds) |
| 00:33:09 | × | kav quits (~kari@dsl-hkibng42-56733f-225.dhcp.inet.fi) (Ping timeout: 246 seconds) |
| 00:33:19 | → | rajivr joins (uid269651@gateway/web/irccloud.com/x-uzqklzijcugoxeov) |
| 00:34:31 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 00:36:47 | → | renzhi joins (~renzhi@2607:fa49:6500:6f00::1e43) |
| 00:36:56 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 00:37:44 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 00:37:58 | × | tzlil quits (~tzlil@unaffiliated/tzlil) (Ping timeout: 260 seconds) |
| 00:39:32 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 00:40:40 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 00:41:26 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 264 seconds) |
| 00:41:44 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 260 seconds) |
| 00:42:39 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 00:44:04 | × | reaverb quits (~reaverb@071-008-105-088.res.spectrum.com) (Quit: Leaving) |
| 00:45:09 | → | kav joins (~kari@dsl-hkibng42-56733f-225.dhcp.inet.fi) |
| 00:47:28 | × | conal quits (~conal@66.115.157.10) (Ping timeout: 256 seconds) |
| 00:47:52 | → | edrx joins (~Eduardo@2804:56c:d2ec:c100:b9cf:4552:2518:d38c) |
| 00:48:03 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 264 seconds) |
| 00:49:45 | × | greymalkin quits (~greymalki@199.180.249.79) (Ping timeout: 240 seconds) |
| 00:50:34 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 00:50:49 | <edrx> | hi! a stylistical question... what would be a good way to translate the definition of "atimes" in the natural-deduction-ish tree in this image, and in the dictionary at the lower right that defines each term, to Haskell? link to the image: https://i.ibb.co/CVHK0qp/sshot.png |
| 00:52:15 | <edrx> | I am trying to use "where", but the only implementation that I got that works is a bit ugly... I on't know how to declare a variable - the "ab" - that is discharged in a lambda at the end... |
| 00:53:19 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:815b:63cc:1253:feb) (Remote host closed the connection) |
| 00:54:35 | → | greymalkin joins (~greymalki@199.180.249.79) |
| 00:54:52 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 00:55:06 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 00:55:40 | × | forgottenone quits (~forgotten@176.42.21.112) (Quit: Konversation terminated!) |
| 00:56:10 | → | conal joins (~conal@66.115.157.10) |
| 00:58:08 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 00:59:00 | × | nhs quits (~nhs@c-71-238-81-158.hsd1.or.comcast.net) (Ping timeout: 260 seconds) |
| 00:59:56 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 256 seconds) |
| 01:00:00 | <dolio> | I don't think anything good would use this many intermediate names. |
| 01:01:13 | <edrx> | good in what sense? |
| 01:01:13 | <dolio> | If you did `abtoac ab = ac` I think you'd have less of a problem with wheres, though. |
| 01:02:44 | × | matryoshka quits (~matryoshk@2606:6080:1002:8:3285:30e:de43:8809) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:02:46 | → | nhs joins (~nhs@c-71-238-81-158.hsd1.or.comcast.net) |
| 01:02:46 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 256 seconds) |
| 01:02:50 | <edrx> | I thought that every "f a = b" was translated to an "f = \ a -> b"... where can I find more about that? |
| 01:03:03 | → | matryoshka joins (~matryoshk@2606:6080:1002:8:3285:30e:de43:8809) |
| 01:03:05 | × | Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.) |
| 01:03:14 | <ski> | you could use `let' |
| 01:03:39 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 260 seconds) |
| 01:03:58 | <Axman6> | a = fst ab; b = fst ab ... why? |
| 01:04:00 | <ski> | find more, about what ? |
| 01:04:12 | <dolio> | Well, I don't know what you're trying to accomplish. But I think something that used that many intermediate names would be much less clear than e.g. the thing at the bottom of the first tree in that picture. |
| 01:04:38 | <edrx> | ok, let me explain what I am trying to accomplish. |
| 01:04:39 | <dolio> | Arguably even clearer would be `\(a,b) -> (a, f b)` |
| 01:04:47 | <ski> | presumably they want a location, in a standardized format, in the source, for each node in the proof tree ? |
| 01:05:26 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 01:05:27 | <Axman6> | edrx: f a = b is equivalent to f = \a -> b, but you asked about style, and the former is (slightly) more common |
| 01:05:49 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 01:06:13 | <Axman6> | surely `b` should be `snd ab`? |
| 01:06:40 | <edrx> | I have some proofs on Heyting Algebras with a modal operator - the ones in page 9 here: http://angg.twu.net/LATEX/2020J-ops-new.pdf - that I want to formalize in Idris at some point. But I am trying to learn Idris and I was progressing very slowly - and I realized that it would be better to learn Haskell first... |
| 01:06:46 | <Axman6> | @djinn (a,b) -> (b -> c) -> (a,c) |
| 01:06:46 | <lambdabot> | f (a, b) c = (a, c b) |
| 01:06:58 | <ski> | the natural-deduction style proof trees in Agda1 used `let ndProof0 = ...; ... in inferenceRule ndProof0 ...' in the raw source (the Alfa editor displayed a prettified, two-dimensional, version) |
| 01:07:40 | <ski> | edrx : hm, so you're learning Haskell ? or learning how to encode ND proofs in Haskell ? |
| 01:08:10 | → | frdg joins (~user@pool-96-252-123-136.bstnma.fios.verizon.net) |
| 01:08:31 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 01:08:49 | __minoru__shirae | is now known as shiraeeshi |
| 01:08:56 | <edrx> | if I find a good way to translate ND trees to Haskell or Idris in way in which each conclusion becomes a line in a let or where I can treat tress as pseudocode for Haskell - and learn bit by bit how to translate new rules that are admissible mathematically |
| 01:09:21 | <ski> | then what ? |
| 01:09:55 | <edrx> | ski: I am learning Haskell and I don't know much. I learned type systems from the mathematical side - from the formal definition of the lambda-cube, even - ages ago |
| 01:10:02 | ski | nods |
| 01:10:17 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 272 seconds) |
| 01:11:14 | <ski> | possibly the easiest way would be to have each node in the tree correspond to an expression. then you'd have \btoc -> \ab -> (fst ab,btoc (snd ab))' as your expression corresponding to the whole ND proof tree |
| 01:11:23 | × | Wuzzy quits (~Wuzzy@p549c93e5.dip0.t-ipconnect.de) (Quit: Wuzzy) |
| 01:11:51 | <frdg> | I removed the library section of my .cabal file for my stack project. I cannot build my project and I am not sure why but the error message doesn't say much and I shouldn't have and dependencies for the project yet. This is the error and my cabal file http://dpaste.com/D2VRZXLDE |
| 01:11:51 | <ski> | (if you prefer, you could insert explicit names like `andIntro',`andElim0',`andElim1',`implIntro',`implElim', and use those) |
| 01:12:13 | <frdg> | Can I not just remove the library section? |
| 01:12:34 | <ski> | edrx : but perhaps you'd prefer giving a name to each node in the proof tree ? (and so probably use either `let' or `where') |
| 01:13:00 | <Axman6> | frdg: you've said you depend on the library "arp-spoofer" buit now you have deleted the library section there is no library named that |
| 01:13:08 | <edrx> | one of my excuses (?) for learning Haskell and Idris is that I am working on a way to do Category Theory diagramatically in a way that *seems* to be easy to translate to Idris, but I don't think that it's honest to say "anyone who knows Idris well can implement this in 5 minutes" |
| 01:13:18 | <ski> | edrx : i guess it probably does make sense to learn some basic Haskell, before attempting to learn Idris |
| 01:13:30 | <frdg> | Axman6: ohh I see |
| 01:13:45 | <edrx> | ski: that's it! my names ab, a, c, btoc, etc, were just ways to name nodes of the tree... |
| 01:13:46 | <frdg> | works now thanks |
| 01:14:16 | <ski> | edrx : and you want to have these names ? or don't care too much about having them ? |
| 01:15:17 | <ski> | edrx : in any case, you will most probably have to expect to use either nested `let's or nested `where's (because of implication-introduction, and other rules that add local hypotheses) |
| 01:15:21 | → | metro joins (Thunderbir@gateway/vpn/mullvad/metreo) |
| 01:15:46 | → | vnz_ joins (~vnz@2001:bc8:604:94f::1) |
| 01:15:46 | → | lukelau_ joins (~lukelau@2a03:b0c0:1:d0::1bc:b001) |
| 01:15:47 | → | Geekingfrog_ joins (~geekingfr@li2156-64.members.linode.com) |
| 01:15:58 | → | noCheese` joins (~nocheese@gw2.aibor.de) |
| 01:16:02 | × | lukelau quits (~lukelau@2a03:b0c0:1:d0::1bc:b001) (Quit: Bye) |
| 01:16:02 | × | Geekingfrog quits (geekingfro@2a01:7e01::f03c:92ff:fe48:8bdf) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:16:02 | × | noCheese quits (~nocheese@unaffiliated/nocheese) (Write error: Broken pipe) |
| 01:16:02 | × | vnz quits (~vnz@unaffiliated/vnz) (Quit: ZNC - http://znc.in) |
| 01:16:02 | × | noan quits (~noan@2604:a880:400:d0::12fc:5001) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:16:02 | × | enikar quits (~enikar@2001:41d0:2:8673::42) (Max SendQ exceeded) |
| 01:16:02 | × | evanjs quits (~evanjs@075-129-098-007.res.spectrum.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:16:02 | × | metreo quits (Thunderbir@gateway/vpn/mullvad/metreo) (Remote host closed the connection) |
| 01:16:02 | lukelau_ | is now known as lukelau |
| 01:16:02 | noCheese` | is now known as noCheese |
| 01:16:03 | metro | is now known as metreo |
| 01:16:03 | × | noCheese quits (~nocheese@gw2.aibor.de) (Changing host) |
| 01:16:03 | → | noCheese joins (~nocheese@unaffiliated/nocheese) |
| 01:16:05 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Ping timeout: 240 seconds) |
| 01:16:11 | vnz_ | is now known as vnz |
| 01:16:15 | × | vnz quits (~vnz@2001:bc8:604:94f::1) (Changing host) |
| 01:16:15 | → | vnz joins (~vnz@unaffiliated/vnz) |
| 01:16:22 | → | enikar joins (~enikar@2001:41d0:2:8673::42) |
| 01:16:23 | × | nhs quits (~nhs@c-71-238-81-158.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 01:16:25 | → | noan joins (~noan@2604:a880:400:d0::12fc:5001) |
| 01:16:30 | → | evanjs joins (~evanjs@075-129-098-007.res.spectrum.com) |
| 01:16:30 | <ski> | with nested `let's, you'd see the code for the leaves and branches before seeing the node which they connect to. while with nested `where's, it'd be the other way around, first you see the root, then it's children, and so on |
| 01:16:35 | <edrx> | ski: yes, I found that it's MUCH easier to start by Haskell... I am reading Hutton's book and the docs of ghc and its library. I think I was able to digest everything until applicatives - I didn't go father than that yet - and this video about the core has helped a lot: http://www.youtube.com/watch?v=fty9QL4aSRc |
| 01:17:40 | <ski> | (perhaps one could do away with the nestedness, using implicit parameters ..) |
| 01:17:55 | <edrx> | ski: one of my attempts that worked used two nested wheres... I modified it and broke it, but let me reconstruct it and upload it to some pastebin. |
| 01:18:04 | <ski> | (or, i guess, explicitly passing all hypotheses to each part .. but that's a bit ugly) |
| 01:18:51 | <edrx> | ski: this looks interesting that the details are not clear to me yet =) let me reconstruct the this with two wheres, one sec... |
| 01:18:56 | <edrx> | this -> thing |
| 01:19:18 | <ski> | edrx : most probably the learning material for Idris already assumes that you know something like Haskell (or Clean, or one of the MLs, or Mercury, ..), and so it'd be harder to follow it for a newbie to statically typed functional programming languages |
| 01:20:24 | × | nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 246 seconds) |
| 01:22:12 | → | jedws joins (~jedws@121.209.139.157) |
| 01:22:24 | <ski> | atimes = implI \btoc -> |
| 01:22:44 | <ski> | implI \ab -> |
| 01:22:54 | <ski> | andI |
| 01:23:13 | <edrx> | it does. and when we do something like ":t myexpr" in the REPL the types include obscure annotation about linear types and things like this... |
| 01:23:17 | <ski> | (andElim0 ab) |
| 01:23:22 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 01:23:23 | <ski> | (implElim |
| 01:23:32 | <ski> | btoc |
| 01:23:38 | <ski> | (andElim1 ab)) |
| 01:23:49 | <ski> | is how it could look, with explicit inference rule names |
| 01:24:45 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 01:24:49 | <ski> | (you need to turn on the language extension `BlockArguments' .. or else replace the `\'s by `$ \'s) |
| 01:24:50 | × | jackk_ quits (~jackk@205.178.111.134) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 01:25:47 | <ski> | edrx : hm, yea .. it's easier to grasp the basics, without more subtle/advanced complications obscuring it |
| 01:26:54 | × | metreo quits (Thunderbir@gateway/vpn/mullvad/metreo) (Quit: metreo) |
| 01:27:02 | <ski> | (btw, if you want to, you could annotate the hypotheses, like `btoc', with their types. you could also do this for each subexpression, if you want to make it directly apparent what the types are) |
| 01:27:04 | <dolio> | This example kind of illustrates another reason to not like old-school natural deduction without contexts. |
| 01:27:22 | <edrx> | ski: I just grepped recursively the ghc source to try to find implElim and friends in the libraries, but got no matches... are they standard? |
| 01:27:35 | <ski> | dolio : you mean Prawitz-style, as opposed to Gentzen-style ? |
| 01:27:50 | <ski> | edrx : no, you'd define these yourself |
| 01:28:07 | <dolio> | I'm not sure. I mean non-hypothetical judgments instead of hypothetical judgments. |
| 01:28:09 | <edrx> | ski: what is the syntax for annotating types in a where or let? sorry for my newbieshness =) |
| 01:28:32 | <ski> | let foo :: MyType |
| 01:28:38 | <ski> | foo = myExpression |
| 01:28:42 | <ski> | in ..foo.. |
| 01:28:52 | <edrx> | ski: ok, let me try to start with your two lambdas and use a let or where in the rest! |
| 01:28:56 | <edrx> | thanks, trying! |
| 01:29:13 | <ski> | for lambdas, you can use `\(btoc :: b -> c) -> ..btoc..' |
| 01:29:35 | <dolio> | Anyhow, I'd never seen a proof where it looked like there were two places where `ab : A×B` is introduced, but it actually doesn't work that way. |
| 01:29:39 | <ski> | (but i think you need to turn on `ScopedTypeVariables', and put a type signature on your main definition, with explicit `forall's) |
| 01:30:06 | <dolio> | And you need to label them to keep track. |
| 01:30:29 | × | conal quits (~conal@66.115.157.10) (Ping timeout: 260 seconds) |
| 01:30:32 | <ski> | dolio : by "non-hypothetical judgments", you mean like ⌜Γ ⊢ e : τ⌝, yes ? |
| 01:30:41 | <dolio> | No, that is a hypothetical one. |
| 01:30:51 | <ski> | ah |
| 01:31:33 | <dolio> | Non-hypothetical is `e : τ` and you have the `[x : A]` at leaves in the tree. |
| 01:32:19 | <frdg> | I learned that `l(a) = 1 + a l(a)` can be translated into `data List a = Nil | Cons a (List a)`. So this is why they are called algebraic data types? There must be a whole class of mathematical equations that can be encoded into types then right. |
| 01:32:29 | × | deviantfero quits (~deviantfe@190.150.27.58) (Quit: WeeChat 3.0) |
| 01:32:46 | <ski> | dolio : i was thinking ⌜implI : ((⊢ x : σ) → (⊢ f x : τ)) → (⊢ λ f : σ ⇒ τ)⌝ was what you meant by "hypothetical judgments" .. but evidently not |
| 01:33:28 | <dolio> | I guess that's another meaning, yeah. I don't know what to call the other one, then. |
| 01:33:36 | <dolio> | Contextual judgments? |
| 01:34:54 | <ski> | the last ⌜implI⌝ would be to encode Prawitz-style ND .. and i guess it'd encode that, using HOAS in the meta-language |
| 01:35:14 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Quit: WeeChat 2.9) |
| 01:35:37 | × | ph88^ quits (~ph88@2a02:8109:9e00:7e5c:6c28:450f:9830:3db8) (Ping timeout: 272 seconds) |
| 01:36:46 | <edrx> | ski: first attempt, using "where"s: https://0x0.st/--gQ.txt - ghci says that ab is not known. lte me try with lets. |
| 01:37:00 | <ski> | frdg : yes, that's one reason |
| 01:37:01 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:815b:63cc:1253:feb) |
| 01:37:27 | × | Tops21 quits (~Tobias@dyndsl-095-033-088-179.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 01:37:46 | <ski> | edrx : with lambdas, you need to use `let' (or maybe implicit parameters ..). to use `where', move the lambda parameters over to the left of the `='s |
| 01:38:35 | <ski> | dolio : not really following what you meant by "Anyhow, I'd never seen a proof where ..","And you need to label them to keep track." .. |
| 01:39:26 | <ski> | anyway, what you called Non-hypothetical is Prawitz-style, and what you called hypothetical is Gentzen-style |
| 01:39:37 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 01:39:49 | <ski> | (at least i think so) |
| 01:39:51 | <edrx> | ski: works!!! https://0x0.st/--ge.txt =) |
| 01:40:27 | <ski> | edrx : if you want to, you could define `a' and `c' locally to `ac', and `b' locally to `c' |
| 01:40:45 | <ski> | (would make the nesting in the source correspond more directly to the nesting in the proof tree) |
| 01:40:58 | ← | frdg parts (~user@pool-96-252-123-136.bstnma.fios.verizon.net) ("ERC (IRC client for Emacs 27.1)") |
| 01:42:36 | <ski> | dolio : also, is "not like old-school natural deduction without contexts" to be parsed as "not like (old-school natural deduction without contexts)", or like "(not like old-school natural deduction) without contexts" ? |
| 01:43:56 | <ski> | edrx : anyway, you could add type signatures also for the local definitions inside the `where's (but you'll need `ScopedTypeVariables', and to replace the top signature by `atimes :: forall a b c. (b -> c) -> ((a,b) -> (a,c))') |
| 01:44:53 | <ski> | edrx : anyway, you can define `andIntro = (,)',`andElim0 = fst',..,`implIntro = id',`implElim = ($)',.. |
| 01:45:25 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 240 seconds) |
| 01:45:51 | → | conal joins (~conal@66.115.157.10) |
| 01:46:26 | <ski> | you could say `type Proof a = a',`type And a b = (a,b)',`type Impl a b = a -> b', and then `andIntro :: Proof a -> Proof b -> Proof (And a b)',`implIntro :: (Proof a -> Proof b) -> Proof (Impl a b)',... |
| 01:46:53 | <edrx> | ski: I'm saving that to look later!!! I took a break from working on slides for a presentation to see if could translate that tree to Haskell with some help... |
| 01:47:17 | <ski> | (makes it a little bit clearer to distinguish between object-language connectives, and meta-language ones, if that's what you want to do) |
| 01:48:03 | <ski> | you could even make a GADT, i suppose, to represent ND proofs .. but that's a bit more advanced |
| 01:48:16 | <edrx> | what is a GADT? |
| 01:48:26 | <ski> | Generalized Algebraic Data Type |
| 01:48:34 | <ski> | (it's not a good name, but we're stuck with it) |
| 01:48:39 | <edrx> | aaah, ok. yes, that's for later. |
| 01:48:53 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 01:48:55 | <edrx> | I've seen that term several times but I didn't know what it meant |
| 01:48:57 | <ski> | something like |
| 01:49:02 | <ski> | data Proof a |
| 01:49:04 | <ski> | where |
| 01:49:09 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 01:49:15 | <ski> | AndIntro :: Proof a -> Proof b -> Proof (And a b) |
| 01:49:31 | <ski> | ImplIntro :: (Proof a -> Proof b) -> Proof (Impl a b) |
| 01:49:43 | × | berberman quits (~berberman@unaffiliated/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:49:43 | <ski> | ImplElim :: Proof (Impl a b) -> Proof a -> Proof b |
| 01:50:04 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 01:50:16 | <ski> | (so, now you couldn't forget to use an explicit inference rule name) |
| 01:50:38 | × | berberman quits (~berberman@unaffiliated/berberman) (Max SendQ exceeded) |
| 01:50:52 | <ski> | edrx : in dependently typed languages, there's indexed data type families, which're close |
| 01:51:08 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 01:51:27 | → | drbean joins (~drbean@TC210-63-209-178.static.apol.com.tw) |
| 01:51:51 | × | berberman quits (~berberman@unaffiliated/berberman) (Max SendQ exceeded) |
| 01:52:23 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 01:52:48 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 01:53:32 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 246 seconds) |
| 01:54:22 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 01:58:52 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 02:00:15 | ski | . o O ( "Free variables are not “implicitly universally quantified”!" by Andrej Bauer in 2012-12-25 at <http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/> ) |
| 02:01:04 | → | fosterite joins (~fosterite@2600:6c46:7800:fecf:e869:5767:13bd:38f6) |
| 02:01:25 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 02:01:51 | × | nect quits (~nect@pool-108-11-28-155.atclnj.fios.verizon.net) (Ping timeout: 264 seconds) |
| 02:02:50 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 02:04:15 | × | stass quits (~stas@2a00:13c0:63:7195::beef) (Read error: Connection reset by peer) |
| 02:04:27 | → | stass joins (~stas@2a00:13c0:63:7195::beef) |
| 02:05:06 | <mniip> | what irks me is that we've come up with ways to "model" formal systems in various categories |
| 02:05:19 | <mniip> | and we kind of implicitly assume there is a unique canonical way to do so |
| 02:12:25 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 02:12:51 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 02:13:07 | × | viluon quits (uid453725@gateway/web/irccloud.com/x-xnconvscggfrpglm) (Quit: Connection closed for inactivity) |
| 02:17:25 | × | Zialus_PT quits (~RMF@2001:818:de63:c300:211:32ff:fe8d:ad29) (Ping timeout: 272 seconds) |
| 02:19:41 | × | notzmv quits (~user@unaffiliated/zmv) (Remote host closed the connection) |
| 02:20:36 | → | srhb_ joins (sid400352@NixOS/user/srhb) |
| 02:20:36 | → | billstclair_ joins (sid77830@gateway/web/irccloud.com/x-mfrxkjqbfrzkbhju) |
| 02:20:36 | → | jackdk_ joins (sid373013@gateway/web/irccloud.com/x-emzaacpvxlnxzzwe) |
| 02:20:58 | → | petersen_ joins (~petersen@redhat/juhp) |
| 02:21:26 | → | travv0_ joins (sid293381@gateway/web/irccloud.com/x-qfqftjhlfdqcrtoj) |
| 02:21:41 | × | billstclair quits (sid77830@gateway/web/irccloud.com/x-bwguxjeidhdnuvtl) (Ping timeout: 256 seconds) |
| 02:21:41 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Ping timeout: 256 seconds) |
| 02:21:41 | × | jackdk quits (sid373013@gateway/web/irccloud.com/x-ldrcqnejhylsiomj) (Ping timeout: 256 seconds) |
| 02:21:41 | × | travv0 quits (sid293381@gateway/web/irccloud.com/x-wunsptkywdjaiqfa) (Ping timeout: 256 seconds) |
| 02:21:41 | × | grfn quits (sid449115@gateway/web/irccloud.com/x-hmpnkfmcodinuykp) (Ping timeout: 256 seconds) |
| 02:21:41 | × | srhb quits (sid400352@NixOS/user/srhb) (Ping timeout: 256 seconds) |
| 02:21:41 | × | hazard-pointer quits (sid331723@gateway/web/irccloud.com/x-gyarisxfextwxxrz) (Ping timeout: 256 seconds) |
| 02:21:41 | × | buggymcbugfix quits (sid432603@gateway/web/irccloud.com/x-wvenlpaniptdcwgt) (Ping timeout: 256 seconds) |
| 02:21:41 | × | lightandlight quits (sid135476@gateway/web/irccloud.com/x-kezvmpubrmcupcfr) (Ping timeout: 256 seconds) |
| 02:21:41 | × | kozowu quits (uid44796@gateway/web/irccloud.com/x-ydwdkyottwyrmeyd) (Ping timeout: 256 seconds) |
| 02:21:41 | × | petersen quits (~petersen@redhat/juhp) (Read error: Connection reset by peer) |
| 02:21:41 | × | jneira quits (501ca940@gateway/web/cgi-irc/kiwiirc.com/ip.80.28.169.64) (Quit: Ping timeout (120 seconds)) |
| 02:21:41 | → | hazard-pointer joins (sid331723@gateway/web/irccloud.com/x-bhgeqiazjzcushnr) |
| 02:21:41 | × | kip quits (sid71464@gateway/web/irccloud.com/x-gxfsffsojjyrkfaj) (Ping timeout: 256 seconds) |
| 02:21:41 | × | natim87 quits (sid286962@gateway/web/irccloud.com/x-wufhxxayzbwsiryk) (Ping timeout: 256 seconds) |
| 02:21:41 | × | parisienne quits (sid383587@gateway/web/irccloud.com/x-ryqyygayfyhsbvxf) (Ping timeout: 256 seconds) |
| 02:21:41 | × | glowcoil quits (sid3405@gateway/web/irccloud.com/x-ujxwywqmvxlksmdy) (Ping timeout: 256 seconds) |
| 02:21:41 | × | graingert quits (sid128301@gateway/web/irccloud.com/x-ydtjetrdxgbtzgqe) (Ping timeout: 256 seconds) |
| 02:21:41 | × | cbarrett quits (sid192934@adium/cbarrett) (Ping timeout: 256 seconds) |
| 02:21:41 | × | agander_m quits (sid407952@gateway/web/irccloud.com/x-sjrbhxuqghzyqapd) (Ping timeout: 256 seconds) |
| 02:21:41 | × | dgpratt quits (sid193493@gateway/web/irccloud.com/x-tzymoqlnztmetlda) (Ping timeout: 256 seconds) |
| 02:21:41 | → | buggymcbugfix joins (sid432603@gateway/web/irccloud.com/x-gafwyjlsqnjdldgo) |
| 02:21:41 | → | grfn joins (sid449115@gateway/web/irccloud.com/x-osyybpyypciuphds) |
| 02:21:42 | srhb_ | is now known as srhb |
| 02:21:42 | travv0_ | is now known as travv0 |
| 02:21:47 | → | geowiesnot joins (~user@87-89-181-157.abo.bbox.fr) |
| 02:21:47 | billstclair_ | is now known as billstclair |
| 02:21:47 | jackdk_ | is now known as jackdk |
| 02:21:50 | × | ep1ctetus quits (~epictetus@ip184-187-162-163.sb.sd.cox.net) (Read error: Connection reset by peer) |
| 02:21:57 | → | kozowu joins (uid44796@gateway/web/irccloud.com/x-usimnzplijgfpzts) |
| 02:21:59 | → | lightandlight joins (sid135476@gateway/web/irccloud.com/x-pxxqueulqsacrejk) |
| 02:22:07 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 256 seconds) |
| 02:22:28 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 02:22:32 | → | dgpratt joins (sid193493@gateway/web/irccloud.com/x-snvletrnsylnvtru) |
| 02:22:33 | → | parisienne joins (sid383587@gateway/web/irccloud.com/x-vdmpszpjqvcsujym) |
| 02:22:34 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 02:22:34 | petersen_ | is now known as petersen |
| 02:22:34 | → | kip joins (sid71464@gateway/web/irccloud.com/x-mjmssaakfrgzogsh) |
| 02:22:35 | → | natim87 joins (sid286962@gateway/web/irccloud.com/x-xkprjgaacfuyoskr) |
| 02:22:35 | → | agander_m joins (sid407952@gateway/web/irccloud.com/x-vptcckfbteeecsdk) |
| 02:22:39 | → | glowcoil joins (sid3405@gateway/web/irccloud.com/x-mesuccdirfzuidoz) |
| 02:22:40 | → | cbarrett joins (sid192934@adium/cbarrett) |
| 02:23:31 | → | graingert joins (sid128301@gateway/web/irccloud.com/x-cyvyzfmycoushmou) |
| 02:24:00 | × | greymalkin quits (~greymalki@199.180.249.79) (Ping timeout: 246 seconds) |
| 02:26:09 | × | m0rphism1 quits (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) (Ping timeout: 256 seconds) |
| 02:26:36 | → | greymalkin joins (~greymalki@199.180.249.79) |
| 02:27:53 | × | conal quits (~conal@66.115.157.10) (Quit: Computer has gone to sleep.) |
| 02:28:25 | → | conal joins (~conal@66.115.157.10) |
| 02:28:36 | → | nineonine joins (~nineonine@2604:3d08:7785:9600:1d25:9d82:8276:bb69) |
| 02:30:42 | → | notzmv joins (~user@unaffiliated/zmv) |
| 02:30:57 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 02:31:22 | → | toorevitimirp joins (~tooreviti@117.182.180.218) |
| 02:31:23 | × | toorevitimirp quits (~tooreviti@117.182.180.218) (Remote host closed the connection) |
| 02:31:48 | → | toorevitimirp joins (~tooreviti@117.182.180.218) |
| 02:31:57 | × | oats quits (~hurr@durr/im/a/sheep) (Quit: until later, my friends) |
| 02:32:36 | → | oats joins (~hurr@durr/im/a/sheep) |
| 02:32:36 | → | conal_ joins (~conal@66.115.157.76) |
| 02:32:39 | <Feuermagier_> | I have a "newtype Graph n = Graph [Node n]" - if I have a function returns a graph, how can I deconstruct it to get the internal nodelist? |
| 02:33:02 | × | conal quits (~conal@66.115.157.10) (Ping timeout: 264 seconds) |
| 02:33:11 | <EvanR> | you can use pattern matching |
| 02:33:25 | <ski> | Feuermagier_ : use pattern-matching |
| 02:33:32 | × | conal_ quits (~conal@66.115.157.76) (Client Quit) |
| 02:33:48 | <ski> | Graph nodes = myGraph |
| 02:34:00 | → | Zialus joins (~RMF@199.125.37.188.rev.vodafone.pt) |
| 02:34:15 | → | conal joins (~conal@66.115.157.76) |
| 02:34:25 | <Feuermagier_> | specifically i'm trying to build a new graph: Graph (currentnode : (addNode n (Graph xs))) |
| 02:34:32 | <ski> | inside a `let' or `where', or in a parameter in a function definition (possibly a lambda expression). or use `case myGraph of Graph nodes -> ..nodes..' |
| 02:34:37 | <Feuermagier_> | addNode does however return a graph |
| 02:34:55 | <ski> | you can define an extractor function, if you want to |
| 02:34:58 | <Feuermagier_> | ski, ah, i'll try with a where |
| 02:35:12 | <ski> | getNodes (Graph nodes) = nodes |
| 02:35:31 | <ski> | if you define `newtype Graph n = Graph {getNodes :: [Node n]}', you get that automatically |
| 02:35:43 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 256 seconds) |
| 02:35:55 | <Feuermagier_> | got it |
| 02:36:00 | <Feuermagier_> | thx |
| 02:36:32 | <ski> | (btw, the intermediate brackets in `Graph (currentnode : (addNode n (Graph xs)))' are redundant) |
| 02:36:33 | <EvanR> | you can define a set of operations for your type, extract the nodes, add a node, etc |
| 02:36:58 | <Feuermagier_> | EvanR, doing that atm |
| 02:37:10 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 02:37:19 | <ski> | do you want/need to be able to operate on lists of nodes, separately from graphs ? |
| 02:37:39 | <ski> | if not, you could modify your functions that operate on lists of nodes, to instead operate on graphs |
| 02:37:50 | × | xff0x quits (~xff0x@2001:1a81:53db:3900:3a5d:5c7b:c52d:348a) (Ping timeout: 264 seconds) |
| 02:38:31 | <Feuermagier_> | ski, I'm currently implementing the internal graphworks. deconstructing the graph worked perfectly |
| 02:38:39 | <ski> | ok |
| 02:39:36 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 02:39:37 | → | xff0x joins (~xff0x@2001:1a81:520f:a600:3f55:41d8:2c0b:4a4c) |
| 02:39:58 | <ski> | when you already have an expression of your data type, it can sometimes be annoying to have to circumlocate by adding a `let' or `where' binding, giving the innards a name. that's when something like `getNodes' may be preferable |
| 02:40:46 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 02:40:46 | <ski> | (if you're doing a recursive function, it may be better to let a local worker function operate directly on the innards, to avoid excessive wrapping and unwrapping) |
| 02:40:55 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 02:41:19 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 02:42:38 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 264 seconds) |
| 02:43:14 | × | nineonine quits (~nineonine@2604:3d08:7785:9600:1d25:9d82:8276:bb69) (Ping timeout: 264 seconds) |
| 02:43:17 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 02:43:48 | → | nineonine joins (~nineonine@50.216.62.2) |
| 02:43:49 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 02:43:58 | × | conal quits (~conal@66.115.157.76) (Quit: Computer has gone to sleep.) |
| 02:44:06 | → | Tario joins (~Tario@201.192.165.173) |
| 02:44:17 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 02:45:20 | × | Zialus quits (~RMF@199.125.37.188.rev.vodafone.pt) (Ping timeout: 246 seconds) |
| 02:45:44 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 260 seconds) |
| 02:45:50 | → | Zialus joins (~RMF@2001:818:de63:c300:211:32ff:fe8d:ad29) |
| 02:48:02 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 264 seconds) |
| 02:48:11 | ← | edrx parts (~Eduardo@2804:56c:d2ec:c100:b9cf:4552:2518:d38c) ("Killed buffer") |
| 02:49:09 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 02:51:56 | → | Saukk joins (~Saukk@83-148-239-3.dynamic.lounea.fi) |
| 02:54:00 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 02:55:46 | × | j3r3my quits (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) (Remote host closed the connection) |
| 02:57:04 | × | borne quits (~fritjof@2a06:8782:ffbb:1337:fc0d:9af0:22aa:9270) (Ping timeout: 260 seconds) |
| 02:57:06 | → | rhemsuda joins (~user@2607:fea8:1e9f:d4df:48db:ef84:146e:4fc1) |
| 02:58:17 | → | j3r3my joins (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) |
| 02:58:31 | × | rhemsuda quits (~user@2607:fea8:1e9f:d4df:48db:ef84:146e:4fc1) (Remote host closed the connection) |
| 03:01:49 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 03:01:56 | → | rhemsuda joins (~user@2607:fea8:1e9f:d4df:48db:ef84:146e:4fc1) |
| 03:04:52 | × | urodna quits (~urodna@unaffiliated/urodna) (Quit: urodna) |
| 03:06:05 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 240 seconds) |
| 03:06:25 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 03:06:47 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 03:09:36 | × | drbean quits (~drbean@TC210-63-209-178.static.apol.com.tw) (Ping timeout: 240 seconds) |
| 03:10:36 | → | ep1ctetus joins (~epictetus@ip184-187-162-163.sb.sd.cox.net) |
| 03:11:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 03:11:52 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 03:13:47 | → | drbean joins (~drbean@TC210-63-209-17.static.apol.com.tw) |
| 03:16:35 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 03:24:40 | × | rhemsuda quits (~user@2607:fea8:1e9f:d4df:48db:ef84:146e:4fc1) (Remote host closed the connection) |
| 03:28:35 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Remote host closed the connection) |
| 03:28:36 | × | theDon quits (~td@94.134.91.140) (Ping timeout: 240 seconds) |
| 03:30:09 | → | gnumonic joins (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) |
| 03:30:49 | → | theDon joins (~td@94.134.91.59) |
| 03:32:12 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 03:33:31 | × | j3r3my quits (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) (Ping timeout: 256 seconds) |
| 03:35:36 | × | raym quits (~ray@45.64.220.55) (Quit: leaving) |
| 03:36:00 | → | raym joins (~ray@45.64.220.55) |
| 03:37:21 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 03:38:28 | × | Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa) |
| 03:42:02 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 264 seconds) |
| 03:42:55 | → | plutoniix joins (~q@184.82.198.91) |
| 03:44:00 | → | FinnElija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) |
| 03:44:00 | finn_elija | is now known as Guest76957 |
| 03:44:00 | FinnElija | is now known as finn_elija |
| 03:44:37 | → | xirhtogal joins (~lagothrix@unaffiliated/lagothrix) |
| 03:44:37 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Killed (kornbluth.freenode.net (Nickname regained by services))) |
| 03:44:37 | xirhtogal | is now known as lagothrix |
| 03:44:42 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving) |
| 03:47:28 | × | Guest76957 quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Ping timeout: 268 seconds) |
| 03:49:06 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 03:49:44 | → | x_ joins (~x@modemcable096.108-162-184.mc.videotron.ca) |
| 03:51:05 | × | thunderrd quits (~thunderrd@183.182.115.7) (Remote host closed the connection) |
| 03:51:21 | × | x_ quits (~x@modemcable096.108-162-184.mc.videotron.ca) (Client Quit) |
| 03:52:48 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) () |
| 03:53:01 | → | thunderrd joins (~thunderrd@183.182.115.7) |
| 03:53:05 | → | elliott__ joins (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) |
| 03:53:55 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 03:54:20 | × | slack1256 quits (~slack1256@dvc-186-186-101-190.movil.vtr.net) (Remote host closed the connection) |
| 03:55:14 | × | kupi quits (uid212005@gateway/web/irccloud.com/x-qxkumumnltldalko) (Quit: Connection closed for inactivity) |
| 03:57:37 | × | shiraeeshi quits (~shiraeesh@77.94.25.134) (Ping timeout: 244 seconds) |
| 03:58:25 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 04:00:01 | × | alexelcu quits (~alexelcu@142.93.180.198) (Quit: ZNC 1.8.2 - https://znc.in) |
| 04:00:49 | → | superstar64 joins (6ccefa7c@108-206-250-124.lightspeed.miamfl.sbcglobal.net) |
| 04:01:01 | → | alexelcu joins (~alexelcu@142.93.180.198) |
| 04:03:02 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 264 seconds) |
| 04:06:17 | × | carlomagno1 quits (~cararell@148.87.23.6) (Remote host closed the connection) |
| 04:09:39 | → | soft-warm joins (4408f588@ip68-8-245-136.sd.sd.cox.net) |
| 04:10:47 | × | hnOsmium0001 quits (uid453710@gateway/web/irccloud.com/x-mqhyhfjnzkwdmfzi) (Quit: Connection closed for inactivity) |
| 04:14:02 | → | kumo joins (~kumo@139.180.144.166) |
| 04:16:16 | × | geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 240 seconds) |
| 04:16:28 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 04:19:22 | × | Sheilong quits (uid293653@gateway/web/irccloud.com/x-vxqiqlobnwjcluux) () |
| 04:20:13 | × | deviantfero quits (~deviantfe@190.150.27.58) (Quit: WeeChat 3.0) |
| 04:23:08 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 04:24:16 | × | deviantfero quits (~deviantfe@190.150.27.58) (Client Quit) |
| 04:27:06 | → | d3od joins (~nickmeno3@78-0-98-144.adsl.net.t-com.hr) |
| 04:31:29 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 04:32:19 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 04:35:00 | × | cheater quits (~user@unaffiliated/cheater) (Ping timeout: 246 seconds) |
| 04:35:56 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 246 seconds) |
| 04:38:14 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 04:40:27 | × | fosterite quits (~fosterite@2600:6c46:7800:fecf:e869:5767:13bd:38f6) () |
| 04:40:41 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 04:43:13 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 04:45:38 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 264 seconds) |
| 04:47:08 | → | kfollstad joins (~kfollstad@23.90.89.3) |
| 04:50:10 | → | cheater joins (~user@unaffiliated/cheater) |
| 04:53:18 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 04:54:44 | → | rayyyy joins (~nanoz@gateway/tor-sasl/nanoz) |
| 04:55:27 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 04:56:02 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 04:57:37 | × | soft-warm quits (4408f588@ip68-8-245-136.sd.sd.cox.net) (Ping timeout: 248 seconds) |
| 04:57:45 | × | philopsos quits (~caecilius@gateway/tor-sasl/caecilius) (Ping timeout: 268 seconds) |
| 04:58:08 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 260 seconds) |
| 05:00:17 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 05:00:29 | × | unlink_ quits (~unlink2@p57b8511e.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 05:00:32 | × | jb55 quits (~jb55@gateway/tor-sasl/jb55) (Remote host closed the connection) |
| 05:01:46 | → | unlink2 joins (~unlink2@p200300ebcf12ea00013250d6b4625a26.dip0.t-ipconnect.de) |
| 05:01:54 | → | jb55 joins (~jb55@gateway/tor-sasl/jb55) |
| 05:04:27 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 05:04:45 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 05:04:56 | <Guest9360> | :t zip |
| 05:04:57 | <lambdabot> | [a] -> [b] -> [(a, b)] |
| 05:05:34 | <Guest9360> | :t curry |
| 05:05:35 | → | ixaxaar joins (~ixaxaar@49.207.210.215) |
| 05:05:35 | <lambdabot> | ((a, b) -> c) -> a -> b -> c |
| 05:05:41 | × | drbean quits (~drbean@TC210-63-209-17.static.apol.com.tw) (Ping timeout: 246 seconds) |
| 05:06:13 | <inkbottle> | Can we say that functions cannot be statically analyzed when inductive data type values can? Would that remotely make sense? |
| 05:07:45 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 05:08:45 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 240 seconds) |
| 05:09:02 | × | cheater quits (~user@unaffiliated/cheater) (Ping timeout: 264 seconds) |
| 05:09:15 | × | superstar64 quits (6ccefa7c@108-206-250-124.lightspeed.miamfl.sbcglobal.net) (Quit: Connection closed) |
| 05:09:50 | → | superstar64 joins (6ccefa7c@108-206-250-124.lightspeed.miamfl.sbcglobal.net) |
| 05:11:09 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 05:11:25 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 05:11:36 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 05:11:38 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Ping timeout: 246 seconds) |
| 05:12:13 | × | cheers quits (user@unaffiliated/cheers) (Ping timeout: 272 seconds) |
| 05:12:16 | → | DANtheBEASTman joins (~dysfigure@li490-89.members.linode.com) |
| 05:12:43 | × | dysfigured quits (dysfigured@2600:3c00::f03c:92ff:feb4:be75) (Ping timeout: 260 seconds) |
| 05:12:43 | × | Forkk quits (forkk@2600:3c00::f03c:91ff:fe84:de4d) (Ping timeout: 260 seconds) |
| 05:12:51 | DANtheBEASTman | is now known as dysfigured |
| 05:13:24 | → | Forkk joins (forkk@2600:3c00::f03c:91ff:fe84:de4d) |
| 05:13:38 | <inkbottle> | What makes me say that is `m >>= \x -> m'` versus `f <*> x`, the applicative form is supposed to be statically analyzable. The monadic form is said not to be analyzable, and the RHS is under a function. |
| 05:14:07 | → | jfe joins (~user@pool-71-184-149-134.bstnma.fios.verizon.net) |
| 05:14:43 | → | cheers joins (user@unaffiliated/cheers) |
| 05:16:59 | → | conal joins (~conal@192.145.117.129) |
| 05:17:26 | × | kpyke quits (~kpyke@185.204.1.185) (Remote host closed the connection) |
| 05:18:32 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 05:20:35 | × | teardown quits (~user@gateway/tor-sasl/mrush) (Ping timeout: 268 seconds) |
| 05:23:21 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 05:23:49 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 260 seconds) |
| 05:25:34 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 05:27:44 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 246 seconds) |
| 05:27:48 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 05:29:50 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 246 seconds) |
| 05:31:11 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 05:35:37 | × | jedws quits (~jedws@121.209.139.157) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 05:35:55 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 05:37:47 | × | inkbottle quits (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 05:38:16 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 05:38:35 | <glguy> | inkbottle, your "Can we say that..." statement doesn't make much sense to me. I think I understand where you're going with the second statement: we have no hope of dynamically inspecting the implementation of a function, we can only apply it to things and see what happens. As far as Applicative being somehow more static, remember that f and x in your example can be recursively defined and infinitely expandable |
| 05:39:16 | <dolio> | They could be functions. |
| 05:39:21 | × | conal quits (~conal@192.145.117.129) (Read error: Connection reset by peer) |
| 05:41:44 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 05:42:03 | <glguy> | <*> has the potential to be more "inspectable" than >>= given >>='s required use of a function |
| 05:42:24 | × | Saukk quits (~Saukk@83-148-239-3.dynamic.lounea.fi) (Remote host closed the connection) |
| 05:42:36 | <dolio> | (>>=) doesn't need to be involved, though (in principle). |
| 05:42:36 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 05:43:39 | × | elliott__ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 05:43:43 | <dolio> | It could be `m (m a) -> m a` |
| 05:44:09 | <glguy> | In that case aren't you going to drag fmap into the mix |
| 05:44:14 | <glguy> | and functions are back in play? |
| 05:44:31 | × | MrCue quits (~Mr._Cue@pengyuzhou.com) (Ping timeout: 272 seconds) |
| 05:44:52 | <glguy> | or are you saying if you limit yourself to join to get back to something potentially more "inspectable"? (if we can agree on what that word means) |
| 05:45:18 | <dolio> | No, the point is that 'join' does not lead to what people consider 'inspectable'. |
| 05:45:43 | <dolio> | But it is having nested ms that causes it, not functions. |
| 05:45:48 | <glguy> | Oh, so the point is that we can eliminate functions from the mix altogether |
| 05:46:10 | <glguy> | and keep the same statements |
| 05:46:14 | <dolio> | When you have two fs for an applicative, they are combined with a cartesian product, not nesting. |
| 05:47:03 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 272 seconds) |
| 05:47:20 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 246 seconds) |
| 05:47:21 | → | Mr_Cue joins (~Mr._Cue@pengyuzhou.com) |
| 05:47:38 | <dolio> | And if you have a cartesian product of monad things, to achieve the same thing via join, you have to put one inside the other, and that is somehow 'not inspectable'. |
| 05:47:51 | → | benjamin-l joins (~benjamin@2601:1c0:8800:67e0:fa16:54ff:febc:2e60) |
| 05:49:09 | <dolio> | But yeah, I'm saying it's not really about not being able to inspect functions. |
| 05:51:48 | → | dnlkrgr joins (~dnlkrgr@HSI-KBW-046-005-005-235.hsi8.kabel-badenwuerttemberg.de) |
| 05:54:06 | <dolio> | If you imagine it for trees, then when you do `ap`, you've duplicated the second thing at the leaves of the first thing, so you can't inspect the second thing without walking down the first thing (and you've thrown away the information that the leaves are duplicates). |
| 05:54:58 | × | benjamin-l quits (~benjamin@2601:1c0:8800:67e0:fa16:54ff:febc:2e60) (Quit: WeeChat 3.0) |
| 05:55:09 | <dolio> | Of course, the applicative behavior for trees is the same thing. |
| 05:56:28 | → | jedws joins (~jedws@121.209.139.157) |
| 05:57:02 | × | Tario quits (~Tario@201.192.165.173) (Ping timeout: 264 seconds) |
| 05:57:03 | <dolio> | Maybe I'd say a better statement is that certain sorts of static analysis require you to maintain that flat structure for observation, and thus they cannot support monad. |
| 05:57:18 | <dolio> | Because flat means you can't nest. |
| 05:58:42 | <glguy> | I'm less sure what sense we mean static now |
| 06:01:37 | → | Sgeo_ joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 06:02:25 | × | deviantfero quits (~deviantfe@190.150.27.58) (Quit: WeeChat 3.0) |
| 06:03:49 | → | shiraeeshi joins (~shiraeesh@77.94.25.134) |
| 06:04:50 | × | Sgeo quits (~Sgeo@ool-18b98aa4.dyn.optonline.net) (Ping timeout: 265 seconds) |
| 06:06:45 | → | conal joins (~conal@192.145.117.129) |
| 06:08:47 | × | noecho quits (~noecho@2a01:4f8:1c0c:80ee::4223) (Quit: ZNC - http://znc.in) |
| 06:09:17 | → | noecho joins (~noecho@2a01:4f8:1c0c:80ee::4223) |
| 06:09:32 | → | elliott__ joins (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) |
| 06:09:52 | × | d3od quits (~nickmeno3@78-0-98-144.adsl.net.t-com.hr) (Remote host closed the connection) |
| 06:10:18 | → | desophos joins (~desophos@2601:249:1680:a570:fd18:5a6e:fadb:9c36) |
| 06:18:21 | × | nineonine quits (~nineonine@50.216.62.2) (Remote host closed the connection) |
| 06:18:22 | → | Arahael joins (~arahael@61.68.77.119) |
| 06:18:51 | → | nineonine joins (~nineonine@50.216.62.2) |
| 06:19:40 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 06:23:54 | × | elliott__ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 06:24:25 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 272 seconds) |
| 06:27:38 | × | kfollstad quits (~kfollstad@23.90.89.3) (Ping timeout: 264 seconds) |
| 06:29:05 | × | nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 240 seconds) |
| 06:32:17 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 06:33:07 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:33:47 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 06:34:45 | × | dnlkrgr quits (~dnlkrgr@HSI-KBW-046-005-005-235.hsi8.kabel-badenwuerttemberg.de) (Ping timeout: 240 seconds) |
| 06:37:05 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 272 seconds) |
| 06:38:23 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 06:39:09 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 06:40:41 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 06:41:11 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 06:43:19 | <olligobber> | Anyone got advice on type level natural numbers in haskell? I've found GHC.TypeNats, but it doesn't let me do stuff like 1 :: Nat |
| 06:45:38 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 264 seconds) |
| 06:46:19 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 256 seconds) |
| 06:47:14 | → | jfe` joins (~user@pool-71-184-149-134.bstnma.fios.verizon.net) |
| 06:47:41 | Geekingfrog_ | is now known as Geekingfrog |
| 06:47:58 | × | shiraeeshi quits (~shiraeesh@77.94.25.134) (Ping timeout: 272 seconds) |
| 06:47:59 | <olligobber> | I want to generalise these types (and maybe values in those types) for arbitrary naturals, not just for the first 4 like I have now: https://github.com/olligobber/IotaBF/blob/8e830b8ad6914f8807cb0057d1c145ddc018081a/Functional/Lambda/Typed/Typed.hs#L24 |
| 06:48:39 | → | hexagoxe- joins (~hexagoxel@2a01:4f8:c0c:e::2) |
| 06:49:12 | → | conal_ joins (~conal@192.145.117.129) |
| 06:49:13 | → | grfn` joins (sid449115@gateway/web/irccloud.com/x-cqdgdcsiifgwwpcb) |
| 06:49:29 | × | conal quits (~conal@192.145.117.129) (Ping timeout: 256 seconds) |
| 06:49:29 | × | entel quits (uid256215@botters/entel) (Ping timeout: 256 seconds) |
| 06:49:29 | × | hexagoxel quits (~hexagoxel@hexagoxel.de) (Ping timeout: 256 seconds) |
| 06:49:29 | × | nckx quits (~nckx@tobias.gr) (Ping timeout: 256 seconds) |
| 06:49:29 | × | graingert quits (sid128301@gateway/web/irccloud.com/x-cyvyzfmycoushmou) (Ping timeout: 256 seconds) |
| 06:49:29 | × | grfn quits (sid449115@gateway/web/irccloud.com/x-osyybpyypciuphds) (Ping timeout: 256 seconds) |
| 06:49:30 | grfn` | is now known as grfn |
| 06:49:35 | × | natim87 quits (sid286962@gateway/web/irccloud.com/x-xkprjgaacfuyoskr) (Ping timeout: 256 seconds) |
| 06:49:35 | × | glowcoil quits (sid3405@gateway/web/irccloud.com/x-mesuccdirfzuidoz) (Ping timeout: 256 seconds) |
| 06:49:35 | × | dgpratt quits (sid193493@gateway/web/irccloud.com/x-snvletrnsylnvtru) (Ping timeout: 256 seconds) |
| 06:49:38 | hexagoxe- | is now known as hexagoxel |
| 06:49:43 | → | entel joins (uid256215@botters/entel) |
| 06:49:45 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 06:50:04 | <nshepperd> | that would work, you just need DataKinds turned on |
| 06:50:09 | × | Arahael quits (~arahael@61.68.77.119) (Ping timeout: 256 seconds) |
| 06:50:09 | × | jfe quits (~user@pool-71-184-149-134.bstnma.fios.verizon.net) (Ping timeout: 256 seconds) |
| 06:50:09 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Ping timeout: 256 seconds) |
| 06:50:09 | × | jlamothe_ quits (~jlamothe@198.251.55.207) (Ping timeout: 256 seconds) |
| 06:50:11 | → | nckx joins (~nckx@tobias.gr) |
| 06:50:29 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 06:50:31 | → | jlamothe joins (~jlamothe@198.251.55.207) |
| 06:50:36 | → | natim87 joins (sid286962@gateway/web/irccloud.com/x-bhrcuiknkqmzemun) |
| 06:50:36 | → | dgpratt joins (sid193493@gateway/web/irccloud.com/x-jvfarnvvlqexedsg) |
| 06:50:42 | → | glowcoil joins (sid3405@gateway/web/irccloud.com/x-drvtpywemyxnydlz) |
| 06:50:50 | → | Arahael joins (~arahael@61.68.77.119) |
| 06:51:01 | → | graingert joins (sid128301@gateway/web/irccloud.com/x-kgpvzuvierfgnrsi) |
| 06:51:07 | <texasmynsted> | Okay I looked at foldM |
| 06:51:57 | <texasmynsted> | what am I not seeing? My 'tsDefaultCompiler' is clearly wrong. https://gist.github.com/mmynsted/40d0d88d7fc67b69e1790c11aa95402e#gistcomment-3610646 |
| 06:52:43 | <olligobber> | nshepperd, I turned on DataKinds but still can't do 1 :: Nat, is there something I'm missing? |
| 06:53:34 | <olligobber> | btw that link I posted just moved to https://github.com/olligobber/IotaBF/blob/f6bb9b9dd8a4f46d6ddba6f5ee3c300ead08151d/Functional/Lambda/Typed.hs#L24 |
| 06:53:35 | <texasmynsted> | I need to keep binding the loadAndAppplyTemplate to the accumulator |
| 06:57:00 | <texasmynsted> | maybe I just need to call it a night |
| 06:57:31 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 07:00:36 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 07:02:30 | <nshepperd> | olligobber: what exactly does 'can't do' mean? what did you write and what error do you get? |
| 07:03:40 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 07:04:56 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 240 seconds) |
| 07:05:25 | <olligobber> | nshepperd, https://gist.github.com/olligobber/2c44f5f9b7846d914b34c361e3dd958a |
| 07:06:22 | → | Boomerang joins (~Boomerang@2a05:f6c7:2179:0:5976:80b4:6657:63a8) |
| 07:06:28 | <nshepperd> | if you just write it at the repl it will be interpreted as a term, not a type |
| 07:06:58 | <nshepperd> | try :kind 1 :: Nat |
| 07:07:32 | <olligobber> | ah, thanks! |
| 07:08:13 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 07:09:17 | → | coot joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 07:11:11 | × | Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 256 seconds) |
| 07:12:09 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 07:12:27 | → | teardown joins (~user@gateway/tor-sasl/mrush) |
| 07:12:38 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 07:13:22 | <texasmynsted> | any suggestions for me on the foldM? |
| 07:15:09 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 07:15:26 | → | nineonine joins (~nineonine@50.216.62.2) |
| 07:16:58 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 260 seconds) |
| 07:17:01 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 07:20:15 | × | nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 256 seconds) |
| 07:20:30 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 07:21:53 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 07:22:17 | → | Graf_Blutwurst joins (~grafblutw@2001:171b:226e:adc0:68cc:bd3d:def0:5db2) |
| 07:22:24 | <dibblego> | what about it? |
| 07:22:56 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 07:23:27 | → | vikid joins (~vikid@bba428846.alshamil.net.ae) |
| 07:26:01 | <texasmynsted> | howdy dibblego |
| 07:26:36 | <texasmynsted> | I am being especially dense today/tonight |
| 07:26:48 | <texasmynsted> | https://gist.github.com/mmynsted/40d0d88d7fc67b69e1790c11aa95402e |
| 07:27:13 | → | forgottenone joins (~forgotten@176.42.21.112) |
| 07:27:30 | <dibblego> | is it not compiling? |
| 07:27:47 | <texasmynsted> | I am trying to apply multiple Identifier/Strings to 'loadAndApplyTemplate' |
| 07:27:59 | → | ArConan joins (9de62a69@157.230.42.105) |
| 07:28:03 | <texasmynsted> | No compile. I will show error |
| 07:28:39 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 07:29:44 | <texasmynsted> | oops |
| 07:30:17 | <texasmynsted> | This is a different error than what I thought I had |
| 07:32:16 | × | Sgeo_ quits (~Sgeo@ool-18b98aa4.dyn.optonline.net) (Read error: Connection reset by peer) |
| 07:32:40 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 07:33:01 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 07:34:11 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 07:36:18 | <texasmynsted> | If I remove the bind to the accumulator, or what I _think_ is the accumulator, then it compiles but always produces an empty. |
| 07:37:09 | × | xff0x quits (~xff0x@2001:1a81:520f:a600:3f55:41d8:2c0b:4a4c) (Quit: xff0x) |
| 07:37:14 | × | jluttine quits (~jluttine@87-95-146-110.bb.dnainternet.fi) (Ping timeout: 264 seconds) |
| 07:37:48 | <texasmynsted> | I now am wondering if it just gives up trying to use the empty since it would process the empty first and move from left to right through the list of Identifier strings. |
| 07:38:23 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:38:46 | → | jluttine joins (~jluttine@85-23-95-149.bb.dnainternet.fi) |
| 07:39:36 | → | hololeap_ joins (~hololeap@unaffiliated/hololeap) |
| 07:40:23 | × | hololeap quits (~hololeap@unaffiliated/hololeap) (Ping timeout: 246 seconds) |
| 07:40:26 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) (Quit: zzz) |
| 07:41:29 | × | Bergle_3 quits (~Bergle_4@101.165.90.119) (Quit: Leaving) |
| 07:42:25 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 240 seconds) |
| 07:44:11 | → | hahawang joins (~Srain@222.90.67.220) |
| 07:44:40 | → | xff0x joins (~xff0x@2001:1a81:520f:a600:d38d:1006:b49a:2688) |
| 07:46:00 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 07:47:09 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 07:48:02 | × | syd quits (~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) (Ping timeout: 264 seconds) |
| 07:50:34 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 07:51:06 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 07:52:03 | → | syd joins (~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) |
| 07:52:52 | <texasmynsted> | in any case, what's new with you? |
| 07:53:36 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.0) |
| 07:53:50 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 07:55:27 | × | jedws quits (~jedws@121.209.139.157) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 07:56:17 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 08:00:32 | × | syd quits (~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 08:00:42 | → | chele joins (~chele@ip5b40237d.dynamic.kabel-deutschland.de) |
| 08:03:00 | → | dhouthoo joins (~dhouthoo@ptr-eitgbj2w0uu6delkbrh.18120a2.ip6.access.telenet.be) |
| 08:03:20 | → | Major_Biscuit joins (~Major_Bis@82-169-100-198.biz.kpn.net) |
| 08:04:16 | <texasmynsted> | Oh well. Catch you later. |
| 08:06:38 | × | revprez_1nzio quits (~revprez_a@pool-108-49-213-40.bstnma.fios.verizon.net) (Ping timeout: 246 seconds) |
| 08:07:02 | × | Feuermagier_ quits (~Feuermagi@213.178.26.41) (Quit: Leaving) |
| 08:07:35 | → | revprez_anzio joins (~revprez_a@pool-108-49-213-40.bstnma.fios.verizon.net) |
| 08:09:54 | → | thc202 joins (~thc202@unaffiliated/thc202) |
| 08:11:12 | <desophos> | hi, i'm sure there's a better way to do this but i don't know what it is. i think this is a "when all you have is an `fmap`, everything looks like an `(a -> b) -> f a -> f b`" situation. specifically, if i'm passing a `Gen [[PlayerState]]` to `playGame`, is there a less clumsy way to end up with a Gen [Int]? https://gist.github.com/desophos/edb68029593cd74f590a7a42f311d345 |
| 08:12:27 | <desophos> | thanks in advance! also, i'm a beginner, please be kind :) |
| 08:12:55 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 08:13:58 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 08:16:10 | → | coot joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 08:16:21 | <c_wraith> | fmap looks right there, assuming you have a function of type [[PlayerState]] -> Int |
| 08:16:25 | <c_wraith> | err, [Int] |
| 08:16:32 | <SIben> | desophos: I am not an expert either, but it seems canonical to me if Gen is a functor :) |
| 08:18:03 | <SIben> | Maybe you would feel it looks better using infix notation? Like "fmap f players" => "f <$> players"? |
| 08:18:13 | <c_wraith> | There are other possibilities, though |
| 08:18:21 | <ArConan> | @src read |
| 08:18:21 | <lambdabot> | read s = either error id (readEither s) |
| 08:18:23 | <desophos> | the temporary intermediate function is what feels awkward to me |
| 08:19:02 | <c_wraith> | does the temporary intermediate value in 2 * 3 + 1 feel weird to you? |
| 08:19:25 | <desophos> | haha, i guess not |
| 08:19:48 | <c_wraith> | functions are values. They can be temporary intermediate values, too :) |
| 08:19:57 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Remote host closed the connection) |
| 08:20:09 | × | totoro2022 quits (~t@unaffiliated/totoro2021) (Read error: Connection reset by peer) |
| 08:20:29 | <c_wraith> | (Note that GHC often will skip that representation if it can see it's only used once...) |
| 08:20:31 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 08:21:10 | <desophos> | ideally i would have `players` as the last argument so i could curry playGame like `playGame dilemma 3 <$> players`, which i think would work? |
| 08:21:30 | <c_wraith> | yep, that seems idiomatic |
| 08:21:51 | → | totoro2022 joins (~t@unaffiliated/totoro2021) |
| 08:21:55 | <desophos> | that's what i want haha, i guess i just need to change the argument order |
| 08:24:36 | <desophos> | yes that satisfied me, thank you |
| 08:25:27 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 08:26:33 | → | nineonine joins (~nineonine@50.216.62.2) |
| 08:26:58 | × | gnumonic quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 08:27:01 | → | coot joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 08:27:31 | → | kritzefitz joins (~kritzefit@fw-front.credativ.com) |
| 08:27:41 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 08:27:44 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 256 seconds) |
| 08:28:23 | <SIben> | I am trying to use DuplicateRecordFields & OverloadedLabels and running into a compilation error when trying to define an instance HasField x r a => IsLabel x (r -> a). Example gist is here: https://gist.github.com/bchetioui/44731bc0e4c0ce6c117ffa18c1c4890b. Could anyone help diagnose/fix? :) |
| 08:30:39 | → | ph88^ joins (~ph88@2a02:8109:9e00:7e5c:6c28:450f:9830:3db8) |
| 08:32:13 | × | nineonine quits (~nineonine@50.216.62.2) (Ping timeout: 260 seconds) |
| 08:33:03 | <lortabac> | SIben: I guess you need to give it the field symbol (getField @x) |
| 08:34:39 | <lortabac> | the type of getField is ambiguous, you always need to pass the field name |
| 08:35:16 | × | ArConan quits (9de62a69@157.230.42.105) (Quit: Connection closed) |
| 08:35:36 | → | ArConan joins (9de62a69@157.230.42.105) |
| 08:36:18 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:befe:a59d:a937:2991) (Ping timeout: 260 seconds) |
| 08:40:21 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 08:41:48 | → | knupfer joins (~Thunderbi@200116b82c7e6d00ed496df8b9d21d50.dip.versatel-1u1.de) |
| 08:42:02 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 08:42:42 | <SIben> | lortabac: hm I can not seem to get it to work like so; I am not super familiar with the label syntax, maybe I need to go back to the documentation :) Thank you |
| 08:43:10 | <lortabac> | SIben: have you enabled TypeApplications? |
| 08:44:05 | <lortabac> | you need the TypeApplications extension to use the @x syntax |
| 08:44:05 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 08:44:13 | <SIben> | I tried; fromLabel = getField @x then results in error: Not in scope: type variable ‘x’ |
| 08:44:18 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 08:44:24 | <lortabac> | oh you also need ScopedTypeVariables |
| 08:44:41 | <merijn> | Now you need ScopedTypeVariables and quickly you'll be wondering why you're making your own life so hard :p |
| 08:44:49 | <SIben> | Oh, now that works :)) |
| 08:45:07 | <SIben> | merijn: I already was, but gotta solve the problem to move on :) |
| 08:45:09 | <lortabac> | yes I agree with merijn, personally I would avoid this instance |
| 08:45:10 | <SIben> | Thanks lortabac! |
| 08:46:11 | × | conal_ quits (~conal@192.145.117.129) (Ping timeout: 246 seconds) |
| 08:46:19 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 08:46:36 | <SIben> | The cost of adding syntactic sugar seems to become very expensive very quick :) |
| 08:46:45 | → | vicfred_ joins (~vicfred@unaffiliated/vicfred) |
| 08:47:26 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 264 seconds) |
| 08:47:34 | <lortabac> | also, keep in mind that you are defining an IsLabel instance for all functions |
| 08:48:46 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:9ca:aef9:e139:13f6) |
| 08:49:01 | × | vicfred quits (~vicfred@unaffiliated/vicfred) (Ping timeout: 244 seconds) |
| 08:50:46 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 08:50:57 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Remote host closed the connection) |
| 08:51:09 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 08:51:55 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 08:52:35 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 08:55:56 | → | borne joins (~fritjof@2a06:8782:ffbb:1337:fc0d:9af0:22aa:9270) |
| 08:58:07 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 08:58:34 | × | nek0 quits (~nek0@mail.nek0.eu) (Quit: The Lounge - https://thelounge.chat) |
| 08:58:56 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 08:59:42 | → | conal joins (~conal@192.145.117.129) |
| 08:59:56 | → | niekvand_ joins (~niekvande@89.205.129.217) |
| 09:00:04 | × | rab24ack[m] quits (rab24ackma@gateway/shell/matrix.org/x-njqxbgxysiyckxsr) (Quit: Idle for 30+ days) |
| 09:00:46 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 09:01:27 | → | nathanic joins (~nathan@1429641-v106.1314-static.bltnilaa.metronetinc.net) |
| 09:03:23 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 256 seconds) |
| 09:04:23 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 09:04:40 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 09:05:52 | → | pxy joins (~pxy@45.32.132.6) |
| 09:06:49 | → | mouseghost joins (~draco@87-206-9-185.dynamic.chello.pl) |
| 09:06:49 | × | mouseghost quits (~draco@87-206-9-185.dynamic.chello.pl) (Changing host) |
| 09:06:49 | → | mouseghost joins (~draco@wikipedia/desperek) |
| 09:08:00 | → | pera joins (~pera@unaffiliated/pera) |
| 09:11:20 | → | y-combinator joins (8ac5df7a@138.197.223.122) |
| 09:11:36 | × | pxy quits (~pxy@45.32.132.6) (Quit: leaving) |
| 09:12:16 | → | nek0 joins (~nek0@mail.nek0.eu) |
| 09:12:59 | × | y-combinator quits (8ac5df7a@138.197.223.122) (Client Quit) |
| 09:13:41 | × | superstar64 quits (6ccefa7c@108-206-250-124.lightspeed.miamfl.sbcglobal.net) (Quit: Connection closed) |
| 09:14:08 | × | worc3131 quits (~quassel@2a02:c7f:dcc4:6500:217b:6c7a:eac3:3be9) (Ping timeout: 268 seconds) |
| 09:15:36 | → | dyeplexer joins (~lol@unaffiliated/terpin) |
| 09:16:14 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 09:17:07 | × | matthew- quits (~matthew@smtp.wellquite.org) (Remote host closed the connection) |
| 09:17:31 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 09:19:50 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:815b:63cc:1253:feb) (Ping timeout: 264 seconds) |
| 09:20:42 | → | heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) |
| 09:22:40 | → | andrew3 joins (~andrew@178.197.235.44) |
| 09:23:25 | × | heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 09:24:38 | × | DTZUZU quits (~DTZUZU@205.ip-149-56-132.net) (Ping timeout: 264 seconds) |
| 09:26:49 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 272 seconds) |
| 09:29:18 | → | DTZUZU joins (~DTZUZU@205.ip-149-56-132.net) |
| 09:29:34 | andrew3 | is now known as atwm |
| 09:34:29 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 09:34:31 | → | oish joins (~charlie@228.25.169.217.in-addr.arpa) |
| 09:36:56 | × | puke quits (~vroom@217.138.252.167) (Ping timeout: 240 seconds) |
| 09:37:59 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 09:40:34 | → | neiluj joins (~jco@91-167-203-101.subs.proxad.net) |
| 09:40:39 | × | neiluj quits (~jco@91-167-203-101.subs.proxad.net) (Changing host) |
| 09:40:39 | → | neiluj joins (~jco@unaffiliated/neiluj) |
| 09:42:04 | × | atwm quits (~andrew@178.197.235.44) (Quit: WeeChat 3.0) |
| 09:42:30 | → | m0rphism1 joins (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) |
| 09:42:46 | → | tatooine-sunset joins (~botond@217-197-190-248.pool.digikabel.hu) |
| 09:42:57 | → | nik joins (58823389@mue-88-130-51-137.dsl.tropolys.de) |
| 09:43:10 | × | nik quits (58823389@mue-88-130-51-137.dsl.tropolys.de) (Client Quit) |
| 09:44:50 | × | howdoi quits (uid224@gateway/web/irccloud.com/x-syubvujjpyxoxxjb) (Quit: Connection closed for inactivity) |
| 09:46:46 | → | atwm joins (~andrew@178.197.235.44) |
| 09:47:36 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 09:48:35 | <tatooine-sunset> | hi! i've recently read an article which explained free monads and showed how they can be used for dependency injection. i'm an oo programmer and i know very little haskell but my mind was blown when i understood that the author was building an ast that could be interpreted in different ways. i've heard something similar about io in haskell a while ago (building an ast which is then interpreted by |
| 09:48:41 | <tatooine-sunset> | the runtime). is this the same idea? does haskell handle io like that? is this why it can remain entirely pure (if we assume the interpreter is not part of the language)? |
| 09:49:25 | <merijn> | tatooine-sunset: "Does haskell handle IO like that?" <- well, that depends |
| 09:49:50 | <merijn> | tatooine-sunset: There are two separate things: 1) "what does IO *mean*?" and 2) "how is IO actually implemented?" |
| 09:50:31 | → | jedws joins (~jedws@121.209.139.157) |
| 09:50:49 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 09:51:39 | <merijn> | tatooine-sunset: The semantics (i.e. what does code mean) are indeed like "we separate execution of IO from evaluation of code so we have pure code constructing big IO abstractions to execute" |
| 09:51:39 | × | jedws quits (~jedws@121.209.139.157) (Client Quit) |
| 09:52:03 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 09:52:36 | <merijn> | tatooine-sunset: But that's a stupid way to implement things, the implementation only has to make sure that whatever it does has the same *behaviour* as what is meant |
| 09:53:44 | <lortabac> | IIRC Stephen Diehl's "Write you a Haskell" tutorial actually implements it that way |
| 09:53:54 | <ephemient> | if we ignore unsafePerformIO, yes you can imagine that the only thing that can evaluate IO is the runtime starting from `main` |
| 09:54:09 | <lortabac> | but it's for educational purposes |
| 09:55:08 | → | kuribas joins (~user@ptr-25vy0i8e75wmxgu7azj.18120a2.ip6.access.telenet.be) |
| 09:55:40 | <tatooine-sunset> | ok, so if i understand correctly, the code describes building the ast but for performance reasons it is implemented in a different way while preserving the semantics of the original code |
| 09:55:53 | <merijn> | tatooine-sunset: I mean, that's all a compiler is ;) |
| 09:56:12 | <merijn> | tatooine-sunset: A program that translates code into something else, while preserving the semantics of the original code |
| 09:56:14 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 09:56:29 | <tatooine-sunset> | merijn: fair enough :) |
| 09:56:37 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 09:56:49 | <merijn> | If you compile C you don't care if functions are done via call/ret or vectorised away, as long as you get the same result as what you wrote |
| 09:57:06 | → | tzlil joins (~tzlil@unaffiliated/tzlil) |
| 09:57:49 | <merijn> | tatooine-sunset: Same goes for IO. In reality the generated code will interleave evaluation and execution of IO, but as long as that interleaving doesn't have a different result you can think of your logic in terms of "using pure code to compose a huge IO action" |
| 09:59:00 | <kuribas> | And that's where C sucks, because it pretends to be like the low level model, but then still the compiler needs to translate to something else. |
| 09:59:52 | <merijn> | kuribas: It doesn't even pretend to be like the low level model :p |
| 09:59:58 | <merijn> | Unless you still have a PDP-11 :p |
| 10:00:18 | <tatooine-sunset> | thank you, this was very helpful |
| 10:01:03 | <merijn> | tatooine-sunset: If you're interested in "how does the implementation actually work" the "Lazy Functional State Threads" paper covers both IO and ST |
| 10:01:16 | <merijn> | https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45.3718&rep=rep1&type=pdf |
| 10:01:38 | <merijn> | But note that will not (directly) help you write code in a sensible way :p |
| 10:02:26 | × | toorevitimirp quits (~tooreviti@117.182.180.218) (Ping timeout: 264 seconds) |
| 10:02:38 | → | LKoen joins (~LKoen@19.175.9.109.rev.sfr.net) |
| 10:04:31 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 10:04:48 | → | Bergle_1 joins (~Bergle_4@101.165.90.119) |
| 10:08:10 | → | Rudd0 joins (~Rudd0@185.189.115.108) |
| 10:09:08 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 10:15:37 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 10:19:13 | → | niekvan__ joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 10:19:13 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Read error: Connection reset by peer) |
| 10:19:15 | × | niekvand_ quits (~niekvande@89.205.129.217) (Ping timeout: 256 seconds) |
| 10:22:13 | → | Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362) |
| 10:22:41 | → | Nahra joins (~Nahra@unaffiliated/nahra) |
| 10:24:18 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 10:24:23 | × | Codaraxis__ quits (Codaraxis@gateway/vpn/mullvad/codaraxis) (Ping timeout: 265 seconds) |
| 10:24:36 | × | gxt quits (~gxt@gateway/tor-sasl/gxt) (Ping timeout: 268 seconds) |
| 10:24:53 | × | Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 246 seconds) |
| 10:25:08 | Lord_of_Life_ | is now known as Lord_of_Life |
| 10:25:12 | × | desophos quits (~desophos@2601:249:1680:a570:fd18:5a6e:fadb:9c36) (Quit: Leaving) |
| 10:25:36 | → | danza joins (~francesco@151.53.68.90) |
| 10:25:52 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 10:27:15 | → | sramsay64[m] joins (sramsay64p@gateway/shell/matrix.org/x-jdvushtbvblurwtq) |
| 10:27:20 | → | Franciman joins (~francesco@host-95-235-155-82.retail.telecomitalia.it) |
| 10:28:19 | × | oish quits (~charlie@228.25.169.217.in-addr.arpa) (Ping timeout: 256 seconds) |
| 10:28:50 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Ping timeout: 264 seconds) |
| 10:29:40 | → | gxt joins (~gxt@gateway/tor-sasl/gxt) |
| 10:30:39 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 10:30:47 | × | johnw quits (~johnw@haskell/developer/johnw) (Ping timeout: 272 seconds) |
| 10:31:29 | → | tribly joins (~tribly@unaffiliated/tribly) |
| 10:35:00 | hololeap_ | is now known as hololeap |
| 10:35:48 | → | bitmagie joins (~Thunderbi@200116b806ad7e005d25719f6165002c.dip.versatel-1u1.de) |
| 10:36:11 | <tribly> | i'm trying to build https://hackage.haskell.org/package/pappy-0.1.0.2/reports/2 with stack, but i'm not really sure on how to do it. i've tried running "stack install --compiler=ghc-7.8.4 pappy" but it fails(?) with https://p.tribly.de/KbBU32/ |
| 10:36:11 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 10:36:25 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 10:36:34 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 10:36:38 | → | cheater joins (~user@unaffiliated/cheater) |
| 10:38:07 | <merijn> | tribly: Looks like your version of stack doesn't support ghc 7.8 |
| 10:38:46 | → | johnw joins (~johnw@haskell/developer/johnw) |
| 10:43:10 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 10:46:02 | → | jedws joins (~jedws@121.209.139.157) |
| 10:46:14 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 10:46:23 | × | bitmagie quits (~Thunderbi@200116b806ad7e005d25719f6165002c.dip.versatel-1u1.de) (Quit: bitmagie) |
| 10:46:47 | × | jedws quits (~jedws@121.209.139.157) (Client Quit) |
| 10:47:23 | → | DavidEichmann joins (~david@234.109.45.217.dyn.plus.net) |
| 10:48:09 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 256 seconds) |
| 10:50:47 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 10:53:44 | × | ArConan quits (9de62a69@157.230.42.105) (Quit: Ping timeout (120 seconds)) |
| 10:55:26 | × | hexo quits (~hexo@gateway/tor-sasl/hexo) (Ping timeout: 268 seconds) |
| 10:56:30 | → | ircbrowse_tom joins (~ircbrowse@64.225.78.177) |
| 10:56:31 | Server | sets mode +CLnt |
| 10:58:19 | × | travisb_ quits (~travisb@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Remote host closed the connection) |
| 10:58:42 | × | dorkside quits (~tdbgamer@208.190.197.222) (Quit: Ping timeout (120 seconds)) |
| 10:58:47 | → | travisb_ joins (~travisb@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 10:59:03 | <tribly> | ah, i figured it out |
| 10:59:05 | → | dorkside joins (~tdbgamer@208.190.197.222) |
| 10:59:33 | → | hexo joins (~hexo@gateway/tor-sasl/hexo) |
| 11:00:12 | → | miguel_clean joins (~Miguel@89-72-187-203.dynamic.chello.pl) |
| 11:00:33 | → | neightchan joins (~natechan@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 11:00:58 | × | natechan quits (~natechan@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 11:01:14 | × | kini quits (~kini@unaffiliated/kini) (Ping timeout: 264 seconds) |
| 11:01:52 | × | vikid quits (~vikid@bba428846.alshamil.net.ae) (Ping timeout: 256 seconds) |
| 11:02:22 | <miguel_clean> | I am using Network.HTTP.Client's managerModifyResponse hook. I would like to have the logic dependant on the Request URL this Response is related to but I can not find it anywhere in the strucutres passed to my hook. Any suggestions please? |
| 11:03:02 | → | kini joins (~kini@unaffiliated/kini) |
| 11:05:54 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Ping timeout: 268 seconds) |
| 11:06:30 | → | ADG1089__ joins (~aditya@223.236.187.18) |
| 11:07:07 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 11:09:05 | → | ArConan joins (9de62a69@157.230.42.105) |
| 11:10:49 | × | cheater quits (~user@unaffiliated/cheater) (Ping timeout: 256 seconds) |
| 11:11:10 | → | cheater joins (~user@unaffiliated/cheater) |
| 11:12:01 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 11:14:15 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 11:19:27 | × | livvy quits (~livvy@gateway/tor-sasl/livvy) (Remote host closed the connection) |
| 11:19:27 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Remote host closed the connection) |
| 11:19:40 | → | livvy joins (~livvy@gateway/tor-sasl/livvy) |
| 11:19:49 | → | fendor joins (~fendor@178.165.131.88.wireless.dyn.drei.com) |
| 11:20:47 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 11:23:02 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 11:28:01 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 11:28:39 | × | DataComputist quits (~lumeng@50.43.26.251) (Quit: Leaving...) |
| 11:32:55 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 11:35:26 | × | sveit quits (~sveit@2001:19f0:ac01:247:5400:ff:fe5c:689f) (Ping timeout: 240 seconds) |
| 11:36:05 | × | simplegauss quits (~simplegau@45.77.0.246) (Ping timeout: 240 seconds) |
| 11:36:56 | × | thonkpod quits (~thonkpod@2001:19f0:ac01:b46:5400:1ff:fec7:d73d) (Ping timeout: 244 seconds) |
| 11:37:14 | × | Nahra quits (~Nahra@unaffiliated/nahra) (Quit: leaving) |
| 11:37:46 | → | sh9 joins (~sh9@softbank060116136158.bbtec.net) |
| 11:38:34 | → | puke joins (~vroom@217.138.252.203) |
| 11:39:17 | → | thonkpod joins (~thonkpod@2001:19f0:ac01:b46:5400:1ff:fec7:d73d) |
| 11:39:26 | → | sagax joins (~sagax_nb@213.138.71.146) |
| 11:42:17 | × | rayyyy quits (~nanoz@gateway/tor-sasl/nanoz) (Ping timeout: 268 seconds) |
| 11:42:52 | × | plutoniix quits (~q@184.82.198.91) (Quit: Leaving) |
| 11:43:33 | → | sveit joins (~sveit@45.77.0.246) |
| 11:44:03 | → | simplegauss joins (~simplegau@2001:19f0:ac01:247:5400:ff:fe5c:689f) |
| 11:44:23 | × | tatooine-sunset quits (~botond@217-197-190-248.pool.digikabel.hu) (Remote host closed the connection) |
| 11:48:49 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 11:49:42 | × | niekvan__ quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Read error: Connection reset by peer) |
| 11:51:23 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 11:51:27 | × | ArConan quits (9de62a69@157.230.42.105) (Quit: Connection closed) |
| 11:51:33 | × | hahawang quits (~Srain@222.90.67.220) (Remote host closed the connection) |
| 11:53:57 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 11:57:07 | × | knupfer quits (~Thunderbi@200116b82c7e6d00ed496df8b9d21d50.dip.versatel-1u1.de) (Remote host closed the connection) |
| 11:57:16 | → | knupfer joins (~Thunderbi@200116b82c7e6d00b82cf3cf122fb0d6.dip.versatel-1u1.de) |
| 12:00:41 | → | niekvand_ joins (~niekvande@89.205.129.217) |
| 12:03:25 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 240 seconds) |
| 12:05:06 | → | jedws joins (~jedws@121.209.139.157) |
| 12:07:50 | × | m0rphism1 quits (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) (Ping timeout: 264 seconds) |
| 12:08:11 | × | jedws quits (~jedws@121.209.139.157) (Client Quit) |
| 12:09:39 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 12:14:46 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds) |
| 12:15:47 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Remote host closed the connection) |
| 12:16:00 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Remote host closed the connection) |
| 12:16:12 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 12:16:40 | × | Major_Biscuit quits (~Major_Bis@82-169-100-198.biz.kpn.net) (Ping timeout: 272 seconds) |
| 12:17:15 | → | jedws joins (~jedws@121.209.139.157) |
| 12:17:34 | <olligobber> | I tried implementing the types dependent on the Nat kind, and it seems to work, just not sure what I'm doing is the best way: https://github.com/olligobber/IotaBF/blob/7e584c22f33d33b5d9c3cf5b00e4ecec97cb74d6/Functional/Lambda/Typed.hs#L25 |
| 12:17:40 | × | teardown quits (~user@gateway/tor-sasl/mrush) (Remote host closed the connection) |
| 12:18:01 | → | teardown joins (~user@gateway/tor-sasl/mrush) |
| 12:18:15 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 12:18:29 | × | _bin quits (~bin@75-54-107-59.lightspeed.hstntx.sbcglobal.net) (Quit: ZNC - https://znc.in) |
| 12:21:17 | → | timCF joins (~i.tkachuk@m91-129-101-103.cust.tele2.ee) |
| 12:21:53 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Quit: WeeChat 3.0) |
| 12:22:02 | × | timCF quits (~i.tkachuk@m91-129-101-103.cust.tele2.ee) (Client Quit) |
| 12:23:06 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 12:23:47 | → | timCF joins (~i.tkachuk@m91-129-101-103.cust.tele2.ee) |
| 12:25:15 | → | _bin joins (~bin@2600:1700:10a1:38d0:48c6:7ef4:249:254a) |
| 12:25:40 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 12:27:21 | <olligobber> | hmm, making the type family injective is hard... |
| 12:27:50 | <timCF> | Hello, haskellers :) Any `Async` library users there? I'm looking for technique how I can reliably terminate all linked child async processes. Let's say I have process A which spawns and links async process B, which spawns and links async process C. Seems like if I apply `cancel` to A, cancellation is not propagated to B and C. How I can fix this? |
| 12:28:26 | × | borne quits (~fritjof@2a06:8782:ffbb:1337:fc0d:9af0:22aa:9270) (Quit: WeeChat 3.0) |
| 12:28:32 | × | hekkaidekapus} quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 268 seconds) |
| 12:29:01 | × | ADG1089__ quits (~aditya@223.236.187.18) (Remote host closed the connection) |
| 12:29:16 | <merijn> | timCF: use withAsync? |
| 12:29:45 | <olligobber> | hmm, using Data.Type.Boo.If didn't help haskell think it's injective.. |
| 12:29:55 | → | hekkaidekapus} joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 12:30:30 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 12:30:33 | <merijn> | timCF: link only causes child exceptions to come to the linking thread, not vice versa |
| 12:30:38 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Ping timeout: 264 seconds) |
| 12:30:48 | <merijn> | timCF: withAsync causes children to get killed when you exit the bracket |
| 12:30:57 | <merijn> | So combining both gets you what you want |
| 12:30:59 | × | jedws quits (~jedws@121.209.139.157) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 12:32:07 | → | qwertyuiop joins (5b816567@m91-129-101-103.cust.tele2.ee) |
| 12:32:24 | → | borne joins (~fritjof@200116b8641b4900438d15c340c1e8fe.dip.versatel-1u1.de) |
| 12:32:32 | → | User670 joins (ca423cb5@gateway/web/cgi-irc/kiwiirc.com/ip.202.66.60.181) |
| 12:33:04 | <User670> | Hi. I'd like to install Haskell using a standalone installer (I don't want to use a package manager), can I do that? Win 10 x64 |
| 12:35:03 | <timCF> | Thanks @merijn, I'll take a look. Being Erlang developer in the past, I'm keeping to follow Erlang architecture patterns even in Haskell, haha) |
| 12:35:26 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 12:36:34 | <idnar> | timCF: use linkOnly; link specifically ignores cancellation |
| 12:37:07 | <olligobber> | hmm, anyone know how I can take in some n :: Nat (using GHC.TypeNats) and produce a value of type TypedInput n t? If I try `(n :: Nat) -> TypedInput n t' I get an error about n having kind Nat instead of Type... |
| 12:37:33 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 12:37:43 | <merijn> | idnar: Only in the child |
| 12:37:51 | <merijn> | idnar: Which is almost certainly what you want |
| 12:38:12 | <lortabac> | olligobber: Haskell doesn't have dependent types |
| 12:38:26 | <lortabac> | you have to emulate them with GADTs (singletons) |
| 12:38:58 | <User670> | Hm, hello? I'd like to install Haskell on Windows without using a package manager; is it possible? |
| 12:39:24 | <merijn> | User670: Short answer: Not really |
| 12:39:40 | → | Major_Biscuit joins (~Major_Bis@82-169-100-198.biz.kpn.net) |
| 12:42:19 | × | dexterlb quits (~dexterlb@2a01:9e40:2:2::2) (Quit: Boing) |
| 12:42:49 | <olligobber> | I tried looking up GADTs but I don't get it |
| 12:42:56 | <olligobber> | is there an article you recommend? |
| 12:43:08 | <lortabac> | olligobber: that said, if n is known statically you can just do (Proxy :: Proxy n) -> TypedInput n t |
| 12:43:20 | <olligobber> | it is |
| 12:43:37 | <lortabac> | then you probably don't need singletons |
| 12:43:52 | → | m0rphism1 joins (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) |
| 12:44:12 | <lortabac> | sorry I meant 'Proxy n -> TypedInput n t' |
| 12:44:13 | → | dexterlb joins (~dexterlb@2a01:9e40:2:2::2) |
| 12:44:58 | <ephemient> | actually reminds me of a question... is there a reason to have a type signature with `Proxy (n :: nat)` instead of `proxy (n :: Nat)`? seems to me like it would accept (Proxy :: Proxy n) either way |
| 12:45:30 | <olligobber> | ok, now it's complaining about my type family being non-injective again |
| 12:45:48 | <idnar> | merijn: true, I was thinking of link2 |
| 12:48:48 | <olligobber> | anyone know how I can make this type family injective? https://github.com/olligobber/IotaBF/blob/7e584c22f33d33b5d9c3cf5b00e4ecec97cb74d6/Functional/Lambda/Typed.hs#L25 |
| 12:49:19 | <olligobber> | I tried just adding a type family dependency, but then the two cases overlap, and I can't figure out how to not make that the case |
| 12:51:24 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 12:51:43 | <olligobber> | maybe it's impossible and I should just give up? |
| 12:52:27 | × | timCF quits (~i.tkachuk@m91-129-101-103.cust.tele2.ee) (Quit: leaving) |
| 12:52:28 | <olligobber> | this is just to make the code more concise so I can write `input 3' instead of `free $ Just $ Just Nothing' |
| 12:52:58 | <merijn> | olligobber: Eh, that's not gonna work |
| 12:53:12 | <merijn> | olligobber: You need dependent types to turn a value level 3 into a type level Nat |
| 12:53:18 | <merijn> | Well, that or wrap it in TH |
| 12:53:36 | <olligobber> | I was gonna use a proxy, would that not do it? |
| 12:54:39 | <merijn> | Then you have to type "input (Proxy :: Proxy 3)" instead |
| 12:54:49 | <olligobber> | that's fine |
| 12:55:29 | × | pavonia quits (~user@unaffiliated/siracusa) (Quit: Bye!) |
| 12:55:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 240 seconds) |
| 12:56:15 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Read error: Connection reset by peer) |
| 12:56:37 | → | jonathanx joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 12:57:18 | <olligobber> | but I tried having input :: Proxy n -> TypedInput n t and I got an error about a type family being non-injective, and I don't know how to write it so it is injective |
| 12:57:23 | <lortabac> | olligobber: you can't force a function to be injective if it isn't |
| 12:57:30 | <olligobber> | but it is injective |
| 12:57:32 | <lortabac> | maybe the error is misleading here |
| 12:57:47 | <olligobber> | I just haven't written it in a way where it looks injective |
| 12:57:59 | <olligobber> | oh |
| 12:58:00 | <olligobber> | wait |
| 12:58:02 | <olligobber> | it isn't |
| 12:58:04 | <olligobber> | f |
| 12:58:23 | → | Aquazi joins (uid312403@gateway/web/irccloud.com/x-vgspjighzgkfvyvf) |
| 12:58:34 | × | jespada quits (~jespada@90.254.242.138) (Ping timeout: 265 seconds) |
| 12:59:12 | <olligobber> | not sure why injectivity is important, but I guess my idea won't work |
| 13:00:19 | <lortabac> | can you paste the code and the error message? |
| 13:00:33 | → | hekkaidekapus[ joins (~tchouri@gateway/tor-sasl/hekkaidekapus) |
| 13:01:41 | → | jespada joins (~jespada@90.254.242.138) |
| 13:02:16 | <olligobber> | code: https://gist.github.com/olligobber/8961972056bf2742232247e3765125c8 |
| 13:02:32 | × | ukari quits (~ukari@unaffiliated/ukari) (Remote host closed the connection) |
| 13:02:45 | <olligobber> | error: https://gist.github.com/olligobber/9394ca6368363a0c112b83eb685fd1c8 |
| 13:03:10 | × | livvy quits (~livvy@gateway/tor-sasl/livvy) (Quit: Network issue or system upgrade probably or maybe I'm testing a new kernel.) |
| 13:03:41 | × | hekkaidekapus} quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 268 seconds) |
| 13:03:45 | → | ukari joins (~ukari@unaffiliated/ukari) |
| 13:06:30 | <olligobber> | the error does suggest allowing ambiguous types, maybe I'll try that |
| 13:07:42 | → | Sheilong joins (uid293653@gateway/web/irccloud.com/x-pnpeukuovkmcsdlh) |
| 13:09:13 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Ping timeout: 272 seconds) |
| 13:09:19 | → | jonathanx_ joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 13:10:22 | × | jonathanx_ quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Client Quit) |
| 13:10:47 | → | Tario joins (~Tario@201.192.165.173) |
| 13:12:12 | <olligobber> | now I'm running into different errors... |
| 13:12:16 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 13:12:36 | → | livvy joins (~livvy@gateway/tor-sasl/livvy) |
| 13:12:53 | → | jonathanx joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 13:13:35 | <dminuoso> | olligobber: take note, that the mention of injectivity is not meant as "this is a problem" |
| 13:13:38 | <dminuoso> | It starts with NB. |
| 13:15:01 | <olligobber> | hmm, this error says `Could not deduce: TypedInput' n t v ~ TypedLambda t0 (Maybe a0) from the context: 1 <= n' |
| 13:15:03 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.0) |
| 13:15:54 | <olligobber> | I can deduce it, why can't the type checker deduce it? |
| 13:16:44 | × | livvy quits (~livvy@gateway/tor-sasl/livvy) (Remote host closed the connection) |
| 13:16:52 | → | geekosaur joins (82650c7c@130.101.12.124) |
| 13:17:11 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 13:17:41 | → | mananamenos_ joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 13:17:49 | <lortabac> | olligobber: I think what you are trying to do is possible, but probably way harder than typing a couple of 'Just's |
| 13:18:17 | <olligobber> | ok, then I think I'll keep trying |
| 13:18:28 | <olligobber> | as a learning experience |
| 13:21:21 | <lortabac> | olligobber: please remember that you can't pattern-match on 'n', so one solution may be to make 'input' a method of a type class |
| 13:21:47 | <olligobber> | so the class would be for the Nat type? |
| 13:22:04 | <lortabac> | the instances would be selected on 'n' |
| 13:22:11 | <olligobber> | right |
| 13:22:16 | → | bitmagie joins (~Thunderbi@200116b806ad7e005d25719f6165002c.dip.versatel-1u1.de) |
| 13:22:18 | <lortabac> | inductively until you meet the base case of 0 |
| 13:22:36 | <olligobber> | hard mode: base case is 1 |
| 13:22:50 | <lortabac> | oh right |
| 13:22:56 | <lortabac> | it doesn't change much |
| 13:24:49 | <olligobber> | Could not deduce (1 <=? n) ~ 'True from the context 2 <= n |
| 13:24:51 | <olligobber> | >:( |
| 13:25:16 | <lortabac> | olligobber: are you sure you need that constraint? |
| 13:25:20 | → | metreo joins (~Thunderbi@unaffiliated/metreo) |
| 13:25:32 | <olligobber> | true |
| 13:25:39 | <lortabac> | maybe for better error messages |
| 13:25:44 | <lortabac> | but you can think about that later |
| 13:26:14 | × | bitmagie quits (~Thunderbi@200116b806ad7e005d25719f6165002c.dip.versatel-1u1.de) (Client Quit) |
| 13:26:36 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 13:26:52 | <lortabac> | olligobber: also, GHC's Nat might not be the best representation, I would personally go for a Peano one |
| 13:27:15 | <lortabac> | and then provide conversions between the two |
| 13:27:18 | <olligobber> | I looked at those but there were too many options |
| 13:27:35 | <olligobber> | I went with GHC's because it was already installed |
| 13:28:06 | × | qwertyuiop quits (5b816567@m91-129-101-103.cust.tele2.ee) (Quit: Connection closed) |
| 13:28:24 | <lortabac> | @hackage fin |
| 13:28:24 | <lambdabot> | https://hackage.haskell.org/package/fin |
| 13:28:43 | <lortabac> | maybe |
| 13:29:21 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 13:29:29 | <lortabac> | I think it's doable with GHC's Nat too, but you need overlapping instances or some complicated workaround |
| 13:29:35 | <olligobber> | tbh I haven't worked out how to install packages from hackage unless they're on the aur |
| 13:29:53 | × | zaquest quits (~notzaques@5.128.210.178) (Quit: Leaving) |
| 13:31:23 | → | zaquest joins (~notzaques@5.128.210.178) |
| 13:31:38 | <olligobber> | this one is on the aur: https://hackage.haskell.org/package/finite-typelits |
| 13:31:50 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Ping timeout: 264 seconds) |
| 13:32:05 | → | urodna joins (~urodna@unaffiliated/urodna) |
| 13:32:24 | <olligobber> | wait that just uses GHC.TypeLits |
| 13:33:05 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 13:33:50 | → | tatooine-sunset joins (~botond@217-197-190-248.pool.digikabel.hu) |
| 13:34:05 | × | tatooine-sunset quits (~botond@217-197-190-248.pool.digikabel.hu) (Client Quit) |
| 13:34:15 | → | livvy joins (~livvy@gateway/tor-sasl/livvy) |
| 13:36:21 | × | renzhi quits (~renzhi@2607:fa49:6500:6f00::1e43) (Ping timeout: 272 seconds) |
| 13:36:23 | <lortabac> | olligobber: if it's an exercise you can just make one yourself |
| 13:36:34 | <olligobber> | yeah |
| 13:38:26 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 13:38:54 | → | wyer joins (~justin_wy@102-65-159-176.dsl.web.africa) |
| 13:40:14 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 264 seconds) |
| 13:42:11 | <olligobber> | ok, switched to peano nats, but I'm still getting errors, let me post them in a second |
| 13:43:01 | <olligobber> | https://gist.github.com/olligobber/3e011a6460896a76e7cd01938c0fa5c3 |
| 13:43:43 | → | pyuk joins (~vroom@217.138.252.203) |
| 13:43:46 | → | vicfred__ joins (~vicfred@unaffiliated/vicfred) |
| 13:43:46 | × | pyuk quits (~vroom@217.138.252.203) (Remote host closed the connection) |
| 13:44:28 | → | tromp_ joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 13:44:37 | → | sMuNiX joins (~sMuNiX@vlnsm8-montreal02-142-122-8-233.internet.virginmobile.ca) |
| 13:45:05 | → | hazard-pointer_ joins (sid331723@gateway/web/irccloud.com/x-hrnpdfrrezibcbfh) |
| 13:45:42 | → | buggymcbugfix_ joins (sid432603@gateway/web/irccloud.com/x-ltyciobmfcunfngz) |
| 13:45:52 | → | coot_ joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 13:45:55 | × | hazard-pointer quits (sid331723@gateway/web/irccloud.com/x-bhgeqiazjzcushnr) (Ping timeout: 256 seconds) |
| 13:45:55 | × | vicfred_ quits (~vicfred@unaffiliated/vicfred) (Read error: Connection reset by peer) |
| 13:45:55 | × | niekvand_ quits (~niekvande@89.205.129.217) (Read error: Connection reset by peer) |
| 13:45:55 | × | buggymcbugfix quits (sid432603@gateway/web/irccloud.com/x-gafwyjlsqnjdldgo) (Ping timeout: 256 seconds) |
| 13:45:55 | × | puke quits (~vroom@217.138.252.203) (Read error: Connection reset by peer) |
| 13:45:55 | → | niekvandepas joins (~niekvande@89.205.129.217) |
| 13:45:56 | buggymcbugfix_ | is now known as buggymcbugfix |
| 13:46:05 | × | sh9 quits (~sh9@softbank060116136158.bbtec.net) (Ping timeout: 256 seconds) |
| 13:46:05 | × | oats quits (~hurr@durr/im/a/sheep) (Ping timeout: 256 seconds) |
| 13:46:06 | → | Nahra joins (~Nahra@unaffiliated/nahra) |
| 13:46:11 | → | Bergle_2 joins (~Bergle_4@101.165.90.119) |
| 13:46:19 | → | oats joins (~hurr@durr/im/a/sheep) |
| 13:46:40 | × | Bergle_1 quits (~Bergle_4@101.165.90.119) (Ping timeout: 256 seconds) |
| 13:46:40 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 256 seconds) |
| 13:46:40 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Ping timeout: 256 seconds) |
| 13:46:40 | coot_ | is now known as coot |
| 13:46:58 | → | sh9 joins (~sh9@softbank060116136158.bbtec.net) |
| 13:48:18 | → | ArConan joins (9de62a69@157.230.42.105) |
| 13:50:53 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 13:53:55 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 13:54:04 | → | hyperisco joins (~hyperisco@104-195-141-253.cpe.teksavvy.com) |
| 13:56:59 | × | elliott_ quits (~elliott_@pool-108-51-101-42.washdc.fios.verizon.net) (Read error: Connection reset by peer) |
| 13:57:42 | → | elliott_ joins (~elliott_@pool-108-51-101-42.washdc.fios.verizon.net) |
| 13:58:26 | <[exa]> | anyone runs Gloss on windows? |
| 13:58:51 | <[exa]> | (scanning for possible gotchas/compatibility problems) |
| 13:59:04 | → | carlomagno joins (~cararell@148.87.23.12) |
| 13:59:07 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 14:00:37 | → | Lycurgus joins (~niemand@cpe-45-46-139-165.buffalo.res.rr.com) |
| 14:00:49 | → | Eugleo joins (5631fa78@gateway/web/cgi-irc/kiwiirc.com/ip.86.49.250.120) |
| 14:01:15 | <Eugleo> | Hey, anybody has experience with Gloss apps on WSL? Do they run? Are there any problems t watch out for? |
| 14:02:53 | × | gxt quits (~gxt@gateway/tor-sasl/gxt) (Ping timeout: 268 seconds) |
| 14:03:30 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 14:04:37 | → | gxt joins (~gxt@gateway/tor-sasl/gxt) |
| 14:05:25 | <olligobber> | maybe I should give up... |
| 14:05:45 | × | vicfred__ quits (~vicfred@unaffiliated/vicfred) (Quit: Leaving) |
| 14:06:17 | <lortabac> | olligobber: this is advanced stuff, maybe you can postpone to when you are more comfortable with these concepts |
| 14:06:51 | <olligobber> | how am I going to become comfortable with these concepts without trying to use them though? |
| 14:08:13 | × | ArConan quits (9de62a69@157.230.42.105) (Quit: Connection closed) |
| 14:08:30 | <lortabac> | fair point :) |
| 14:11:06 | <lortabac> | olligobber: I can see at least two problems in your code |
| 14:11:06 | × | niekvandepas quits (~niekvande@89.205.129.217) (Read error: Connection reset by peer) |
| 14:11:18 | <olligobber> | I would love to know where they are |
| 14:11:20 | → | niekvandepas joins (~niekvande@89.205.129.217) |
| 14:11:34 | <lortabac> | the instances are overlapping -- the second one should match 'Succ (Succ n)' |
| 14:12:44 | <fendor> | [exa], we ran a game using gloss on windows |
| 14:12:45 | <olligobber> | I get the same errors either way |
| 14:12:59 | <lortabac> | olligobber: also, 't' is ambiguous, you need to pass it through a Proxy or a type-application |
| 14:13:32 | <fendor> | everything was pretty alright, but can't remember how we actually managed to install everything properly |
| 14:14:46 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:14:50 | <olligobber> | lortabac, I implemented both those changes and get almost the same errors :( |
| 14:15:22 | <Eugleo> | fendor: And was it windows or WSL? |
| 14:15:28 | → | puke joins (~vroom@217.138.252.203) |
| 14:15:42 | <fendor> | Eugleo, iirc, it was windows |
| 14:15:54 | <fendor> | but we used stack, so maybe cygwin? |
| 14:16:01 | → | Profpatsch joins (~Profpatsc@static.88-198-193-255.clients.your-server.de) |
| 14:16:09 | <fendor> | no, stack install msys2, right? |
| 14:16:25 | <olligobber> | I have another idea... |
| 14:17:03 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 14:17:06 | <fendor> | I think you have to install opengl |
| 14:17:30 | → | berberman_ joins (~berberman@unaffiliated/berberman) |
| 14:18:09 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 14:18:09 | × | berberman quits (~berberman@unaffiliated/berberman) (Ping timeout: 272 seconds) |
| 14:18:16 | × | conal quits (~conal@192.145.117.129) (Ping timeout: 240 seconds) |
| 14:18:17 | × | berberman_ quits (~berberman@unaffiliated/berberman) (Max SendQ exceeded) |
| 14:18:57 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 14:19:52 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 14:21:24 | → | niekvand_ joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 14:21:24 | × | niekvandepas quits (~niekvande@89.205.129.217) (Read error: Connection reset by peer) |
| 14:21:37 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 260 seconds) |
| 14:21:40 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) |
| 14:23:29 | <olligobber> | it didn't work |
| 14:24:09 | <olligobber> | lortabac, are you sure this is possible? |
| 14:24:49 | → | syd joins (~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) |
| 14:25:05 | → | Tops2 joins (~Tobias@dyndsl-095-033-024-195.ewe-ip-backbone.de) |
| 14:25:14 | × | jchia__ quits (~jchia@58.32.38.49) (Ping timeout: 264 seconds) |
| 14:26:41 | → | conal joins (~conal@192.145.117.129) |
| 14:26:58 | <olligobber> | hmm, can I mix type applications with multi param type classes? |
| 14:27:03 | <lortabac> | olligobber: yes but as I said this is advanced stuff |
| 14:27:31 | <olligobber> | lortabac, do you have any tips? things I could look up that might help? |
| 14:27:33 | × | geekosaur quits (82650c7c@130.101.12.124) (Quit: Ping timeout (120 seconds)) |
| 14:27:35 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 14:28:00 | × | Lycurgus quits (~niemand@cpe-45-46-139-165.buffalo.res.rr.com) (Quit: Exeunt) |
| 14:28:24 | → | Cocytus joins (~Cocytus@cpe-76-95-48-109.socal.res.rr.com) |
| 14:28:32 | → | geekosaur joins (82650c7c@130.101.12.124) |
| 14:28:52 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 14:30:20 | → | cocytus_ joins (~cocytus@cpe-76-95-48-109.socal.res.rr.com) |
| 14:30:39 | ← | Cocytus parts (~Cocytus@cpe-76-95-48-109.socal.res.rr.com) () |
| 14:32:23 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Ping timeout: 260 seconds) |
| 14:32:53 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 14:33:48 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 14:34:10 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) |
| 14:34:12 | × | berberman quits (~berberman@unaffiliated/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 14:35:02 | × | cocytus_ quits (~cocytus@cpe-76-95-48-109.socal.res.rr.com) (Client Quit) |
| 14:35:05 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 14:35:38 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:36:18 | → | cocytus joins (~cocytus@cpe-76-95-48-109.socal.res.rr.com) |
| 14:37:23 | → | son0p joins (~son0p@181.136.122.143) |
| 14:38:26 | → | j3r3my joins (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) |
| 14:40:50 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 14:41:15 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 14:42:25 | → | jackk_ joins (~jackk@205.178.111.134) |
| 14:43:41 | × | Nahra quits (~Nahra@unaffiliated/nahra) (Quit: leaving) |
| 14:44:46 | × | dexterlb quits (~dexterlb@2a01:9e40:2:2::2) (Quit: Boing) |
| 14:45:23 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 272 seconds) |
| 14:46:32 | × | raym quits (~ray@45.64.220.55) (Quit: leaving) |
| 14:46:46 | → | raym joins (~ray@45.64.220.55) |
| 14:47:25 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 14:47:51 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 14:49:06 | × | Eugleo quits (5631fa78@gateway/web/cgi-irc/kiwiirc.com/ip.86.49.250.120) (Quit: Connection closed) |
| 14:52:44 | <[exa]> | fendor: good thanks. I guess installing the gl sdk is not a hard problem |
| 14:53:31 | × | geekosaur quits (82650c7c@130.101.12.124) (Quit: Connection closed) |
| 14:54:42 | → | shiraeeshi joins (~shiraeesh@77.94.25.134) |
| 14:56:03 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 14:56:59 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 14:58:06 | → | dexterlb joins (~dexterlb@2a01:9e40:2:2::2) |
| 15:01:23 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 15:02:24 | → | lukaswilkeer joins (b3438f77@179-67-143-119.user3p.veloxzone.com.br) |
| 15:03:45 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 15:04:12 | → | Tario joins (~Tario@201.192.165.173) |
| 15:04:18 | <olligobber> | I just had an idea |
| 15:04:23 | <olligobber> | ugh better try it now |
| 15:05:25 | → | Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 15:06:22 | × | denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Remote host closed the connection) |
| 15:06:40 | → | denisse joins (~spaceCat@gateway/tor-sasl/alephzer0) |
| 15:11:40 | <lukaswilkeer> | Can someone explain the map function annotation? In that case, receives a list (a->b), proceeds to a list [a] resulting a list of [b]. But map is a function whereas apply a to b, so, what is the list [a]? You need to know about how map works to comprehend the annotation, and the second parameter, [a], as a resulting of a(b), so on [b(a) | b <- b). |
| 15:11:40 | <lukaswilkeer> | Or there's a meaning about in this? |
| 15:12:04 | <lukaswilkeer> | ops, [a(b) | b <- b] |
| 15:12:30 | × | jackk_ quits (~jackk@205.178.111.134) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 15:15:22 | <merijn> | lukaswilkeer: (a->b) is not a list... ? |
| 15:15:32 | <lukaswilkeer> | it's a function |
| 15:16:03 | <lukaswilkeer> | receives a function as a first parameter an b as a list. |
| 15:16:19 | → | flatmap joins (~flatmap@p200300dd373b2a0018f40ccf4f078e3d.dip0.t-ipconnect.de) |
| 15:16:27 | <merijn> | I can't understand that sentence |
| 15:16:28 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 15:16:40 | <ephemient> | I can't understand you either. do you mean [a->b] -> [a] -> [b]? |
| 15:17:13 | → | coot joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 15:17:25 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:17:44 | <lukaswilkeer> | yep, but this is a map function annotation. :info map (a->b) -> [a] -> [b], where (a->b) is a function wich receives two parameters. |
| 15:17:46 | <olligobber> | wtf it worked |
| 15:18:23 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Read error: Connection reset by peer) |
| 15:18:43 | → | jonathanx joins (~jonathan@h-176-109.A357.priv.bahnhof.se) |
| 15:18:43 | <shiraeeshi> | function (a -> b) receives one parameter |
| 15:18:46 | <ephemient> | if type b = x -> y, then you're using map :: (a -> x -> y) -> [a] -> [x -> y], which is fine |
| 15:18:58 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 15:19:04 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 15:19:13 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 15:19:27 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 15:19:53 | <lukaswilkeer> | on that case, [a] is a list o f(x) function where's the image is a response to the o map, after this, they converge to a list of result, that are [b]. |
| 15:20:23 | <lukaswilkeer> | rigth? |
| 15:20:36 | <merijn> | I don't think anyone can answer that question |
| 15:20:50 | <ephemient> | I cannot parse your statement |
| 15:22:02 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 15:22:56 | <lukaswilkeer> | where is a set witch is the resulting process of parsing map(a.b), translating, f(b), or a(b), result on another set on the group, that is another set, [b] wich is a result of the primarily set of functors. |
| 15:23:10 | → | Sh4rPEYE joins (~textual@2a02:8308:388:aa00:c445:300:dc4e:194f) |
| 15:23:44 | <lukaswilkeer> | category theory, sets. concret math. so this function(i mean, the annotation) makes total sense |
| 15:24:07 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 256 seconds) |
| 15:24:08 | → | rayyyy joins (~nanoz@gateway/tor-sasl/nanoz) |
| 15:24:54 | <lukaswilkeer> | *the resulting (image) of the first set |
| 15:26:03 | <lukaswilkeer> | every set posses a image, this is, set theory. |
| 15:26:52 | <kuribas> | If I have: data A = AA Int | AB Int, could it be coerced to data B = BA (Sum Int) | BB (Sum Int) ? |
| 15:27:08 | <ephemient> | it doesn't make a great deal of sense here as lists are not sets... but sure, if you want to think about it like that... |
| 15:27:27 | <ephemient> | in a sense, the type doesn't tell you that such is the behavior; `map _ _ = []` would satisfy the type signature as well (but it would be rather useless) |
| 15:27:39 | <ephemient> | @djinn (a -> b) -> [a] -> [b] |
| 15:27:39 | <lambdabot> | Error: Undefined type [] |
| 15:27:54 | <ephemient> | oh I guess djinn can't do magic |
| 15:28:22 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 15:28:56 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 15:29:07 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 15:29:41 | <lukaswilkeer> | kuribas using? You have a type(I think a struct) that can be coerced(applying transformations to the data, wich is function composition) resulting in BA | BB |
| 15:29:57 | <lukaswilkeer> | lambda calculus |
| 15:30:16 | <lukaswilkeer> | right? |
| 15:31:11 | <kuribas> | sure I can write a function to do that |
| 15:31:23 | <kuribas> | I was wondering if it could be coerced, using "coerce" |
| 15:31:23 | <lukaswilkeer> | ok, that's it. |
| 15:32:09 | <kuribas> | I am probably micro-optimizing though.. |
| 15:32:17 | <ephemient> | kuribas: alternately, if you defined `data C x = CA x | CB x` then you could `coerce :: C Int -> C (Sum Int)` |
| 15:32:44 | <kuribas> | I could, but they are in a different module... |
| 15:33:03 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Ping timeout: 260 seconds) |
| 15:33:51 | <lukaswilkeer> | coerce :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b, by the annotation you can to that. I saw on the hoogle. |
| 15:35:11 | <merijn> | kuribas: "no" |
| 15:35:14 | × | knupfer quits (~Thunderbi@200116b82c7e6d00b82cf3cf122fb0d6.dip.versatel-1u1.de) (Remote host closed the connection) |
| 15:35:15 | → | brightly-salty[m joins (brightly-s@gateway/shell/matrix.org/x-aarthkmmqveerxer) |
| 15:35:19 | <merijn> | kuribas: You can't coerce datatypes |
| 15:35:22 | → | knupfer joins (~Thunderbi@200116b82c7e6d00f93273791f4c549b.dip.versatel-1u1.de) |
| 15:35:38 | <merijn> | kuribas: You could unsafeCoerce them, but, eh...good luck with that :p |
| 15:35:39 | → | jchia__ joins (~jchia@jungle.jchia.net) |
| 15:35:44 | <lukaswilkeer> | on that case, the resulting type is a Int |
| 15:36:03 | <lukaswilkeer> | *an |
| 15:36:10 | <kuribas> | merijn: coerce is only for newtypes right? |
| 15:36:16 | <merijn> | Yeah |
| 15:36:48 | <merijn> | kuribas: If you had "data A a = AA a | AB a" you could coerce from "A Int" to "A (Sum Int)" |
| 15:37:26 | <kuribas> | because that coerces the newtypes |
| 15:37:32 | <kuribas> | not a data type into another data type |
| 15:37:51 | <merijn> | right |
| 15:37:52 | <olligobber> | lortabac, I did it |
| 15:38:16 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:38:17 | × | conal quits (~conal@192.145.117.129) (Ping timeout: 256 seconds) |
| 15:38:49 | <lukaswilkeer> | @mer |
| 15:38:49 | <lambdabot> | Maybe you meant: vera msg more metar let arr |
| 15:39:09 | <lortabac> | olligobber: nice, what did you do? |
| 15:39:39 | <olligobber> | lortabac, made my type family injective |
| 15:39:49 | <olligobber> | lortabac, by making the base case use Void |
| 15:39:55 | × | jchia__ quits (~jchia@jungle.jchia.net) (Remote host closed the connection) |
| 15:40:05 | <lukaswilkeer> | @mergin "you could coerce from "A Int" to "A (Sum Int)" that's is what i'm talking. |
| 15:40:05 | <lambdabot> | Unknown command, try @list |
| 15:40:18 | <lukaswilkeer> | i have to left the group, so, thanks you all |
| 15:40:29 | × | lukaswilkeer quits (b3438f77@179-67-143-119.user3p.veloxzone.com.br) (Quit: Connection closed) |
| 15:40:33 | <olligobber> | I'll push the code soon |
| 15:40:45 | × | rayyyy quits (~nanoz@gateway/tor-sasl/nanoz) (Remote host closed the connection) |
| 15:41:06 | → | rayyyy joins (~nanoz@gateway/tor-sasl/nanoz) |
| 15:41:27 | <olligobber> | it would be nicer if I could type 0,1,2,... instead of Zero, Succ Zero, Succ (Succ Zero), ... |
| 15:42:46 | <lortabac> | olligobber: that's a simple feature to add |
| 15:42:54 | <kuribas> | olligobber: you can write a Num instance |
| 15:42:58 | × | User670 quits (ca423cb5@gateway/web/cgi-irc/kiwiirc.com/ip.202.66.60.181) (Quit: Connection closed) |
| 15:43:05 | <olligobber> | kuribas, it isn't a type |
| 15:43:11 | <olligobber> | wait |
| 15:43:16 | <olligobber> | it is a type, it isn't a term |
| 15:43:21 | <olligobber> | Zero :: Type |
| 15:43:30 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 15:43:31 | <kuribas> | oh... |
| 15:45:11 | <shiraeeshi> | you can programmatically generate source code to represent numbers as types |
| 15:45:16 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 15:45:34 | <shiraeeshi> | like data MyNumbers = One | Two | Three | etc. |
| 15:45:34 | <olligobber> | sounds hacky |
| 15:46:02 | <merijn> | I have an easier solution :) |
| 15:46:19 | <merijn> | Give up on trying to use Haskell as a dependently typed language :p |
| 15:46:31 | <olligobber> | merijn, I was about to do that, but then I didn't |
| 15:46:50 | <merijn> | olligobber: I, too, often make poor life choices ;) |
| 15:47:45 | <kuribas> | merijn: why try a simple solution, when you can make life hard (and typesafe)? |
| 15:48:26 | <olligobber> | my old solution was typesafe, but also involved many nested Justs and Maybes |
| 15:48:38 | tdammers | almost reinvented linear types badly in haskell |
| 15:49:08 | <ephemient> | have you ever thought, binary numbers are too efficient |
| 15:49:18 | <tdammers> | in the end, though, I settled on wrapping values in MVars, and throwing runtime exceptions when finding them empty |
| 15:49:36 | → | rdivyanshu joins (uid322626@gateway/web/irccloud.com/x-lnncqkpdqnzwrber) |
| 15:50:17 | → | soft-warm joins (4408f588@ip68-8-245-136.sd.sd.cox.net) |
| 15:51:13 | <shiraeeshi> | tdammers, what was the use case? |
| 15:51:15 | <olligobber> | do I just make a type family to convert Nat to my types? |
| 15:51:26 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 15:51:39 | <tdammers> | shiraeeshi: deterministic deallocation |
| 15:52:15 | <tdammers> | shiraeeshi: specifically, storing secrets in mlocked RAM, and then "forgetting" them securely by overwriting the locked RAM with zeroes before unlocking it |
| 15:53:17 | <lortabac> | olligobber: yes |
| 15:53:21 | <tdammers> | ideally, I would have wanted a setup where a context in which a reference is "valid" (i.e., allocated and mlocked) has a different type than one where it has been erased and unlocked |
| 15:53:54 | → | d3od joins (~nickmeno3@78-0-98-144.adsl.net.t-com.hr) |
| 15:54:41 | → | conal joins (~conal@192.145.117.129) |
| 15:55:31 | <shiraeeshi> | tdammers, so you filled memory with zeros before releasing an MVar? |
| 15:55:50 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 264 seconds) |
| 15:56:00 | <tdammers> | the MVar is just there to signal validity |
| 15:56:20 | <tdammers> | it holds a raw C pointer to a block of mlocked memory |
| 15:56:35 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.0) |
| 15:56:39 | <shiraeeshi> | oh, I think I need to refresh my memory about how MVars work |
| 15:56:40 | <tdammers> | or rather, a ForeignPtr |
| 15:57:15 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 15:57:17 | <tdammers> | the ForeignPtr has a finalizer that erases the memory before unlocking and freeing it |
| 15:57:22 | <tdammers> | so that part is fine |
| 15:57:50 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 15:57:56 | <tdammers> | but the way finalizers work, the raw pointer would still be accessible after the finalizer has run, so we need to prevent that from happening |
| 15:57:57 | <olligobber> | lortabac, yeet |
| 15:58:07 | × | atwm quits (~andrew@178.197.235.44) (Ping timeout: 256 seconds) |
| 15:58:15 | → | sayola joins (~vekto@dslb-002-201-085-014.002.201.pools.vodafone-ip.de) |
| 15:58:39 | <tdammers> | hence, we put it in an MVar. when we allocate the memory, we put it in an MVar; and when we deallocate it, we first take it out of the MVar, and from that point on, it is no longer accessible to any other code |
| 15:59:54 | <olligobber> | wait it still doesn't work? |
| 16:00:22 | <olligobber> | oh no |
| 16:00:36 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 16:02:00 | × | knupfer quits (~Thunderbi@200116b82c7e6d00f93273791f4c549b.dip.versatel-1u1.de) (Quit: knupfer) |
| 16:04:50 | → | jchia__ joins (~jchia@58.32.38.49) |
| 16:05:03 | <olligobber> | ok I have yet another idea |
| 16:07:43 | → | cr3 joins (~cr3@192-222-143-195.qc.cable.ebox.net) |
| 16:11:46 | → | klausgena joins (~user@ip-62-235-175-179.dsl.scarlet.be) |
| 16:12:36 | × | strangeglyph quits (~strangegl@boreeas.net) (Quit: User terminated) |
| 16:12:44 | → | nineonine joins (~nineonine@2604:3d08:7785:9600:5538:6d40:d5d9:f8a6) |
| 16:13:38 | → | ubert joins (~Thunderbi@p200300ecdf25d950e6b318fffe838f33.dip0.t-ipconnect.de) |
| 16:13:52 | <olligobber> | I sleep and figure this out tomorrow |
| 16:14:03 | × | xff0x quits (~xff0x@2001:1a81:520f:a600:d38d:1006:b49a:2688) (Ping timeout: 272 seconds) |
| 16:14:04 | × | JunoTrix quits (~Junotrix@90.221.74.173) (Ping timeout: 240 seconds) |
| 16:14:15 | × | nineonine quits (~nineonine@2604:3d08:7785:9600:5538:6d40:d5d9:f8a6) (Remote host closed the connection) |
| 16:14:41 | → | xff0x joins (~xff0x@2001:1a81:520f:a600:96af:82c9:7615:9820) |
| 16:16:50 | × | berberman quits (~berberman@unaffiliated/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 16:17:21 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 16:17:48 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 16:18:53 | → | nineonine joins (~nineonine@2604:3d08:7785:9600:5538:6d40:d5d9:f8a6) |
| 16:21:28 | × | niekvand_ quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Read error: Connection reset by peer) |
| 16:22:23 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 260 seconds) |
| 16:22:29 | × | Sh4rPEYE quits (~textual@2a02:8308:388:aa00:c445:300:dc4e:194f) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 16:22:35 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 246 seconds) |
| 16:22:36 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 16:23:04 | × | nineonine quits (~nineonine@2604:3d08:7785:9600:5538:6d40:d5d9:f8a6) (Ping timeout: 240 seconds) |
| 16:24:06 | × | finn_elija quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Quit: finn_elija) |
| 16:25:01 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 16:26:45 | × | natim87 quits (sid286962@gateway/web/irccloud.com/x-bhrcuiknkqmzemun) (Ping timeout: 240 seconds) |
| 16:26:57 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 16:27:07 | → | natim87 joins (sid286962@gateway/web/irccloud.com/x-kdprozyavblxdjvv) |
| 16:27:20 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 16:29:17 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 16:30:02 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 16:31:23 | → | Quivver joins (~Quivver@90.221.74.173) |
| 16:32:07 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 256 seconds) |
| 16:32:29 | × | mouseghost quits (~draco@wikipedia/desperek) (Quit: mew wew) |
| 16:33:28 | → | hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-obbamytoysiptieo) |
| 16:36:54 | × | ep1ctetus quits (~epictetus@ip184-187-162-163.sb.sd.cox.net) (Read error: Connection reset by peer) |
| 16:37:17 | × | jbetz quits (sid283648@gateway/web/irccloud.com/x-uicdxgcisyukzace) (Read error: Connection reset by peer) |
| 16:37:21 | × | amatecha__ quits (sid10006@gateway/web/irccloud.com/x-vxhybhzhmzrloeom) (Read error: Connection reset by peer) |
| 16:37:23 | × | moobar quits (sid171730@gateway/web/irccloud.com/x-rlawjbnutexbmbgm) (Read error: Connection reset by peer) |
| 16:37:27 | → | jbetz joins (sid283648@gateway/web/irccloud.com/x-uzbrvncunhpksqyc) |
| 16:37:29 | × | drupol quits (sid117588@gateway/web/irccloud.com/x-taxejniqfymjmivt) (Ping timeout: 272 seconds) |
| 16:37:33 | → | moobar joins (sid171730@gateway/web/irccloud.com/x-ddlgralqoxtibhbj) |
| 16:37:35 | × | topos quits (sid467876@gateway/web/irccloud.com/x-sihzqcktpapeemrw) (Read error: Connection reset by peer) |
| 16:37:47 | → | topos joins (sid467876@gateway/web/irccloud.com/x-dbccdihuivdjslyq) |
| 16:37:47 | × | jlpeters quits (sid25606@gateway/web/irccloud.com/x-qlrrxljjcptcncpm) (Read error: Connection reset by peer) |
| 16:38:03 | → | jlpeters joins (sid25606@gateway/web/irccloud.com/x-sgprjlxzuwmmyvui) |
| 16:38:03 | → | drupol joins (sid117588@gateway/web/irccloud.com/x-kjvismejvnpqwehu) |
| 16:38:12 | → | amatecha__ joins (sid10006@gateway/web/irccloud.com/x-fnkwtebeukswlkmi) |
| 16:38:25 | × | son0p quits (~son0p@181.136.122.143) (Quit: leaving) |
| 16:39:09 | → | son0p joins (~son0p@181.136.122.143) |
| 16:39:33 | × | kritzefitz quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection) |
| 16:41:36 | × | thunderrd quits (~thunderrd@183.182.115.7) (Remote host closed the connection) |
| 16:41:57 | → | plutoniix joins (~q@node-ug8.pool-125-24.dynamic.totinternet.net) |
| 16:42:52 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 16:43:50 | × | conal quits (~conal@192.145.117.129) (Ping timeout: 264 seconds) |
| 16:44:07 | × | chele quits (~chele@ip5b40237d.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 16:46:42 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 16:49:08 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 16:49:32 | <kuribas> | why does ghc warn about "unused constructor", when a constructor is mandatory? |
| 16:51:09 | → | alx741 joins (~alx741@186.178.110.213) |
| 16:52:38 | <hc> | kuribas: could ye paste the code somewhere, please? |
| 16:52:51 | <kuribas> | hc: sure |
| 16:53:40 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 16:54:03 | <kuribas> | hc: https://github.com/kuribas/hasqlator-mysql/blob/main/src/Database/MySQL/Hasqlator/Typed.hs |
| 16:55:26 | × | klausgena quits (~user@ip-62-235-175-179.dsl.scarlet.be) (Ping timeout: 240 seconds) |
| 16:55:27 | → | geekosaur joins (82650c7c@130.101.12.124) |
| 16:56:11 | → | nineonine joins (~nineonine@2604:3d08:7785:9600:5538:6d40:d5d9:f8a6) |
| 16:56:33 | <hc> | which line? |
| 16:57:24 | <kuribas> | hc: https://github.com/kuribas/hasqlator-mysql/blob/main/src/Database/MySQL/Hasqlator/Typed.hs#L102 |
| 16:58:53 | × | zar quits (~zar@fw1.ciirc.cvut.cz) (Quit: Leaving) |
| 16:59:06 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 16:59:10 | <hc> | looks to me like the data constructor is neither used nor exported |
| 16:59:21 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 16:59:56 | <geekosaur> | and ghc isn't smart enough to count `coerce` as a use |
| 17:00:06 | <hc> | and neither am I ;) |
| 17:00:11 | <kuribas> | hc: I don't want to export it |
| 17:00:13 | <geekosaur> | (remember that `coerce` is magical) |
| 17:00:23 | <hc> | btw, http://www.resonata.be/ (linked on your github page) looks kinda broken to me |
| 17:00:24 | × | _bin quits (~bin@2600:1700:10a1:38d0:48c6:7ef4:249:254a) (Quit: ZNC - https://znc.in) |
| 17:01:05 | <kuribas> | hc: it *is* broken |
| 17:01:26 | × | nineonine quits (~nineonine@2604:3d08:7785:9600:5538:6d40:d5d9:f8a6) (Ping timeout: 240 seconds) |
| 17:02:23 | → | _bin joins (~bin@2600:1700:10a1:38d0:29a8:1bef:481c:a3c1) |
| 17:02:39 | × | deviantfero quits (~deviantfe@190.150.27.58) (Ping timeout: 265 seconds) |
| 17:04:34 | → | cocytus_ joins (~cocytus@cpe-76-95-48-109.socal.res.rr.com) |
| 17:05:15 | <hc> | Okay, I had never heard of coerce. Looks useful enough |
| 17:05:19 | → | Tops21 joins (~Tobias@dyndsl-095-033-024-195.ewe-ip-backbone.de) |
| 17:05:55 | → | rcdilorenzo joins (~rcdiloren@62.182.99.136) |
| 17:06:02 | → | jeremym joins (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) |
| 17:06:23 | <kuribas> | very useful, I wish I knew about it earlier |
| 17:06:52 | → | royal_screwup219 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 17:07:00 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) |
| 17:07:02 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Read error: Connection reset by peer) |
| 17:07:02 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Ping timeout (120 seconds)) |
| 17:07:02 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 256 seconds) |
| 17:07:02 | × | shiraeeshi quits (~shiraeesh@77.94.25.134) (Remote host closed the connection) |
| 17:07:07 | → | Rudd0^ joins (~Rudd0@185.189.115.108) |
| 17:07:11 | → | shiraeeshi joins (~shiraeesh@77.94.25.134) |
| 17:07:14 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) (Remote host closed the connection) |
| 17:07:38 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) |
| 17:07:41 | × | _bin quits (~bin@2600:1700:10a1:38d0:29a8:1bef:481c:a3c1) (Quit: ZNC - https://znc.in) |
| 17:07:50 | × | plutoniix quits (~q@node-ug8.pool-125-24.dynamic.totinternet.net) (Ping timeout: 256 seconds) |
| 17:07:50 | × | j3r3my quits (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) (Ping timeout: 256 seconds) |
| 17:07:50 | × | cocytus quits (~cocytus@cpe-76-95-48-109.socal.res.rr.com) (Ping timeout: 256 seconds) |
| 17:07:50 | × | Tops2 quits (~Tobias@dyndsl-095-033-024-195.ewe-ip-backbone.de) (Ping timeout: 256 seconds) |
| 17:08:15 | → | plutoniix joins (~q@node-ug8.pool-125-24.dynamic.totinternet.net) |
| 17:08:16 | → | atwm joins (~andrew@19-193-28-81.ftth.cust.kwaoo.net) |
| 17:08:27 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 17:08:44 | → | _bin joins (~bin@75-54-107-59.lightspeed.hstntx.sbcglobal.net) |
| 17:09:36 | <ph88^> | is there any way i can choose the resolver from the command line when doing stack install ? |
| 17:10:22 | <tdammers> | --resolver, off the top of my head |
| 17:10:30 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 17:10:35 | <geekosaur> | that's my recollection as well |
| 17:11:40 | <ph88^> | hmm strange i found that now in the guide .. but didn't see it when i did stack install --help or stack build --help |
| 17:11:42 | <geekosaur> | may not work if installing a package with its own `stack.yaml` that specifies a different one, that is `stack install` with no args |
| 17:11:53 | <ph88^> | maybe i should open a ticket for that that it is missing in the help |
| 17:12:08 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 17:13:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:16:35 | <merijn> | We still don't have a nice pretty formatting function/library for numbers, do we? >.> |
| 17:16:45 | → | Sh4rPEYE joins (~textual@2a02:8308:388:aa00:c445:300:dc4e:194f) |
| 17:17:07 | <maerwald> | one more thing you can do after your thesis |
| 17:17:23 | × | Boomerang quits (~Boomerang@2a05:f6c7:2179:0:5976:80b4:6657:63a8) (Ping timeout: 272 seconds) |
| 17:17:32 | <ProofTechnique> | https://hackage.haskell.org/package/format-numbers-0.1.0.1/docs/Data-Text-Format-Numbers.html? |
| 17:17:43 | <merijn> | maerwald: But I want it to help explore the results :( |
| 17:18:28 | <merijn> | ah, that might work |
| 17:19:00 | <merijn> | Probably not very fast, though xD |
| 17:19:16 | × | Major_Biscuit quits (~Major_Bis@82-169-100-198.biz.kpn.net) (Ping timeout: 240 seconds) |
| 17:20:42 | × | Graf_Blutwurst quits (~grafblutw@2001:171b:226e:adc0:68cc:bd3d:def0:5db2) (Quit: WeeChat 3.0) |
| 17:21:20 | → | juuandyy joins (~juuandyy@90.106.228.121) |
| 17:24:47 | → | nineonine joins (~nineonine@2604:3d08:7785:9600:1d25:9d82:8276:bb69) |
| 17:25:12 | <Sh4rPEYE> | Hey, anybody here with experience with Purescript / Elm who would want to chime in in this discussion? |
| 17:25:27 | <Sh4rPEYE> | https://www.reddit.com/r/purescript/comments/l70qjn/which_one_of_purescript_elm_and_reason_is_most/ |
| 17:25:56 | <Sh4rPEYE> | (Teacher looking for an ideal FP language to base a course on) |
| 17:26:14 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 17:27:00 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 17:27:37 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Remote host closed the connection) |
| 17:27:52 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 17:28:08 | × | royal_screwup219 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 17:28:30 | → | royal_screwup219 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 17:31:14 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds) |
| 17:31:49 | → | conal joins (~conal@192.145.117.109) |
| 17:38:00 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 17:38:14 | × | ChaiTRex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Remote host closed the connection) |
| 17:38:54 | → | ChaiTRex joins (~ChaiTRex@gateway/tor-sasl/chaitrex) |
| 17:42:24 | × | conal quits (~conal@192.145.117.109) (Ping timeout: 256 seconds) |
| 17:43:41 | → | nineonin_ joins (~nineonine@50.216.62.2) |
| 17:44:22 | × | Jesin quits (~Jesin@pool-72-66-101-18.washdc.fios.verizon.net) (Quit: Leaving) |
| 17:45:35 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 17:46:25 | × | mananamenos quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 256 seconds) |
| 17:46:29 | × | pera quits (~pera@unaffiliated/pera) (Quit: leaving) |
| 17:47:27 | × | nineonine quits (~nineonine@2604:3d08:7785:9600:1d25:9d82:8276:bb69) (Ping timeout: 260 seconds) |
| 17:47:58 | × | rayyyy quits (~nanoz@gateway/tor-sasl/nanoz) (Ping timeout: 268 seconds) |
| 17:48:25 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 17:48:46 | <texasmynsted> | Sh4rPEYE: If you are creating a course I would use Haskell or Racket |
| 17:49:23 | → | jmchael joins (~jmchael@87.112.235.234) |
| 17:49:40 | <kuribas> | scheme is very nice |
| 17:49:43 | → | Varis joins (~Tadas@unaffiliated/varis) |
| 17:49:49 | <maerwald> | Elm sounds like a good fit of the course is about web dev |
| 17:50:00 | <kuribas> | because the core language is very small, but you can explain many concepts from it. |
| 17:50:08 | <texasmynsted> | While Purescript and Elm are both great in practice, a course should be focused on the important things not implementation details. |
| 17:50:29 | <texasmynsted> | yes, scheme is great |
| 17:50:35 | <maerwald> | being productive is important |
| 17:50:44 | <maerwald> | especially in practical courses |
| 17:50:50 | → | Jesin joins (~Jesin@pool-72-66-101-18.washdc.fios.verizon.net) |
| 17:51:09 | <texasmynsted> | I think people can be very productive using haskell. |
| 17:51:21 | <maerwald> | not as fast |
| 17:51:42 | <texasmynsted> | "not as fast"? |
| 17:51:53 | <texasmynsted> | I do not believe that. |
| 17:52:07 | <maerwald> | then you have never taught it |
| 17:53:18 | <kuribas> | maerwald: not as fast productive? |
| 17:53:40 | <maerwald> | yeah, compared to elm |
| 17:53:47 | <texasmynsted> | People are simply learning the important stuff. Learning is work. |
| 17:53:47 | <maerwald> | especially in web dev |
| 17:54:02 | texasmynsted | shrug |
| 17:54:25 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 17:54:26 | <koz_> | What maerwald says is 100% the problem with 'the web'. |
| 17:54:28 | <texasmynsted> | If it is web dev then I suppose a web specific language would be useful |
| 17:54:46 | <koz_> | It's all a mountain of trash built atop other trash, because nobody cares about anything but 'forall X build X in 5 minutes'. |
| 17:54:53 | <texasmynsted> | It depends on the mission of your class |
| 17:55:45 | → | conal joins (~conal@192.145.117.109) |
| 17:56:00 | <texasmynsted> | Write code in seconds may sell classes but does not make for good code |
| 17:56:17 | <maerwald> | did you read the reddit thread? |
| 17:56:18 | <texasmynsted> | Python is a good example |
| 17:56:21 | <geekosaur> | nobody on the web cares about good code |
| 17:56:26 | <texasmynsted> | no I did not |
| 17:56:36 | <koz_> | texasmynsted: I dunno if you were here at the time, but there was someone in here 100% saying 'acshually, Haskell is bad because you have to write good code in it'. |
| 17:56:47 | <maerwald> | well, there are specific requirements |
| 17:56:51 | <koz_> | (no seriously his argument amounted to 'people want to write garbage and we should let them') |
| 17:56:55 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 17:57:03 | <koz_> | geekosaur: Truth right there, lizard bro. |
| 17:57:23 | <texasmynsted> | That is exactly what is wrong with development |
| 17:57:56 | <koz_> | 'Worse is better' is a hell of a drug. |
| 17:58:17 | <maerwald> | Well, whatever you guya are arguing about, it's not about the reddit thread :p |
| 17:58:19 | texasmynsted | attempts to read the reddit |
| 17:58:36 | <merijn> | texasmynsted: You can't, it's all GameStop :p |
| 17:58:59 | <merijn> | koz_: Reminds me |
| 17:59:04 | <merijn> | @quote everything.is.hard |
| 17:59:04 | <lambdabot> | #haskell says: Writing good code is hard in any language. Writing bad code is hard in Haskell, therefore, everything is hard in Haskell |
| 17:59:15 | × | rdivyanshu quits (uid322626@gateway/web/irccloud.com/x-lnncqkpdqnzwrber) (Quit: Connection closed for inactivity) |
| 17:59:33 | × | dyeplexer quits (~lol@unaffiliated/terpin) (Remote host closed the connection) |
| 18:00:17 | <texasmynsted> | One of the biggest advantages a language can give the programmer is making it difficult to write bad code. |
| 18:00:21 | <merijn> | It's funny, 'cause it's true |
| 18:00:31 | <monochrom> | And nobody cares about reading the original article/thread. Has been true since slashdot. |
| 18:00:41 | <texasmynsted> | I read the heading in reddit |
| 18:00:46 | <monochrom> | Yes. |
| 18:01:01 | <texasmynsted> | I stick with Haskell or Racket |
| 18:01:01 | → | howdoi joins (uid224@gateway/web/irccloud.com/x-kendsybseqbsecek) |
| 18:01:03 | → | rayyyy joins (~nanoz@gateway/tor-sasl/nanoz) |
| 18:01:06 | <monochrom> | People simply read the heading and, the fun part being, start debating. |
| 18:01:09 | <merijn> | monochrom: Did you ever read Ender's Game? |
| 18:01:22 | <monochrom> | No. I watched the movie though. |
| 18:01:30 | <maerwald> | I'm wondering if I agree that haskell makes writing bad code hard. You have to go out of yourway maybe, but once you've learned a few bad patterns, you can basically use them everywhere |
| 18:01:34 | <monochrom> | I suppose it doesn't count. |
| 18:01:34 | <texasmynsted> | I read the book and saw the movie |
| 18:01:40 | <merijn> | monochrom: ah...I dunno the movie, so I'm not sure my comment was gonna make sense :p |
| 18:02:04 | <koz_> | maerwald: The fact that you have to go out of your way already makes it better than a lot of other languages I could name. |
| 18:02:13 | <merijn> | Ender's brother/sister influencing the world is, in hindsight, the most hilariously dumb plot point in history of fiction |
| 18:02:40 | <monochrom> | Hrm, I think I didn't see that in the movie. |
| 18:02:54 | <merijn> | monochrom: Since the plot is effectively "a pair of teens write a series of blogposts, so logical and persuasive the entire world voluntarily decides to follow them" |
| 18:02:55 | <texasmynsted> | The more a language makes it possible to make defective code something that can not be represented, the better. |
| 18:03:06 | × | rajivr quits (uid269651@gateway/web/irccloud.com/x-uzqklzijcugoxeov) (Quit: Connection closed for inactivity) |
| 18:03:08 | <monochrom> | haha |
| 18:03:09 | <maerwald> | in retrospect, it isn't that hard... oleg wrote a paper about it: https://arxiv.org/abs/cs/0509027 |
| 18:03:25 | <kuribas> | maerwald: it makes it hard, not impossible |
| 18:03:26 | <texasmynsted> | The worst programming problem is code that compiles and runs and has defects |
| 18:03:45 | × | lagothrix quits (~lagothrix@unaffiliated/lagothrix) (Ping timeout: 240 seconds) |
| 18:03:45 | <merijn> | maerwald: "Oleg wrote a paper about it" doesn't say anything about how hard something is :p |
| 18:04:04 | <merijn> | maerwald: Or maybe it does, but mostly due to "oleg" have a negative correlation with easy problems :p |
| 18:04:10 | <maerwald> | hehe |
| 18:04:14 | <texasmynsted> | Example: Tests do not prove that code is free of defects, it only exposes some conditions that are likely defects. |
| 18:04:26 | × | syd quits (~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) (Quit: Lost terminal) |
| 18:04:32 | <monochrom> | So anyway, what are we arguing over again? |
| 18:04:43 | → | finn_elija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) |
| 18:04:46 | <koz_> | Honestly, "Oleg wrote a paper about it" means that it's hard for everyoen who isn't Oleg. |
| 18:04:46 | <maerwald> | heading of a reddit thread |
| 18:04:48 | <texasmynsted> | heh |
| 18:05:02 | <koz_> | (especially now that he's in OCaml land) |
| 18:05:07 | <maerwald> | and Oleg memes |
| 18:06:19 | <texasmynsted> | I really need to develop zettelkasten or just set of note for every time questions like these come up |
| 18:06:58 | <maerwald> | "how to win every argument on the internet" |
| 18:07:20 | <texasmynsted> | There is no winning |
| 18:08:10 | <koz_> | Who cares about winning? |
| 18:08:11 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Read error: Connection reset by peer) |
| 18:08:13 | <texasmynsted> | I am likely taking the wrong approach. I need to find a way to profit from the foolishness and help those who want to make the world a better place. |
| 18:08:18 | <koz_> | Winning internet arguments is a pointless goal. |
| 18:08:38 | × | ubert quits (~Thunderbi@p200300ecdf25d950e6b318fffe838f33.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 18:08:47 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 18:08:51 | <texasmynsted> | I have the second part. The profit from the foolishness part requires more thought |
| 18:08:58 | → | ubert joins (~Thunderbi@p200300ecdf25d950e6b318fffe838f33.dip0.t-ipconnect.de) |
| 18:09:05 | <maerwald> | an idealist? |
| 18:09:32 | × | flatmap quits (~flatmap@p200300dd373b2a0018f40ccf4f078e3d.dip0.t-ipconnect.de) (Quit: Textual IRC Client: www.textualapp.com) |
| 18:09:37 | → | lagothrix joins (~lagothrix@unaffiliated/lagothrix) |
| 18:10:11 | → | denisse_ joins (~spaceCat@gateway/tor-sasl/alephzer0) |
| 18:10:20 | → | nojster joins (~noj@vmd62096.contaboserver.net) |
| 18:10:22 | <maerwald> | usually all that gets washed away in industry, where everything sucks, no matter the language |
| 18:10:35 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 18:10:39 | <maerwald> | i'm an optimist, obviously |
| 18:10:47 | <texasmynsted> | Maybe, or maybe I have encountered enough pain from the bs that I want to rid the world of it to save other from that suffering? |
| 18:10:47 | × | denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Ping timeout: 268 seconds) |
| 18:10:49 | <koz_> | maerwald: Gee, I'd never have guessed. |
| 18:10:53 | <maerwald> | xD |
| 18:11:19 | × | juuandyy quits (~juuandyy@90.106.228.121) (Ping timeout: 272 seconds) |
| 18:11:21 | × | jeremym quits (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) (Ping timeout: 256 seconds) |
| 18:12:14 | <srid> | Is `heist` the recommended library for doing HTML templates in Haskell, in 2021? http://snapframework.com/docs/tutorials/heist |
| 18:12:35 | <rotaerk> | huh, didn't realize haskell could be used for bank robbery |
| 18:12:51 | <koz_> | rotaerk: Bank -> IO Money :P |
| 18:13:01 | <rotaerk> | hehe |
| 18:13:16 | <maerwald> | IO Bank -> IO Money |
| 18:13:45 | <texasmynsted> | recommended? I think you might find what best fits your needs. |
| 18:13:56 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 18:14:06 | <koz_> | maerwald: Why is the bank in IO? |
| 18:14:08 | × | soft-warm quits (4408f588@ip68-8-245-136.sd.sd.cox.net) (Quit: Ping timeout (120 seconds)) |
| 18:14:16 | <koz_> | Surely the correct thing here is to have a Kleisli arrow? |
| 18:14:23 | <texasmynsted> | Because you can never get the money out of the IO? |
| 18:14:36 | <koz_> | Well, money _is_ external to your program... |
| 18:14:57 | × | geekosaur quits (82650c7c@130.101.12.124) (Quit: Ping timeout (120 seconds)) |
| 18:16:20 | <maerwald> | srid: https://hackage.haskell.org/package/blaze-html is also an option |
| 18:16:32 | <monochrom> | All of you are wrong. Both Bank and Money are linear: you should be using LinearTypes. |
| 18:17:22 | <maerwald> | money is eventually consistent in the bank though |
| 18:17:35 | → | geekosaur joins (82650c7c@130.101.12.124) |
| 18:17:58 | <koz_> | monochrom: Money being linear I can understand; when did you last consume a _bank_? |
| 18:18:09 | <koz_> | Are you secretly Godzilla? |
| 18:18:27 | <srid> | maerwald: Blaze does variable substitution, "includes", templates, etc.? |
| 18:18:39 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 18:19:00 | <monochrom> | Well, you can't clone a bank... |
| 18:19:01 | <srid> | ... allowing users to write raw HTML, that is. (Not baked into Haskell code, like reflex-dom, lucid, etc.) |
| 18:19:05 | × | bitmapper quits (uid464869@gateway/web/irccloud.com/x-pkbnmictikqwzgfz) (Quit: Connection closed for inactivity) |
| 18:19:20 | <maerwald> | srid: check the tutorial |
| 18:19:21 | <koz_> | monochrom: ST s Bank. |
| 18:19:38 | <koz_> | (or rather, STRef s Bank) |
| 18:19:52 | <srid> | maerwald: This one? https://jaspervdj.be/blaze/tutorial.html ... I see no raw HTML here. |
| 18:20:10 | → | juuandyy joins (~juuandyy@90.106.228.121) |
| 18:20:14 | <maerwald> | yeah, it's a html combinator library, allowing templating |
| 18:20:26 | × | conal quits (~conal@192.145.117.109) (Ping timeout: 264 seconds) |
| 18:20:59 | × | atwm quits (~andrew@19-193-28-81.ftth.cust.kwaoo.net) (Ping timeout: 256 seconds) |
| 18:21:08 | <srid> | Blaze forces the programmer to theme the app's HTML. What I want for the user to be able to do that. |
| 18:21:26 | × | danza quits (~francesco@151.53.68.90) (Quit: Leaving) |
| 18:21:28 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 18:22:04 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 18:22:10 | <texasmynsted> | I like the approach that pandoc takes, making and AST |
| 18:22:14 | <texasmynsted> | s/and/an/ |
| 18:22:29 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Remote host closed the connection) |
| 18:22:59 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 246 seconds) |
| 18:23:47 | <texasmynsted> | I always thought that Hamlet might be fun. https://www.yesodweb.com/book/shakespearean-templates |
| 18:23:56 | <texasmynsted> | I have never tried it though |
| 18:23:56 | × | forgottenone quits (~forgotten@176.42.21.112) (Remote host closed the connection) |
| 18:28:28 | <ph88^> | how can i benchmark a serializing library ? |
| 18:29:52 | → | condemnedferret joins (~condemned@2400:ac40:700:9e27:2c9e:215f:59bf:6442) |
| 18:30:41 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 18:30:43 | <ammar2> | ph88^: I'd probably use criterion |
| 18:30:56 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 18:32:19 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 18:32:20 | <ph88^> | what can i use as input data though ? |
| 18:32:57 | <geekosaur> | in't that what Arbitrary instances are for? |
| 18:33:18 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 18:33:37 | <ammar2> | presumably you have some data you're interested in serializing? |
| 18:33:42 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Client Quit) |
| 18:33:57 | <ammar2> | or some common cases that the serialization library should be able to handle |
| 18:34:27 | <ph88^> | no i don't have it :/ |
| 18:34:32 | → | conal joins (~conal@192.145.117.109) |
| 18:34:34 | <ph88^> | no use case at this moment |
| 18:35:13 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 18:35:29 | × | condemnedferret quits (~condemned@2400:ac40:700:9e27:2c9e:215f:59bf:6442) (Quit: Quit) |
| 18:35:48 | <koz_> | With Hedgehog, is there a way to write a generator that chooses a sublist of a list? |
| 18:35:50 | <koz_> | So something like |
| 18:35:57 | <koz_> | sublist :: [a] -> Gen [a] |
| 18:36:30 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Read error: Connection reset by peer) |
| 18:36:54 | × | wonko7 quits (~wonko7@78.199.183.4) (Ping timeout: 256 seconds) |
| 18:37:13 | <koz_> | Oh, Gen.subsequence, OK. |
| 18:37:18 | <ph88^> | ok :P |
| 18:38:52 | → | wonko7 joins (~wonko7@2a01:e34:ec7b:7040:40c9:55ff:fe52:3a73) |
| 18:41:06 | × | o1lo01ol1o quits (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) (Remote host closed the connection) |
| 18:41:22 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 18:41:28 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) |
| 18:43:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 18:43:48 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 18:45:31 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 18:45:43 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 18:48:21 | × | shiraeeshi quits (~shiraeesh@77.94.25.134) (Quit: Konversation terminated!) |
| 18:48:44 | → | shiraeeshi joins (~shiraeesh@77.94.25.134) |
| 18:49:23 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 18:49:36 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 18:49:48 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 18:49:50 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 18:51:45 | × | geekosaur quits (82650c7c@130.101.12.124) (Ping timeout: 248 seconds) |
| 18:52:00 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Read error: Connection reset by peer) |
| 18:52:08 | → | condemnedferret joins (~condemned@64.120.2.177) |
| 18:52:37 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 18:52:42 | × | unlink2 quits (~unlink2@p200300ebcf12ea00013250d6b4625a26.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 18:53:12 | → | smitop joins (uid328768@gateway/web/irccloud.com/x-tlgczbpxaoiulfpk) |
| 18:53:54 | → | unlink2 joins (~unlink2@p57b8511e.dip0.t-ipconnect.de) |
| 18:54:04 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 18:58:25 | × | juuandyy quits (~juuandyy@90.106.228.121) (Read error: Connection reset by peer) |
| 18:58:36 | → | juuandyy joins (~juuandyy@90.106.228.121) |
| 18:58:41 | × | ubert quits (~Thunderbi@p200300ecdf25d950e6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 18:59:58 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 19:00:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 19:01:21 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:03:24 | × | vgtw quits (~vgtw@gateway/tor-sasl/vgtw) (Remote host closed the connection) |
| 19:03:30 | → | berberman_ joins (~berberman@unaffiliated/berberman) |
| 19:03:44 | → | vgtw joins (~vgtw@gateway/tor-sasl/vgtw) |
| 19:04:09 | × | ft quits (~ft@shell.chaostreff-dortmund.de) (Ping timeout: 260 seconds) |
| 19:04:14 | × | berberman quits (~berberman@unaffiliated/berberman) (Ping timeout: 264 seconds) |
| 19:06:25 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 19:06:38 | → | writenix joins (~quassel@a94-133-31-209.cpe.netcabo.pt) |
| 19:06:55 | → | shf joins (~sheaf@2a01:cb19:80cc:7e00:2939:2eff:3d7d:ae11) |
| 19:07:00 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:07:33 | × | writenix quits (~quassel@a94-133-31-209.cpe.netcabo.pt) (Remote host closed the connection) |
| 19:08:24 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 19:08:26 | → | geekosaur joins (82650c7c@130.101.12.124) |
| 19:08:38 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 19:08:51 | × | tromp_ quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 19:08:59 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 19:09:19 | <Sh4rPEYE> | I missed out on the discussion, but hopefully some of you are still here |
| 19:09:58 | <Sh4rPEYE> | The course isn't really focused on webdev, I chose it mostly because web things are well supported, portable and mostly easy to setup on whicherver playtform you are using |
| 19:10:44 | × | borne quits (~fritjof@200116b8641b4900438d15c340c1e8fe.dip.versatel-1u1.de) (Ping timeout: 240 seconds) |
| 19:10:53 | <Sh4rPEYE> | What IS it focused on, then? The students already know FP (from a scheme-like language I taught in the first semester), I want to introduce them to types, patter matching, and all that good Haskell stuff |
| 19:11:27 | <Sh4rPEYE> | (texasmynsted and maerwald) |
| 19:11:56 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 19:12:41 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 19:12:57 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 19:13:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:13:41 | <Sh4rPEYE> | I specifically chose a typed FP language, because I think they wouldn't have seen this type of programming otherwise. I hope to broaden their horizons, so to say. And I chose project-based (game-centric) approach, because that's what the students like. And I still want them to get better at programming, you know |
| 19:14:21 | <Sh4rPEYE> | Purescript/Elm are just means to this end — show them something new and interesting through a project-based curriculum. That's it. |
| 19:16:05 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Quit: Lost terminal) |
| 19:16:49 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 260 seconds) |
| 19:18:05 | → | poscat1 joins (~poscat@114.245.115.216) |
| 19:19:14 | × | poscat quits (~poscat@114.245.115.216) (Ping timeout: 264 seconds) |
| 19:21:15 | → | soft-warm joins (4408f588@ip68-8-245-136.sd.sd.cox.net) |
| 19:22:42 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 19:23:01 | × | jchia__ quits (~jchia@58.32.38.49) (Ping timeout: 265 seconds) |
| 19:24:03 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 272 seconds) |
| 19:24:19 | → | usr25 joins (~usr25@unaffiliated/usr25) |
| 19:24:38 | × | carlomagno quits (~cararell@148.87.23.12) (Ping timeout: 264 seconds) |
| 19:24:50 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:28:06 | → | carlomagno joins (~cararell@148.87.23.12) |
| 19:29:48 | × | juuandyy quits (~juuandyy@90.106.228.121) (Quit: Konversation terminated!) |
| 19:29:53 | × | usr25 quits (~usr25@unaffiliated/usr25) (Read error: Connection reset by peer) |
| 19:30:04 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 19:30:08 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 19:31:05 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:31:30 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Client Quit) |
| 19:31:59 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 19:32:26 | → | jneira joins (501ca940@gateway/web/cgi-irc/kiwiirc.com/ip.80.28.169.64) |
| 19:32:48 | <texasmynsted> | Then it sounds like either are a fine choice. |
| 19:36:07 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 19:36:45 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:37:58 | <AWizzArd> | In the example at https://ihp.digitallyinduced.com/Guide/your-first-project.html#displaying-a-post I see the call `(get #title post)`. What is #title? The hash sign looks strange. |
| 19:39:51 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 19:40:47 | → | ft joins (~ft@shell.chaostreff-dortmund.de) |
| 19:41:44 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 19:42:27 | × | condemnedferret quits (~condemned@64.120.2.177) (Quit: Quit) |
| 19:42:43 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:43:44 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Remote host closed the connection) |
| 19:44:12 | × | carlomagno quits (~cararell@148.87.23.12) (Remote host closed the connection) |
| 19:44:26 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 264 seconds) |
| 19:47:15 | → | shadowdaemon joins (~user@unaffiliated/shadowdaemon) |
| 19:47:49 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 19:48:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 19:48:40 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:48:56 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 19:49:25 | × | ixaxaar quits (~ixaxaar@49.207.210.215) (Ping timeout: 240 seconds) |
| 19:49:29 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 19:50:16 | → | coot joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 19:51:38 | × | ukari quits (~ukari@unaffiliated/ukari) (Remote host closed the connection) |
| 19:52:31 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Remote host closed the connection) |
| 19:54:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 19:54:04 | <geekosaur> | AWizzArd, field selection |
| 19:54:49 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 19:57:35 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 19:57:48 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 19:58:50 | × | Mr_Cue quits (~Mr._Cue@pengyuzhou.com) (Remote host closed the connection) |
| 19:59:15 | → | Mr_Cue joins (~Mr._Cue@pengyuzhou.com) |
| 20:01:01 | → | jeremym joins (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) |
| 20:01:22 | × | jonathanx quits (~jonathan@h-176-109.A357.priv.bahnhof.se) (Quit: Leaving) |
| 20:02:11 | → | joe6842 joins (4cbf1b10@s-27-16.flex.volo.net) |
| 20:02:21 | × | DavidEichmann quits (~david@234.109.45.217.dyn.plus.net) (Remote host closed the connection) |
| 20:02:25 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 256 seconds) |
| 20:02:38 | → | dnlkrgr joins (~dnlkrgr@HSI-KBW-046-005-005-235.hsi8.kabel-badenwuerttemberg.de) |
| 20:03:32 | × | wonko7 quits (~wonko7@2a01:e34:ec7b:7040:40c9:55ff:fe52:3a73) (Quit: See You Space Cowboy..) |
| 20:05:06 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 20:05:07 | × | o1lo01ol1o quits (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) (Remote host closed the connection) |
| 20:05:26 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 20:05:26 | × | petersen quits (~petersen@redhat/juhp) (Ping timeout: 264 seconds) |
| 20:06:18 | → | kupi joins (uid212005@gateway/web/irccloud.com/x-lcljveiqhawksjqz) |
| 20:06:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:07:26 | → | petersen joins (~petersen@redhat/juhp) |
| 20:07:49 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection) |
| 20:08:06 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 20:08:26 | × | conal quits (~conal@192.145.117.109) (Ping timeout: 264 seconds) |
| 20:08:26 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 20:08:27 | × | fendor quits (~fendor@178.165.131.88.wireless.dyn.drei.com) (Remote host closed the connection) |
| 20:08:43 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 20:08:53 | × | joe6842 quits (4cbf1b10@s-27-16.flex.volo.net) (Quit: Connection closed) |
| 20:09:53 | × | toppler quits (~user@mtop.default.momentoftop.uk0.bigv.io) (Remote host closed the connection) |
| 20:10:25 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 20:10:41 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 20:11:59 | → | forgottenone joins (~forgotten@176.42.21.112) |
| 20:12:24 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 20:14:08 | × | rayyyy quits (~nanoz@gateway/tor-sasl/nanoz) (Ping timeout: 268 seconds) |
| 20:14:36 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 20:14:41 | → | vgtw_ joins (~vgtw@gateway/tor-sasl/vgtw) |
| 20:15:21 | × | vgtw quits (~vgtw@gateway/tor-sasl/vgtw) (Ping timeout: 268 seconds) |
| 20:15:22 | vgtw_ | is now known as vgtw |
| 20:15:31 | → | conal joins (~conal@192.145.117.109) |
| 20:15:49 | <koz_> | That website proves everything I've been saying about the web. |
| 20:15:52 | <koz_> | Link is broken. |
| 20:15:58 | <koz_> | Text looks awful and unreadable on my monitor. |
| 20:16:02 | <koz_> | Loads like trash. |
| 20:16:08 | → | machined1od joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 20:16:18 | <koz_> | It's a glorified blog, it's not that hard. |
| 20:16:24 | × | machined1od quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Client Quit) |
| 20:16:35 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 20:17:53 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood) |
| 20:17:54 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:18:25 | × | jeremym quits (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) (Quit: Leaving) |
| 20:18:38 | × | jfe` quits (~user@pool-71-184-149-134.bstnma.fios.verizon.net) (Ping timeout: 264 seconds) |
| 20:19:07 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 20:19:18 | → | j3r3my joins (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) |
| 20:19:31 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 20:20:32 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 20:21:04 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Remote host closed the connection) |
| 20:21:25 | × | tsrt^ quits (tsrt@ip98-184-89-2.mc.at.cox.net) () |
| 20:23:26 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 20:23:39 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:24:22 | → | jfe` joins (~user@pool-71-184-149-134.bstnma.fios.verizon.net) |
| 20:24:29 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 260 seconds) |
| 20:24:33 | × | soft-warm quits (4408f588@ip68-8-245-136.sd.sd.cox.net) (Ping timeout: 248 seconds) |
| 20:25:01 | → | Deide joins (~Deide@217.155.19.23) |
| 20:25:21 | → | Lycurgus joins (~niemand@cpe-45-46-139-165.buffalo.res.rr.com) |
| 20:26:23 | × | Jesin quits (~Jesin@pool-72-66-101-18.washdc.fios.verizon.net) (Quit: Leaving) |
| 20:27:06 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 20:28:45 | × | kuribas quits (~user@ptr-25vy0i8e75wmxgu7azj.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 20:29:00 | × | jfe` quits (~user@pool-71-184-149-134.bstnma.fios.verizon.net) (Ping timeout: 256 seconds) |
| 20:29:06 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 20:29:16 | → | justsomeguy joins (~justsomeg@unaffiliated/--/x-3805311) |
| 20:29:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:30:37 | → | jfe` joins (~user@pool-71-184-149-134.bstnma.fios.verizon.net) |
| 20:31:49 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 272 seconds) |
| 20:31:59 | → | jchia__ joins (~jchia@jungle.jchia.net) |
| 20:33:23 | → | borne joins (~fritjof@200116b8641b4900438d15c340c1e8fe.dip.versatel-1u1.de) |
| 20:34:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 20:35:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:35:37 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 20:36:14 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 20:38:04 | × | jchia__ quits (~jchia@jungle.jchia.net) (Ping timeout: 256 seconds) |
| 20:39:28 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Remote host closed the connection) |
| 20:40:40 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 20:40:49 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 20:41:11 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:41:53 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Client Quit) |
| 20:42:25 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 20:42:28 | → | carlomagno joins (~cararell@148.87.23.12) |
| 20:42:37 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 246 seconds) |
| 20:44:24 | → | coot joins (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) |
| 20:44:29 | × | Sh4rPEYE quits (~textual@2a02:8308:388:aa00:c445:300:dc4e:194f) (Ping timeout: 272 seconds) |
| 20:44:55 | → | DarukFromHyrule joins (542e199d@gateway/web/cgi-irc/kiwiirc.com/ip.84.46.25.157) |
| 20:46:18 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 20:46:34 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 20:46:58 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:47:42 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 20:48:42 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 20:50:27 | → | tatooine-sunset joins (~botond@217-197-190-248.pool.digikabel.hu) |
| 20:50:45 | → | igghibu joins (~igghibu@91.193.4.172) |
| 20:50:56 | × | xff0x quits (~xff0x@2001:1a81:520f:a600:96af:82c9:7615:9820) (Ping timeout: 240 seconds) |
| 20:51:01 | <sm[m]> | way to trash someone's work :) |
| 20:51:31 | <koz_> | sm[m]: If I made somethign like this, I'd rather someoen call me out publically. |
| 20:51:47 | <koz_> | _Especially_ if I was paid for it. |
| 20:51:54 | → | xff0x joins (~xff0x@2001:1a81:520f:a600:db8b:92ac:b959:cbfe) |
| 20:52:08 | <koz_> | But that's offtopic anyway. |
| 20:52:29 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 20:52:43 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:52:43 | × | son0p quits (~son0p@181.136.122.143) (Ping timeout: 272 seconds) |
| 20:54:01 | × | Narinas quits (~Narinas@189.223.62.254.dsl.dyn.telnor.net) (Read error: Connection reset by peer) |
| 20:54:22 | → | son0p joins (~son0p@181.136.122.143) |
| 20:54:36 | × | coot quits (~coot@37.30.55.132.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 20:54:51 | <idnar> | AWizzArd: -XOverloadedLabels probably |
| 20:55:18 | <Uniaika> | AWizzArd: yep', Overloaded Labels |
| 20:55:25 | × | cocytus_ quits (~cocytus@cpe-76-95-48-109.socal.res.rr.com) (Ping timeout: 240 seconds) |
| 20:55:27 | → | Narinas joins (~Narinas@189.223.62.254.dsl.dyn.telnor.net) |
| 20:56:13 | geekosaur | got lost looking through all the record-related syntax goop |
| 20:56:27 | <geekosaur> | there's how many ways to do that now? |
| 20:56:29 | Lycurgus | turned up his nose at it when he saw it was nix centric |
| 20:56:37 | <koz_> | geekosaur: A multitude, but less than a horde. |
| 20:56:39 | Lycurgus | *up |
| 20:57:07 | Lycurgus | s/*up// |
| 20:57:44 | × | igghibu quits (~igghibu@91.193.4.172) (Ping timeout: 260 seconds) |
| 20:57:54 | × | tatooine-sunset quits (~botond@217-197-190-248.pool.digikabel.hu) (Ping timeout: 256 seconds) |
| 20:58:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 20:58:25 | × | jiribenes quits (~jiribenes@rosa.jiribenes.com) (Ping timeout: 272 seconds) |
| 20:58:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:58:55 | <koz_> | Lycurgus: Sup? :P |
| 20:59:21 | <Lycurgus> | :) |
| 20:59:37 | DarukFromHyrule | hugs ski |
| 20:59:37 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) |
| 21:01:38 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 21:02:44 | × | smitop quits (uid328768@gateway/web/irccloud.com/x-tlgczbpxaoiulfpk) (Quit: Connection closed for inactivity) |
| 21:03:27 | → | cocytus joins (~cocytus@cpe-76-95-48-109.socal.res.rr.com) |
| 21:04:07 | × | o1lo01ol1o quits (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) (Remote host closed the connection) |
| 21:04:24 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-140-216.dsl.telepac.pt) |
| 21:05:19 | → | jchia__ joins (~jchia@58.32.38.49) |
| 21:06:04 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 246 seconds) |
| 21:06:32 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 21:06:45 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 21:06:48 | <topos> | hugging? in my haskell? it is not of god. Christian elbow bumps only pls |
| 21:07:13 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 264 seconds) |
| 21:08:40 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 21:08:57 | <AWizzArd> | idnar and Uniaika: thx, OverloadedLabels |
| 21:09:50 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 21:09:57 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:10:19 | <koz_> | topos: Do you have a moment to hear about our lord and saviour Nyarlathotep? |
| 21:10:25 | × | Kaiepi quits (~Kaiepi@47.54.252.148) (Remote host closed the connection) |
| 21:10:42 | <topos> | ah yes, the crawling chaos |
| 21:10:52 | <Uniaika> | 👋 topos |
| 21:10:57 | <topos> | hihi |
| 21:11:11 | → | Kaiepi joins (~Kaiepi@47.54.252.148) |
| 21:11:42 | × | j3r3my quits (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) (Remote host closed the connection) |
| 21:12:19 | → | j3r3my joins (~jeremym@68-73-116-155.lightspeed.rlghnc.sbcglobal.net) |
| 21:12:32 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 21:12:58 | × | kritzefitz quits (~kritzefit@212.86.56.80) (Remote host closed the connection) |
| 21:13:57 | → | ubert joins (~Thunderbi@p200300ecdf25d950e6b318fffe838f33.dip0.t-ipconnect.de) |
| 21:14:14 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 21:14:26 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 264 seconds) |
| 21:14:56 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 21:15:42 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:18:37 | × | nineonin_ quits (~nineonine@50.216.62.2) (Ping timeout: 264 seconds) |
| 21:21:27 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 21:21:49 | × | xff0x quits (~xff0x@2001:1a81:520f:a600:db8b:92ac:b959:cbfe) (Remote host closed the connection) |
| 21:22:07 | → | xff0x joins (~xff0x@2001:1a81:520f:a600:9140:9df9:51ef:c0ff) |
| 21:22:13 | × | deviantfero quits (~deviantfe@190.150.27.58) (Ping timeout: 264 seconds) |
| 21:22:21 | × | ph88^ quits (~ph88@2a02:8109:9e00:7e5c:6c28:450f:9830:3db8) (Quit: Leaving) |
| 21:23:01 | × | dhouthoo quits (~dhouthoo@ptr-eitgbj2w0uu6delkbrh.18120a2.ip6.access.telenet.be) (Quit: WeeChat 3.0) |
| 21:25:44 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 21:26:17 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) (Ping timeout: 260 seconds) |
| 21:26:53 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:26:58 | × | natim87 quits (sid286962@gateway/web/irccloud.com/x-kdprozyavblxdjvv) (Ping timeout: 244 seconds) |
| 21:27:27 | × | totbwf quits (sid402332@gateway/web/irccloud.com/x-extwtohnnhcghckc) (Ping timeout: 260 seconds) |
| 21:27:31 | × | SrPx quits (sid108780@gateway/web/irccloud.com/x-ftlqxaankfwodccw) (Ping timeout: 265 seconds) |
| 21:27:38 | × | ryjm quits (sid383513@gateway/web/irccloud.com/x-rtromtwwgkanhrlc) (Ping timeout: 264 seconds) |
| 21:28:01 | → | natim87 joins (sid286962@gateway/web/irccloud.com/x-zlsantvwbppaghas) |
| 21:28:37 | × | joshmeredith quits (sid387798@gateway/web/irccloud.com/x-ystdraxbfucupaph) (Ping timeout: 260 seconds) |
| 21:28:38 | × | banjiewen__ quits (sid115913@gateway/web/irccloud.com/x-tffjgjycoobvvwpf) (Ping timeout: 260 seconds) |
| 21:29:02 | → | joshmeredith joins (sid387798@gateway/web/irccloud.com/x-ygnxigyifustxkeb) |
| 21:29:10 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:54b6:e8d3:c70d:8881) |
| 21:29:12 | × | AndreasK quits (uid320732@gateway/web/irccloud.com/x-rryhvqtibixmjgby) (Ping timeout: 268 seconds) |
| 21:29:56 | → | SrPx joins (sid108780@gateway/web/irccloud.com/x-rmsqcmcogdpaxgkg) |
| 21:30:02 | → | totbwf joins (sid402332@gateway/web/irccloud.com/x-mndywvdfsgsxqtwx) |
| 21:30:09 | → | ryjm joins (sid383513@gateway/web/irccloud.com/x-tszvxtkoavldjrjz) |
| 21:30:12 | → | AndreasK joins (uid320732@gateway/web/irccloud.com/x-uxhknygpiwtxbjmk) |
| 21:30:15 | → | banjiewen__ joins (sid115913@gateway/web/irccloud.com/x-ierynqowzkoepfnn) |
| 21:32:08 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 21:32:15 | → | jfe`` joins (~user@pool-71-184-149-134.bstnma.fios.verizon.net) |
| 21:32:26 | → | cocytus_ joins (~cocytus@cpe-76-95-48-109.socal.res.rr.com) |
| 21:32:40 | → | comerijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 21:32:43 | → | usr25 joins (~usr25@unaffiliated/usr25) |
| 21:33:54 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 21:35:33 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 21:35:52 | × | cocytus quits (~cocytus@cpe-76-95-48-109.socal.res.rr.com) (Ping timeout: 256 seconds) |
| 21:35:52 | × | jfe` quits (~user@pool-71-184-149-134.bstnma.fios.verizon.net) (Ping timeout: 256 seconds) |
| 21:36:39 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 21:38:00 | × | Lycurgus quits (~niemand@cpe-45-46-139-165.buffalo.res.rr.com) (Quit: Exeunt) |
| 21:38:00 | → | nineonine joins (~nineonine@50.216.62.2) |
| 21:38:08 | × | comerijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 21:39:35 | → | jiribenes joins (~jiribenes@rosa.jiribenes.com) |
| 21:40:05 | × | Varis quits (~Tadas@unaffiliated/varis) (Remote host closed the connection) |
| 21:41:04 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 246 seconds) |
| 21:43:25 | × | d3od quits (~nickmeno3@78-0-98-144.adsl.net.t-com.hr) (Ping timeout: 240 seconds) |
| 21:43:52 | × | conal quits (~conal@192.145.117.109) (Quit: Computer has gone to sleep.) |
| 21:44:03 | ← | jfe`` parts (~user@pool-71-184-149-134.bstnma.fios.verizon.net) ("ERC (IRC client for Emacs 27.1)") |
| 21:47:32 | × | darjeeling_ quits (~darjeelin@122.245.219.80) (Ping timeout: 265 seconds) |
| 21:51:57 | → | conal joins (~conal@198.8.81.77) |
| 21:52:17 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 21:52:48 | × | geekosaur quits (82650c7c@130.101.12.124) (Quit: Connection closed) |
| 21:55:46 | → | mentaal[m] joins (mentaalmat@gateway/shell/matrix.org/x-ocjxyfmxlffojmgc) |
| 21:57:01 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 264 seconds) |
| 21:59:33 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Remote host closed the connection) |
| 21:59:47 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 22:00:07 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 22:00:18 | → | deviantfero joins (~deviantfe@190.150.27.58) |
| 22:00:31 | <monochrom> | Hugs has simpler error messages. (Speaking of hugging.) |
| 22:02:30 | → | darjeeling_ joins (~darjeelin@122.245.219.80) |
| 22:02:57 | × | jmchael quits (~jmchael@87.112.235.234) (Quit: Leaving) |
| 22:03:02 | <koz_> | And a really nice record system. |
| 22:03:07 | → | ph88 joins (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de) |
| 22:03:31 | × | johnw quits (~johnw@haskell/developer/johnw) (Quit: ZNC - http://znc.in) |
| 22:03:42 | <ph88> | Why is there a dollar sign in front of allProperties ? https://hackage.haskell.org/package/QuickCheck-2.14.2/docs/Test-QuickCheck.html#v:allProperties |
| 22:04:02 | <koz_> | ph88: It's a TH splice. |
| 22:04:07 | <ph88> | oh ok |
| 22:04:46 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 256 seconds) |
| 22:06:26 | ← | DarukFromHyrule parts (542e199d@gateway/web/cgi-irc/kiwiirc.com/ip.84.46.25.157) () |
| 22:06:53 | <ph88> | where can i set this option ? https://hackage.haskell.org/package/tasty-quickcheck-0.10.1.2/docs/Test-Tasty-QuickCheck.html#t:QuickCheckShowReplay i don't see any function that takes IsOption |
| 22:06:58 | × | dnlkrgr quits (~dnlkrgr@HSI-KBW-046-005-005-235.hsi8.kabel-badenwuerttemberg.de) (Ping timeout: 246 seconds) |
| 22:07:02 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 22:07:19 | <koz_> | ph88: localOption is what you seek. |
| 22:07:57 | <ph88> | thx |
| 22:08:40 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:08:57 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 22:10:01 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 22:11:16 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 22:11:37 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 22:12:19 | × | livvy quits (~livvy@gateway/tor-sasl/livvy) (Remote host closed the connection) |
| 22:12:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 22:13:38 | → | livvy joins (~livvy@gateway/tor-sasl/livvy) |
| 22:13:50 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 264 seconds) |
| 22:14:19 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 246 seconds) |
| 22:15:51 | × | livvy quits (~livvy@gateway/tor-sasl/livvy) (Remote host closed the connection) |
| 22:16:40 | <ph88> | where can i see the default value for an option like https://hackage.haskell.org/package/tasty-quickcheck-0.10.1.2/docs/Test-Tasty-QuickCheck.html#t:QuickCheckTests ? |
| 22:16:50 | × | borne quits (~fritjof@200116b8641b4900438d15c340c1e8fe.dip.versatel-1u1.de) (Ping timeout: 264 seconds) |
| 22:17:04 | <koz_> | ph88: https://hackage.haskell.org/package/tasty-quickcheck-0.10.1.2/docs/src/Test.Tasty.QuickCheck.html#line-102 |
| 22:17:08 | <koz_> | 100 in this case. |
| 22:17:20 | <koz_> | Every instance of 'IsOption' must supply 'defaultValue'. |
| 22:17:27 | <ph88> | thanks |
| 22:17:33 | <koz_> | (also, that default is far, _far_ too low for anything useful) |
| 22:17:42 | <koz_> | (I recommend raising it to at least 1000, and the more the better) |
| 22:17:42 | → | livvy joins (~livvy@gateway/tor-sasl/livvy) |
| 22:17:56 | × | jchia__ quits (~jchia@58.32.38.49) (Ping timeout: 240 seconds) |
| 22:18:01 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 22:18:05 | <ph88> | is there a function to apply a list of options ? |
| 22:18:48 | <koz_> | ph88: No, unless every single one of them has the same type. |
| 22:18:52 | <koz_> | You can do something like |
| 22:19:12 | <koz_> | localOptions :: [forall v . IsOption v => v] -> TestTree -> TestTree |
| 22:19:17 | <koz_> | But then you're on your own. :P |
| 22:20:06 | → | Heffalump joins (~ganesh@urchin.earth.li) |
| 22:20:21 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Quit: Leaving) |
| 22:22:14 | → | jchia__ joins (~jchia@jungle.jchia.net) |
| 22:22:44 | → | cheater1 joins (~user@unaffiliated/cheater) |
| 22:22:57 | × | cheater quits (~user@unaffiliated/cheater) (Ping timeout: 256 seconds) |
| 22:22:57 | <Heffalump> | anyone have a rough idea when to expect GHC 9.0 final? |
| 22:22:58 | <ph88> | koz_, how did you get a feeling for the amount of testcases ? |
| 22:22:59 | cheater1 | is now known as cheater |
| 22:23:00 | × | wyer quits (~justin_wy@102-65-159-176.dsl.web.africa) (Ping timeout: 256 seconds) |
| 22:23:06 | <koz_> | ph88: _Did_? |
| 22:23:13 | <koz_> | Heffalump: Don't hold your breath. |
| 22:23:55 | × | justanotheruser quits (~justanoth@unaffiliated/justanotheruser) (Ping timeout: 272 seconds) |
| 22:25:08 | × | jchia__ quits (~jchia@jungle.jchia.net) (Remote host closed the connection) |
| 22:25:08 | <koz_> | There's a page listing what remains to do before 9.0, and it has a _lot_ of unchecked entries. |
| 22:25:50 | <ph88> | Heffalump, i would guess around april |
| 22:25:59 | <ph88> | https://gitlab.haskell.org/ghc/ghc/-/issues/18216 |
| 22:26:04 | × | sud0 quits (~Death@hackspaceuy/member/sud0) (Remote host closed the connection) |
| 22:26:11 | <Heffalump> | koz_: I've looked at that off and on, but on the other hand there was actually an RC1 which sort of implies all the genuine TODOs are done |
| 22:26:17 | <ph88> | koz_, yes did because you mentioned a specific number of 1000 .. and also "do" :P |
| 22:26:25 | <koz_> | ph88: I said _at least_. |
| 22:26:32 | <koz_> | That's actually quite a small number. |
| 22:26:39 | <koz_> | My general policy is roughly thus. |
| 22:26:41 | <ph88> | ye question still stands |
| 22:27:11 | <Heffalump> | ph88: ah, I should have looked at that ticket again before asking here, sounds like it's mainly libraries now |
| 22:27:19 | <koz_> | 1. Pick a number of zeroes between five and eight. 2. Run 1 followed by that many zeroes in tests. 3. Is this taking a tolerably short time? If yes, add a zero; if not, remove one. 4. Run again. |
| 22:27:32 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:9ca:aef9:e139:13f6) (Ping timeout: 260 seconds) |
| 22:28:00 | <ph88> | how much time do you find tolerable ? |
| 22:28:06 | <koz_> | Basically, the larger your test count, the more likely you are to find issues, but you have to consider that test times being too long makes it likely that nobody will run them. |
| 22:28:06 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 22:28:13 | <koz_> | Me personally? Probably <10 for entire suite. |
| 22:28:18 | <koz_> | <10s* |
| 22:28:27 | <koz_> | Any longer than that, and folks will look for excuses not to run it. |
| 22:28:36 | <ph88> | what about in CI ? |
| 22:28:47 | <koz_> | ph88: That's a different problem entirely and I cannot speak for it. |
| 22:28:51 | <koz_> | I'm not responsible for CI. |
| 22:29:06 | <ph88> | haha :P |
| 22:29:12 | <koz_> | Basically, the general idea is 'run as many tests as is tolerable'. |
| 22:29:16 | <ph88> | do you know how to give command line option for how many runs ? |
| 22:29:23 | <koz_> | ph88: Not to tasty. |
| 22:29:32 | → | jackk_ joins (~jackk@205.178.111.134) |
| 22:29:34 | <ph88> | you don't know or it's not possible ? |
| 22:29:40 | <koz_> | I don't know. |
| 22:29:42 | <ph88> | ok |
| 22:29:53 | <koz_> | Your question was phrased 'do you know X', hence my response is about my knowledge. |
| 22:30:02 | <koz_> | It's likely possible, I just never needed that. :P |
| 22:31:43 | → | jchia__ joins (~jchia@58.32.38.49) |
| 22:31:46 | <ph88> | feuerbach_ ? :) |
| 22:32:09 | → | borne joins (~fritjof@200116b8641b4900438d15c340c1e8fe.dip.versatel-1u1.de) |
| 22:32:16 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) (Ping timeout: 240 seconds) |
| 22:33:34 | × | hyperisco quits (~hyperisco@104-195-141-253.cpe.teksavvy.com) (Ping timeout: 246 seconds) |
| 22:34:08 | <ph88> | i think i found it :P |
| 22:34:10 | <ph88> | wasn't that hard |
| 22:36:26 | → | bogdanp joins (~bogdanp@188.24.80.165) |
| 22:39:34 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:1bf9:a0e5:954d:9e4e) |
| 22:39:43 | × | LKoen quits (~LKoen@19.175.9.109.rev.sfr.net) (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”) |
| 22:40:46 | <ph88> | tasty looks like a nice package |
| 22:41:11 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 22:41:39 | × | bogdanp quits (~bogdanp@188.24.80.165) (Ping timeout: 272 seconds) |
| 22:41:43 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 22:42:26 | × | mananamenos_ quits (~mananamen@84.122.202.215.dyn.user.ono.com) (Ping timeout: 265 seconds) |
| 22:43:52 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 22:44:25 | <koz_> | I agree. |
| 22:44:49 | × | son0p quits (~son0p@181.136.122.143) (Quit: Lost terminal) |
| 22:45:48 | <ski> | koz_,ph88 : `[forall v . IsOption v => v]' looks rather useless to me. perhaps you meant `[exists v. IsOption v *> v]' |
| 22:46:40 | <ph88> | jeez that's fancy |
| 22:46:46 | <ph88> | never even see *> before |
| 22:47:02 | <ph88> | also didn't know exists was a quantifier in haskell o_O |
| 22:48:23 | → | acidjnk_new joins (~acidjnk@p200300d0c704e733dd41bcd6e6128dbe.dip0.t-ipconnect.de) |
| 22:49:30 | <koz_> | It's not? |
| 22:49:41 | <koz_> | I don't believe it is at leasts. |
| 22:49:46 | <koz_> | s/leasts/least/ |
| 22:50:03 | <koz_> | I was going for 'I am a list of things, and the only thing we know about them is that they have an IsOption instance. |
| 22:50:05 | <koz_> | ' |
| 22:50:16 | <koz_> | I know this can be phrased somehow, but I don't remember how exactly. |
| 22:50:20 | × | neiluj quits (~jco@unaffiliated/neiluj) (Quit: leaving) |
| 22:50:25 | <Heffalump> | I think *> is a typo for => |
| 22:50:36 | <ski> | no |
| 22:50:44 | <Heffalump> | oh, ok |
| 22:50:48 | <ski> | both `exists' and `*>' are pseudo-Haskell |
| 22:51:36 | <ski> | (iirc, LHC does support `exists', but only to the left of a function arrow (the trivial case). perhaps it's also allowed in type synonyms, provided you only use them to the left of a function arrow) |
| 22:51:59 | <ski> | koz_ : yes, sounds like you meant my version |
| 22:52:12 | <koz_> | ski: Yep, so how do you phrase it in non-pseudo-Haskell? |
| 22:52:17 | → | niekvandepas joins (~niekvande@dhcp-077-249-088-250.chello.nl) |
| 22:52:20 | <koz_> | Do you need to do a GADT or something? |
| 22:52:26 | <Heffalump> | koz_: at worst you could write a GADT to wrap it, yes |
| 22:52:38 | <Heffalump> | that's almost certainly the best strategy too |
| 22:53:06 | <ski> | i find it useful to discuss existentials in terms of `exists' and `*>', because, imho, it's often clearer to talk about it, in these terms, rather than immediately jumping to one of the two encodings of them in Haskell ("existentially quantified data constructor" vs. CPS encoding) |
| 22:53:22 | <Heffalump> | forall v . IsOption v => v is "value" (actually really a function) that can construct a 'v' for any possible type that is an instance of IsOption |
| 22:53:44 | <koz_> | Yeah, definitely my bad then. |
| 22:53:51 | <ski> | and yes, you'd either need `ExistentialQuantification' (a misnomer, imho) or `GADTs' .. or else `Rank2Types' (which nowadays does the same as `RankNTypes') |
| 22:55:58 | × | jchia__ quits (~jchia@58.32.38.49) (Ping timeout: 246 seconds) |
| 22:56:05 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 22:56:24 | <ski> | koz_ : replace `exists v. IsOption v *> v' by a new type, say `SomeOption' |
| 22:57:46 | <ski> | koz_ : btw, you should note that `... -> (forall a. ..a..)' is logically equivalent to `forall a. (... -> ..a..)', and `(exists a. ..a..) -> ...' is logically equivalent to `forall a. (..a.. -> ...)' |
| 22:57:52 | × | ubert quits (~Thunderbi@p200300ecdf25d950e6b318fffe838f33.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 22:58:28 | <ski> | (and similarly, `T -> (C => U)' is equivalent to `C => (T -> U)', and `(C *> T) -> U' is also equivalent to `C => (T -> U)') |
| 22:58:39 | <koz_> | Hmm, interesting. |
| 22:58:50 | <Heffalump> | what are you trying to convey with *> ? |
| 22:59:08 | <ski> | (a value of type `C => T' is a value such that, if *you* (the user/consumer/caller) provides evidence for `C', then you may use the value as if having type `T') |
| 23:00:13 | <ski> | (otoh, a value of type `C *> T' carries with it *both* evidence for `C', and a value of type `T'. so, when *producing* such a value, you will need to produce evidence of `C'. while when producing a value of type `C => T', you may freely assume the user/consumer will hand you evidence for `C') |
| 23:00:42 | <ski> | `C => T' is akin to `C -> T' in the same way that `C *> T' is akin to `(C,T)' |
| 23:01:26 | <ski> | anyway, consider e.g. `length :: forall a. ([a] -> Int)'. by the above equivalence, this states the same as `length :: (exists a. [a]) -> Int' |
| 23:01:50 | <ski> | the former says : for all types `a', if we call `length' with a list of `a's, then we get an `Int' back |
| 23:02:02 | × | niekvandepas quits (~niekvande@dhcp-077-249-088-250.chello.nl) (Ping timeout: 272 seconds) |
| 23:02:14 | <ski> | the latter says : if we call `length', we'll get an `Int' back, provided there exists some type `a' such that the argument passed is a list of `a's |
| 23:02:49 | × | deviantfero quits (~deviantfe@190.150.27.58) (Quit: WeeChat 3.0) |
| 23:03:35 | <ski> | you may consider an `isSorted :: forall a. (Ord a => ([a] -> Bool))' function. by the equivalences above, this is the same as `isSorted :: forall a. ((Ord a *> [a]) -> Bool)' is the same as `isSorted :: (exists a. (Ord a *> [a])) -> Bool' |
| 23:04:02 | × | MidAutumnHotaru quits (~MidAutumn@unaffiliated/midautumnhotaru) (Quit: Ping timeout (120 seconds)) |
| 23:04:04 | <ski> | (you can call `isSorted' as long as there exists some type `a', that is an instance of `Ord', and the argument has type `[a]') |
| 23:04:22 | → | MidAutumnHotaru joins (~MidAutumn@unaffiliated/midautumnhotaru) |
| 23:04:24 | <ski> | (extra brackets in the type signatures, for emphasis/clarity) |
| 23:05:03 | → | aidecoe joins (~aidecoe@unaffiliated/aidecoe) |
| 23:05:30 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 23:05:38 | <ski> | (one can approximate `*>' in Haskell by `data cxt *> a = cxt => Provide a'. here `Provide :: cxt => (a -> (cxt *> a))'. compare with `(,) :: a -> (b -> (a,b))') |
| 23:06:07 | <ski> | koz_ : the type equivalences making any sense ? |
| 23:06:36 | <koz_> | Yeah, I think so. |
| 23:06:44 | <koz_> | Basically, I'm gonna take the short answer and go something like |
| 23:06:47 | → | hackerhercules joins (~hackerher@c-98-248-15-216.hsd1.ca.comcast.net) |
| 23:06:53 | <koz_> | ph88: Ask ski about such things not me. |
| 23:06:56 | <ski> | ok, so we want something like `type SomeOption = exists v. IsOption v *> v' |
| 23:07:22 | <ph88> | im going to safe this in a notepad |
| 23:07:50 | <ski> | in the first (data constructor) encoding, we have to make a new `data' type (`newtype' sadly doesn't work, in the case where there's no constraints) |
| 23:07:54 | <ski> | so, next attempt is |
| 23:08:10 | <ski> | data SomeOption = WrapOption (exists v. IsOption v *> v) |
| 23:08:32 | <ski> | if you prefer, you could use the alternative (`GADTSyntax') syntax for `data' declarations, which would look like |
| 23:08:36 | <ski> | data SomeOption |
| 23:08:37 | <ski> | where |
| 23:08:48 | <ski> | WrapOption :: (exists v. IsOption v *> v) -> SomeOption |
| 23:09:01 | <ski> | in both variants, we'd get the signature |
| 23:09:03 | <ski> | WrapOption :: (exists v. IsOption v *> v) -> SomeOption |
| 23:09:14 | <ski> | for the data constructor. and this is still pseudo-Haskell |
| 23:09:26 | <ski> | now, we apply the equivalences from above, to rewrite this into |
| 23:09:41 | <ski> | WrapOption :: forall v. ((IsOption v *> v) -> SomeOption) |
| 23:09:42 | <ski> | and then to |
| 23:09:50 | <ski> | WrapOption :: forall v. (IsOption v => (v -> SomeOption)) |
| 23:10:00 | <ski> | or, eliding redundant brackets, just |
| 23:10:05 | <ski> | WrapOption :: forall v. IsOption v => v -> SomeOption |
| 23:10:31 | <ski> | (compare with `length' and `isSorted' from above) |
| 23:10:48 | <ski> | now, *this* signature we can actually write in Haskell (with extensions) |
| 23:10:57 | <koz_> | You could be rather dirty here and then define an instance of IsOption for SomeOption. |
| 23:11:19 | <koz_> | (all of whose methods are just a lot of tedious GADT unpacking) |
| 23:11:31 | <koz_> | Wait actually, you can't, rofl. |
| 23:11:33 | <ski> | note that `SomeOption' encapsulates an existential, because there's a type variable, `v', which does not occur in the result type of the data constructor |
| 23:12:02 | <ski> | (so, it's really the data constructor, not the type itself, which encodes the existential. you could also have other data constructors, which don't encode existentials) |
| 23:12:14 | <ski> | anyway, to make this into valid Haskell-with-extensions, you say either |
| 23:12:31 | <ski> | data SomeOption = forall v. IsOption v => WrapOption v |
| 23:13:15 | <ski> | (the `forall' here should be read as : the data constructor can hide *any* type `v', as long as it's an instance of `IsOption'. the data constructor is polymorphic in `v') |
| 23:13:18 | <ski> | or else |
| 23:13:22 | <ski> | data SomeOption |
| 23:13:24 | <ski> | where |
| 23:13:29 | <ski> | WrapOption :: forall v. IsOption v => v -> SomeOption |
| 23:13:40 | <ski> | where in this case, we can elide the `forall', writing just |
| 23:13:44 | <ski> | WrapOption :: IsOption v => v -> SomeOption |
| 23:14:33 | → | madnight_ joins (~madnight@static.59.103.201.195.clients.your-server.de) |
| 23:14:34 | <ski> | koz_ : you can't ? |
| 23:14:43 | ski | has no idea how `IsOption' is defined |
| 23:14:47 | <koz_> | How would you write 'defaultValue :: a'. |
| 23:14:48 | × | madnight quits (~madnight@static.59.103.201.195.clients.your-server.de) (Quit: ZNC 1.7.1 - https://znc.in) |
| 23:14:48 | × | usr25 quits (~usr25@unaffiliated/usr25) (Quit: Leaving) |
| 23:15:12 | <ski> | Heffalump : did i manage to answer your question ? |
| 23:15:26 | <ski> | koz_ : context ? |
| 23:15:35 | <koz_> | Actually you still could. |
| 23:15:35 | → | Ishutin_ joins (~Ishutin@87-97-30-255.pool.digikabel.hu) |
| 23:15:41 | <koz_> | https://hackage.haskell.org/package/tasty-1.4.0.3/docs/Test-Tasty-Options.html#t:IsOption |
| 23:15:48 | <koz_> | I misread slightly becasue I was doing 10 other things. |
| 23:16:05 | <Heffalump> | ski: yes, thanks :-) |
| 23:16:08 | <ski> | koz_ : ah, i see |
| 23:16:44 | <ski> | Heffalump : anyway, it's notation that i made up, in here, many years ago, when talking about existentials to other people, and explaining them, and how they relate to constraints |
| 23:16:56 | × | tv quits (~tv@unaffiliated/tv) (Ping timeout: 240 seconds) |
| 23:17:35 | <Heffalump> | ski: fair enough |
| 23:17:36 | <ski> | (i've done variations of intros to existentials in here, rather many times now ..) |
| 23:17:55 | <Heffalump> | FWIW the constraints package is quite handy for actually working with constraints as values |
| 23:18:00 | <ski> | yes |
| 23:18:01 | × | Ishutin quits (~Ishutin@92-249-193-64.pool.digikabel.hu) (Ping timeout: 264 seconds) |
| 23:18:39 | × | conal quits (~conal@198.8.81.77) (Quit: Computer has gone to sleep.) |
| 23:18:45 | <koz_> | ski: Perhaps doing a monochrom is in order (aka, writing it up and having it online somewhere to link to people)? |
| 23:18:56 | <ski> | maybe some day |
| 23:19:00 | <koz_> | Student-oriented backstory optional. |
| 23:19:01 | <ski> | so far, i've been too lazy for that |
| 23:19:42 | <ski> | (also, i think my explanations have improved, over the years, by viewing it from different angles, and also by encountering different situations that people bring up, where existentials bear on the issue in some way) |
| 23:20:02 | × | poscat1 quits (~poscat@114.245.115.216) (Ping timeout: 260 seconds) |
| 23:20:03 | <ski> | koz_ : anyway, if you want to, i could mention the main other way to encode existentials, as well, while i'm at it ? |
| 23:20:16 | <koz_> | Sure, why not? |
| 23:20:22 | <koz_> | We're all here anyway. |
| 23:20:49 | <ski> | (also, one could go into more details about existentials, how to think about them, what one can do with them, perhaps some caveats. and relations to e.g. higher-rank stuff) |
| 23:21:29 | → | poscat joins (~poscat@114.245.115.216) |
| 23:21:37 | <ski> | (often i've started these intros with a more thorough intro to polymorphism and `forall', in particular stressing some details which i think help understanding how `forall' and `exists' relates to each other, and how they differ) |
| 23:22:39 | <ski> | anyway, the other encoding is the CPS (Continuation-Passing Style) encoding |
| 23:22:39 | <Heffalump> | ski: for added bonus points describe how it's done in F# :-) |
| 23:23:05 | → | tv joins (~tv@unaffiliated/tv) |
| 23:23:17 | → | DarukFromHyrule joins (542e199d@gateway/web/cgi-irc/kiwiirc.com/ip.84.46.25.157) |
| 23:23:26 | <ski> | Heffalump : hm, you mean like the static polymorphism (if i recall the name correctly) ? |
| 23:24:14 | <Heffalump> | ski: no, just a direct encoding of existentials with CPS - it just gets a bit annoying because of having to combine it with an encoding of higher-rank polymorphism. |
| 23:24:15 | <ski> | koz_ : anyway, have you seen the `Cont o' monad before ? |
| 23:24:20 | <koz_> | ski: Yes. |
| 23:24:29 | <koz_> | I've had to work with it (in various forms) recently. |
| 23:24:40 | <ski> | ok, so you should be somewhat familiar with seeing types like `(a -> o) -> o', then ? |
| 23:24:53 | <koz_> | Yep. |
| 23:24:59 | <koz_> | Again, in various forms. |
| 23:25:00 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Remote host closed the connection) |
| 23:25:15 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 23:25:29 | <ski> | note that `return :: a -> ((a -> o) -> o)' could be defined as `return a = ($ a)' (or `return a = \k -> k a' or `return a k = k a', if you prefer) |
| 23:25:45 | <monochrom> | O hai how can I help? :) |
| 23:25:55 | <monochrom> | Oh, that. |
| 23:26:29 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 23:26:44 | <ski> | koz_ : but note that not all values of type `(a -> o) -> o' are of form `\k -> k x', for some `x :: a' |
| 23:26:56 | <monochrom> | I have long accepted the selection bias that if someone has become an IRCer instead of a blogger, it is because they don't want to make a permanent once-and-for-all document. |
| 23:27:13 | <ski> | @type (`all` [2,3,5,7 :: Integer]) |
| 23:27:14 | <lambdabot> | (Integer -> Bool) -> Bool |
| 23:27:21 | <ski> | @type cont (`all` [2,3,5,7 :: Integer]) |
| 23:27:22 | <lambdabot> | Cont Bool Integer |
| 23:27:45 | <ski> | (`all` [2,3,5,7 :: Integer]) is `\k -> k 2 && k 3 && k 5 && k 7' |
| 23:28:11 | <monochrom> | But in the case of Cont r a or (a->r)->r, http://www.vex.net/~trebla/haskell/cont.xhtml |
| 23:28:19 | ski | nods |
| 23:28:30 | ski | looks at koz_ |
| 23:29:06 | <ski> | Heffalump : hm, i see |
| 23:29:31 | <Heffalump> | monochrom: I mostly stopped IRCing but I never started blogging. I guess I'm just lazy. |
| 23:29:50 | → | pavonia_ joins (~user@unaffiliated/siracusa) |
| 23:30:02 | <Heffalump> | ironically I do have a blog post about existentials in F#, but it's internal at work |
| 23:30:14 | <ski> | (in this case, the point isn't `Cont', but rather the version universally quantifying over the answer type. `Codensity Identity', if you like) |
| 23:30:23 | <ski> | Heffalump : aww, too bad :/ |
| 23:31:12 | <monochrom> | It is possible that working on (a->r)->r first helps with ∀r.(a->r)->r later. |
| 23:31:18 | <ski> | yes |
| 23:32:46 | → | carlomagno1 joins (~cararell@148.87.23.12) |
| 23:32:46 | × | deu quits (de@uio.re) (Ping timeout: 240 seconds) |
| 23:32:46 | × | pavonia quits (~user@unaffiliated/siracusa) (Ping timeout: 240 seconds) |
| 23:32:59 | pavonia_ | is now known as pavonia |
| 23:33:01 | × | carlomagno quits (~cararell@148.87.23.12) (Ping timeout: 264 seconds) |
| 23:33:50 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 23:33:50 | × | cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Read error: Connection reset by peer) |
| 23:34:10 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-106-113.w86-212.abo.wanadoo.fr) |
| 23:34:39 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 23:34:52 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 23:35:03 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood) |
| 23:35:07 | × | metreo quits (~Thunderbi@unaffiliated/metreo) (Quit: metreo) |
| 23:35:52 | × | adius quits (sid321344@gateway/web/irccloud.com/x-akpavffyaasqderl) (Ping timeout: 246 seconds) |
| 23:35:52 | × | dmj` quits (sid72307@gateway/web/irccloud.com/x-iewosydijsdukmsg) (Ping timeout: 246 seconds) |
| 23:36:00 | × | nhs quits (~nhs@c-24-20-87-79.hsd1.or.comcast.net) (Ping timeout: 256 seconds) |
| 23:36:01 | × | Firedancer quits (sid336191@gateway/web/irccloud.com/x-gtlpvcapzeuqwxzg) (Ping timeout: 264 seconds) |
| 23:36:13 | → | metreo joins (Thunderbir@gateway/vpn/mullvad/metreo) |
| 23:36:17 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 23:36:22 | × | lexi-lambda quits (sid92601@gateway/web/irccloud.com/x-csygfzivesdqoxgr) (Ping timeout: 260 seconds) |
| 23:36:25 | × | yahb quits (xsbot@haskell/bot/yahb) (Ping timeout: 240 seconds) |
| 23:36:34 | × | edwinb quits (sid69486@gateway/web/irccloud.com/x-eambhkarpptzvjfq) (Ping timeout: 265 seconds) |
| 23:36:37 | × | kupi quits (uid212005@gateway/web/irccloud.com/x-lcljveiqhawksjqz) (Read error: Connection reset by peer) |
| 23:36:37 | × | hnOsmium0001 quits (uid453710@gateway/web/irccloud.com/x-obbamytoysiptieo) (Read error: Connection reset by peer) |
| 23:36:38 | <ph88> | ski, why do you call ExistentialQuantification a misnomer ? |
| 23:36:45 | × | borne quits (~fritjof@200116b8641b4900438d15c340c1e8fe.dip.versatel-1u1.de) (Ping timeout: 272 seconds) |
| 23:36:51 | × | hamishmack quits (sid389057@gateway/web/irccloud.com/x-fucfppgjsuoyaurt) (Ping timeout: 268 seconds) |
| 23:36:55 | × | nick_h quits (sid319833@gateway/web/irccloud.com/x-kwcoegnoeruauebu) (Ping timeout: 246 seconds) |
| 23:36:57 | → | nhs joins (~nhs@c-24-20-87-79.hsd1.or.comcast.net) |
| 23:36:57 | × | Tritlo quits (sid58727@gateway/web/irccloud.com/x-ztesssmxwfujyabv) (Ping timeout: 260 seconds) |
| 23:36:57 | × | heyj quits (sid171370@gateway/web/irccloud.com/x-uudfnudbkkdvqztk) (Ping timeout: 260 seconds) |
| 23:36:57 | × | PoliticsII______ quits (sid193551@gateway/web/irccloud.com/x-ufujqhptyitxuagq) (Ping timeout: 260 seconds) |
| 23:36:57 | × | gluegadget quits (sid22336@gateway/web/irccloud.com/x-ejhqtoxqloyjxviw) (Ping timeout: 260 seconds) |
| 23:37:03 | → | adius joins (sid321344@gateway/web/irccloud.com/x-xzosmbbgxpzyuaxq) |
| 23:37:04 | → | mpickering_ joins (sid78412@gateway/web/irccloud.com/x-nlhzowtetdmoksio) |
| 23:37:12 | → | PoliticsII______ joins (sid193551@gateway/web/irccloud.com/x-yqgnnlehvwiyobbj) |
| 23:37:13 | × | SanchayanMaity quits (sid478177@gateway/web/irccloud.com/x-abgxgwzmanypeakf) (Ping timeout: 264 seconds) |
| 23:37:14 | × | mpickering quits (sid78412@gateway/web/irccloud.com/x-bmdkrpzszxynczwk) (Ping timeout: 264 seconds) |
| 23:37:14 | mpickering_ | is now known as mpickering |
| 23:37:21 | → | borne joins (~fritjof@2a06:8782:ffbb:1337:146f:6feb:7131:6215) |
| 23:37:25 | × | sagax quits (~sagax_nb@213.138.71.146) (Remote host closed the connection) |
| 23:37:26 | × | DTZUZU quits (~DTZUZU@205.ip-149-56-132.net) (Read error: Connection reset by peer) |
| 23:37:28 | × | benl23 quits (sid284234@gateway/web/irccloud.com/x-qrlnvldurzlpxkvd) (Ping timeout: 268 seconds) |
| 23:37:30 | × | forgottenone quits (~forgotten@176.42.21.112) (Ping timeout: 272 seconds) |
| 23:37:33 | × | simony quits (sid226116@gateway/web/irccloud.com/x-kqfgsijmdpcuknoe) (Ping timeout: 260 seconds) |
| 23:37:37 | → | affinespaces_ joins (sid327561@gateway/web/irccloud.com/x-bebojrcoufbnwpah) |
| 23:37:39 | → | DTZUZU joins (~DTZUZU@205.ip-149-56-132.net) |
| 23:37:41 | → | kupi joins (uid212005@gateway/web/irccloud.com/x-cknjqmjrxwpkvwqw) |
| 23:37:42 | → | SanchayanMaity joins (sid478177@gateway/web/irccloud.com/x-xfixrnosidhdkmvo) |
| 23:37:44 | → | acertain_ joins (sid470584@gateway/web/irccloud.com/x-ukmpkghtxinppagh) |
| 23:37:44 | × | alx741 quits (~alx741@186.178.110.213) (Quit: alx741) |
| 23:37:48 | → | Tritlo joins (sid58727@gateway/web/irccloud.com/x-lizgbcpbnixnerye) |
| 23:37:50 | × | rann quits (sid175221@gateway/web/irccloud.com/x-ivdplelrshviator) (Ping timeout: 264 seconds) |
| 23:38:01 | × | affinespaces quits (sid327561@gateway/web/irccloud.com/x-smororhywdobhsyf) (Ping timeout: 265 seconds) |
| 23:38:01 | → | rann joins (sid175221@gateway/web/irccloud.com/x-rebkjmgtrafnpeif) |
| 23:38:07 | × | acertain quits (sid470584@gateway/web/irccloud.com/x-laviekbaqfjfjwuo) (Ping timeout: 260 seconds) |
| 23:38:07 | × | dsturnbull quits (sid347899@gateway/web/irccloud.com/x-hptiydarodbrprwa) (Ping timeout: 260 seconds) |
| 23:38:08 | → | gluegadget joins (sid22336@gateway/web/irccloud.com/x-uqcwrzaflpkghsoy) |
| 23:38:08 | acertain_ | is now known as acertain |
| 23:38:08 | → | simony joins (sid226116@gateway/web/irccloud.com/x-wuwbandquivjrcox) |
| 23:38:11 | → | nick_h joins (sid319833@gateway/web/irccloud.com/x-ikiutvcdzbiuuesy) |
| 23:38:13 | → | Firedancer joins (sid336191@gateway/web/irccloud.com/x-eedluoddpkolzhde) |
| 23:38:14 | → | hamishmack joins (sid389057@gateway/web/irccloud.com/x-wekimeracfifvmya) |
| 23:38:19 | → | benl23 joins (sid284234@gateway/web/irccloud.com/x-cqkabivleljrbyfw) |
| 23:38:21 | → | hnOsmium0001 joins (uid453710@gateway/web/irccloud.com/x-uijdyahdbrrobyxg) |
| 23:38:23 | → | heyj joins (sid171370@gateway/web/irccloud.com/x-bflehhffxpswalwj) |
| 23:38:29 | → | dmj` joins (sid72307@gateway/web/irccloud.com/x-orqoyluhohfgpsiw) |
| 23:38:41 | affinespaces_ | is now known as affinespaces |
| 23:39:01 | → | edwinb joins (sid69486@gateway/web/irccloud.com/x-mayongskwkdlziau) |
| 23:39:09 | → | lexi-lambda joins (sid92601@gateway/web/irccloud.com/x-zhabaycedniqzhzc) |
| 23:40:03 | → | carlomagno joins (~cararell@148.87.23.12) |
| 23:40:11 | → | dsturnbull joins (sid347899@gateway/web/irccloud.com/x-vmumozmnyaqkkdty) |
| 23:40:35 | <ski> | ph88 : because it doesn't enable existentially quantifying type variables |
| 23:40:50 | <ski> | it enables a particular *encoding* of them |
| 23:40:56 | × | carlomagno1 quits (~cararell@148.87.23.12) (Ping timeout: 240 seconds) |
| 23:41:13 | <ski> | universal quantification to me is `forall a. ..a..'. existential quantification is `exists a. ..a..' |
| 23:41:43 | × | Franciman quits (~francesco@host-95-235-155-82.retail.telecomitalia.it) (Quit: Leaving) |
| 23:41:58 | <ski> | (some other concrete syntax might be used, that's immaterial. but it must be a (type) expression form, not something requiring circumlocations like having to invent a new `data' type) |
| 23:42:51 | → | yahb joins (xsbot@178.219.36.155) |
| 23:42:51 | × | yahb quits (xsbot@178.219.36.155) (Changing host) |
| 23:42:51 | → | yahb joins (xsbot@haskell/bot/yahb) |
| 23:42:54 | <nshepperd> | one day ghc will add an actual exists keyword, under the extension ActuallyExistentialQuantification |
| 23:43:00 | → | conal joins (~conal@209.58.135.89) |
| 23:43:48 | → | nrh^ joins (nrh@ip98-184-89-2.mc.at.cox.net) |
| 23:43:58 | → | deu joins (de@uio.re) |
| 23:44:01 | <koz_> | nshepperd: ExistentialExistentialQuantification |
| 23:44:10 | <koz_> | (as in, existential quantification which actually exists) |
| 23:44:16 | <ski> | the current `ExistentialQuantification' would, imho, be better named something like `ExistentialDataConstructors' |
| 23:44:31 | <ski> | conasider e.g. |
| 23:44:37 | <ski> | data Expr a = Lit a |
| 23:45:11 | <ski> | | forall b. App (Expr (b -> a)) (Expr b) |
| 23:45:27 | <ski> | | If (Expr Bool) (Expr a) (Expr a) |
| 23:45:41 | <ski> | (you can imagine more data constructors) |
| 23:45:46 | <ski> | note that here |
| 23:45:51 | × | jackk_ quits (~jackk@205.178.111.134) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 23:45:56 | <ski> | App :: Expr (b -> a) -> (Expr b -> Expr a) |
| 23:46:07 | <ski> | we can e.g. write now a function |
| 23:46:13 | <ski> | eval :: Expr a -> a |
| 23:46:19 | <ski> | eval (List x) = x |
| 23:46:32 | <ski> | eval (App ef ex) = (eval ef) (eval ex) |
| 23:46:50 | <ski> | eval (If eb et ee) = if eval eb then eval et else eval ee |
| 23:47:35 | <ski> | the data constructor `App' here is "existential, in the sense that `App' expresses (more or less) `App :: (exists b. (Expr (b -> a),Expr b)) -> Expr a' |
| 23:47:52 | <ski> | (except that that formulation requires uncurrying/tupling the data constructor) |
| 23:48:46 | <ski> | (but `Lit' and `If' aren't "existential". so it's rather a property of the data constructor, not of the data type itself, primarily) |
| 23:48:48 | → | Codaraxis joins (Codaraxis@gateway/vpn/mullvad/codaraxis) |
| 23:49:30 | → | philopsos joins (~caecilius@gateway/tor-sasl/caecilius) |
| 23:49:59 | <srid> | How do you inject raw HTML value as-is in Snap's `heist` templates? |
| 23:50:05 | <ski> | koz_ : anyway .. i was waiting for confirmation to continue about the CPS stuff |
| 23:50:07 | <monochrom> | data Frankenstein'sMonster = C1 (forall a. ...) | forall a. C2 ... :) |
| 23:50:14 | <koz_> | ski: Don't let me stop you. |
| 23:50:34 | <ski> | (yes, the placement of the `forall's there are crucial, lead to opposite meaning) |
| 23:51:11 | <ski> | well .. i tend to prefer letting my explanations be a bit more interactive, if possible |
| 23:52:37 | <ski> | (i have in the past ranted for more than an hour, with mostly no interaction .. and people have thanked me for it. but i think it's better if the other party doesn't stumble on some initial hurdle and can't grok the continuation because of that) |
| 23:52:42 | × | tromp quits (~tromp@dhcp-077-249-230-040.chello.nl) (Remote host closed the connection) |
| 23:52:53 | <monochrom> | :) |
| 23:54:38 | × | shatriff quits (~vitaliish@176-52-216-242.irishtelecom.com) (Remote host closed the connection) |
| 23:55:11 | → | shatriff joins (~vitaliish@176-52-216-242.irishtelecom.com) |
| 23:55:14 | <ski> | so, anyway .. i brought up the topic of the CPS type `(a -> o) -> o', and to what extent values of it are of the form `\k -> k x', for some `x :: a' |
| 23:55:27 | <ski> | koz_ : did you follow my `all' example ? |
| 23:55:39 | <koz_> | ski: Yes. I get how Cont r a behaves. |
| 23:55:47 | <ski> | ok |
| 23:55:48 | <koz_> | (with some help from the type checker) |
| 23:55:53 | <koz_> | (but the idea makes sense) |
| 23:56:10 | × | metreo quits (Thunderbir@gateway/vpn/mullvad/metreo) (Quit: metreo) |
| 23:56:23 | × | Kronic quits (sid480486@gateway/web/irccloud.com/x-qcpyvuxebnsxbmdz) (Ping timeout: 265 seconds) |
| 23:56:37 | <ski> | so, the reason that we're able to construct `\k -> k 2 && k 3 && k 5 && k 7' (which is *not* of the above form), is because of the specificity of the type `o' here .. that we know `o' is specifically `Bool' |
| 23:56:38 | → | __minoru__shirae joins (~shiraeesh@5.101.59.137) |
| 23:56:59 | <ski> | because of that, we can call `k' multiple times, getting multiple `Bool's, and then combine them in some way to get the final `Bool' |
| 23:57:08 | × | shiraeeshi quits (~shiraeesh@77.94.25.134) (Ping timeout: 272 seconds) |
| 23:57:27 | → | renzhi joins (~renzhi@2607:fa49:6500:6f00::1e43) |
| 23:57:28 | <koz_> | Yep. |
| 23:57:44 | → | Kronic joins (sid480486@gateway/web/irccloud.com/x-bjshlkomyddejefl) |
| 23:58:12 | <ski> | (you could also note that, in the CPS terminology, the body of that function is *not* in Continuation-Passing Style, because the calls to `k' are not in "tail position", aren't tail calls. we "do something after them", namely we call `(&&)') |
| 23:58:36 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 23:59:15 | <ski> | now, if we instead consider the universal type `forall o. (a -> o) -> o', then a piece of code implementing a value of this type can't do the same trick, because it doesn't know what type the user will pick for `o' |
All times are in UTC on 2021-01-28.