Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 .. 5022
— 502,152 events total
2020-11-19 00:44:55 → fr33domlover joins (~fr33domlo@fsf/member/fr33domlover)
2020-11-19 00:46:23 <dolio> Yeah, an analogous type family would work. That it does work is a massive difference in expectation of what they mean, more or less.
2020-11-19 00:46:25 × Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 240 seconds)
2020-11-19 00:46:39 <dolio> Like, type families are assuming that all the things they operate over have decidable equality.
2020-11-19 00:47:05 <boxscape> Oh, that's interesting
2020-11-19 00:47:39 <dolio> I guess in some ways it's not even that, though.
2020-11-19 00:47:52 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45)
2020-11-19 00:48:27 × nbloomf quits (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45) (Client Quit)
2020-11-19 00:48:48 <dolio> Because the actual behavior is like, 'if you ever figure out that m = n, then `foo m n` reduces to one thing, and if you figure out that m /= n, it reduces to another.'
2020-11-19 00:49:16 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-19 00:49:55 <boxscape> oh, yeah.. I thought it would work in agda if you wrote {a} {.a}, but with your it doesn't sound like it, and indeed, it says "Failed to infer the value of dotted pattern".
2020-11-19 00:50:09 <boxscape> s/with your/with your explanation
2020-11-19 00:50:17 × bergey quits (~user@pool-74-108-99-127.nycmny.fios.verizon.net) (Remote host closed the connection)
2020-11-19 00:50:19 <dolio> No, .a is for when you match on a proof that two things are equal.
2020-11-19 00:50:51 <boxscape> RIght, okay
2020-11-19 00:51:03 <boxscape> So it's very different from saying @a @a in a type family
2020-11-19 00:51:26 <dolio> Yeah.
2020-11-19 00:51:49 × DataComp_ quits (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net) (Remote host closed the connection)
2020-11-19 00:54:30 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds)
2020-11-19 00:54:46 → rogue_cheddar joins (~manjaro-u@2806:1000:8003:2a54:da9a:e457:f660:288a)
2020-11-19 00:55:37 <dolio> Anyhow, if you don't want things to get stuck, which is important in Agda, then decidable equality is kind of important for justifying that sort of matching.
2020-11-19 00:56:07 → nbloomf joins (~nbloomf@2600:1700:ad14:3020:6c29:bc9c:b97a:2b45)
2020-11-19 00:56:19 <dolio> Whereas type families are kind of based on the idea of adding things that get stuck, and specifying certain scenarios where they become unstuck, with no guarantee that all scenarios are covered.
2020-11-19 00:56:37 × wpcarro quits (sid397589@gateway/web/irccloud.com/x-jyvrhcovkjnuufaq) (Ping timeout: 260 seconds)
2020-11-19 00:57:36 <boxscape> hmm I wonder how this pretend-dec-eq-ness will work when you try to match on unsaturated type families once those are merged
2020-11-19 00:57:44 <boxscape> I guess maybe it'll just get stuck
2020-11-19 00:58:21 × Tuplanolla quits (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) (Quit: Leaving.)
2020-11-19 00:59:24 → wpcarro joins (sid397589@gateway/web/irccloud.com/x-mptadpaqtazralft)
2020-11-19 00:59:33 × xsperry quits (~as@unaffiliated/xsperry) (Ping timeout: 260 seconds)
2020-11-19 01:01:14 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-19 01:02:13 → Tesseraction joins (~Tesseract@unaffiliated/tesseraction)
2020-11-19 01:02:54 × thc202 quits (~thc202@unaffiliated/thc202) (Quit: thc202)
2020-11-19 01:03:00 <ski> boxscape : yes, you'd need `sameNat {false} {false} = just refl; sameNat {true} {true} = just refl; sameNat = nothing', pretty sure
2020-11-19 01:03:47 <boxscape> yeah, that does work
2020-11-19 01:05:37 × jneira quits (02896ac0@gateway/web/cgi-irc/kiwiirc.com/ip.2.137.106.192) (Ping timeout: 264 seconds)
2020-11-19 01:05:38 × chkno quits (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net) (Read error: Connection reset by peer)
2020-11-19 01:06:01 → chkno joins (~chkno@75-7-2-127.lightspeed.sntcca.sbcglobal.net)
2020-11-19 01:06:30 <p0a> /quit bye
2020-11-19 01:06:32 × p0a quits (~user@unaffiliated/p0a) (Quit: bye)
2020-11-19 01:06:39 × SupaYoshi quits (~supayoshi@213-10-140-13.fixed.kpn.net) (Ping timeout: 260 seconds)
2020-11-19 01:08:14 → cosimone joins (~cosimone@5.171.24.92)
2020-11-19 01:08:19 ← iqubic parts (~user@2601:602:9500:4870:18b7:5f73:2db2:1881) ("ERC (IRC client for Emacs 28.0.50)")
2020-11-19 01:09:18 → vicfred joins (~vicfred@unaffiliated/vicfred)
2020-11-19 01:13:25 × m0rphism quits (~m0rphism@HSI-KBW-095-208-098-207.hsi5.kabel-badenwuerttemberg.de) (Ping timeout: 264 seconds)
2020-11-19 01:13:49 → SupaYoshi joins (~supayoshi@213-10-140-13.fixed.kpn.net)
2020-11-19 01:17:10 × elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Quit: Leaving)
2020-11-19 01:17:45 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds)
2020-11-19 01:19:14 → DataComputist joins (~lumeng@static-50-43-26-251.bvtn.or.frontiernet.net)
2020-11-19 01:20:37 → Tourist joins (~tourist@da.tourist.sh)
2020-11-19 01:20:37 × Tourist quits (~tourist@da.tourist.sh) (Changing host)
2020-11-19 01:20:37 → Tourist joins (~tourist@unaffiliated/tourist)
2020-11-19 01:20:41 → christo joins (~chris@81.96.113.213)
2020-11-19 01:21:14 → nuncanada joins (~dude@179.235.160.168)
2020-11-19 01:21:27 → guest1119 joins (~user@49.5.6.87)
2020-11-19 01:25:32 × nek0 quits (~nek0@mail.nek0.eu) (Ping timeout: 260 seconds)
2020-11-19 01:25:45 × cgfuh quits (~cgfuh@181.167.191.58) (Ping timeout: 240 seconds)
2020-11-19 01:27:03 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-19 01:30:34 → i8ucl joins (~manjaro-u@201.130.137.230.dsl.dyn.telnor.net)
2020-11-19 01:31:07 × rogue_cheddar quits (~manjaro-u@2806:1000:8003:2a54:da9a:e457:f660:288a) (Ping timeout: 272 seconds)
2020-11-19 01:32:06 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds)
2020-11-19 01:32:45 × Rudd0 quits (~Rudd0@185.189.115.103) (Ping timeout: 240 seconds)
2020-11-19 01:33:16 × cr3 quits (~cr3@192-222-143-195.qc.cable.ebox.net) (Quit: leaving)
2020-11-19 01:33:24 → magnuscake joins (~magnuscak@103.44.33.121)
2020-11-19 01:33:36 → Lord_of_Life_ joins (~Lord@46.217.218.252)
2020-11-19 01:33:36 × Lord_of_Life quits (~Lord@46.217.217.18) (Ping timeout: 240 seconds)
2020-11-19 01:34:31 hackage citeproc 0.2 - Generates citations and bibliography from CSL styles. https://hackage.haskell.org/package/citeproc-0.2 (JohnMacFarlane)
2020-11-19 01:35:47 × magnuscake quits (~magnuscak@103.44.33.121) (Client Quit)
2020-11-19 01:37:03 → wh0 joins (~wh0000@cpc152777-shef18-2-0-cust223.17-1.cable.virginm.net)
2020-11-19 01:37:05 → elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net)
2020-11-19 01:42:42 → nek0 joins (~nek0@mail.nek0.eu)
2020-11-19 01:44:51 × Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa)
2020-11-19 01:47:29 × nek0 quits (~nek0@mail.nek0.eu) (Client Quit)
2020-11-19 01:49:07 → nek0 joins (~nek0@mail.nek0.eu)
2020-11-19 01:52:07 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2020-11-19 01:52:51 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2020-11-19 02:06:19 <guest1119> case parse (spaces >> symbol) "lisp" input of ...
2020-11-19 02:06:27 <guest1119> what "lisp" and input here mean?
2020-11-19 02:06:40 <guest1119> parse :: Stream s Identity t => Parsec s () a -> SourceName -> s -> Either ParseError a
2020-11-19 02:06:52 <guest1119> from https://hackage.haskell.org/package/parsec-3.1.14.0/docs/Text-Parsec.html
2020-11-19 02:07:25 × wh0 quits (~wh0000@cpc152777-shef18-2-0-cust223.17-1.cable.virginm.net) (Ping timeout: 264 seconds)
2020-11-19 02:07:46 <guest1119> also, what do Stream s Identity t constraint? constraint for s? not t?
2020-11-19 02:08:37 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-19 02:10:47 <glguy> "lisp" is the name of the input
2020-11-19 02:11:01 <glguy> Often that's a filename or some other description
2020-11-19 02:13:19 → christo joins (~chris@81.96.113.213)
2020-11-19 02:15:44 <Axman6> s appears to be the type of impot that's being parsed, to probably usually a String or Text
2020-11-19 02:15:51 <Axman6> input*
2020-11-19 02:17:49 → xsperry joins (~as@unaffiliated/xsperry)
2020-11-19 02:18:44 → toorevitimirp joins (~tooreviti@117.182.180.118)
2020-11-19 02:23:00 × jakob_ quits (~textual@p200300f49f162200756a589588d5c172.dip0.t-ipconnect.de) (Quit: My Laptop has gone to sleep. ZZZzzz…)
2020-11-19 02:23:44 × conal quits (~conal@66.115.157.132) (Quit: Computer has gone to sleep.)
2020-11-19 02:24:46 <Axman6> guest1119: does that help at all?
2020-11-19 02:30:34 <guest1119> Axman6: yes
2020-11-19 02:30:50 <guest1119> but why we would give input a name?
2020-11-19 02:31:03 <guest1119> case (parse numbers "" "11, 2, 43") of
2020-11-19 02:31:15 <guest1119> numbers = commaSep integer
2020-11-19 02:31:43 × acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 260 seconds)
2020-11-19 02:31:44 <guest1119> this give "11, 2, 43" a "" name?
2020-11-19 02:33:25 × st8less quits (~st8less@2603:a060:11fd:0:9539:fd10:c1ca:1d78) (Quit: WeeChat 2.9)
2020-11-19 02:37:40 × guest1119 quits (~user@49.5.6.87) (Remote host closed the connection)
←Prev  Next→
Page 1 .. 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 .. 5022

All times are in UTC.