Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→ 502,152 events total
2020-11-26 15:53:42 <maerwald> only going down, how depressing
2020-11-26 15:53:59 × adm_ quits (~adm@43.229.89.234) (Remote host closed the connection)
2020-11-26 15:54:13 keviv joins (~keviv@35.142.17.117)
2020-11-26 15:55:06 <dminuoso> Would it help if Down was renamed to Depress?
2020-11-26 15:55:08 × Sheilong quits (uid293653@gateway/web/irccloud.com/x-xzqgkxnkzvzsvgqp) (Quit: Connection closed for inactivity)
2020-11-26 15:55:29 <hc> lol
2020-11-26 15:56:56 adm_ joins (~adm@43.229.89.234)
2020-11-26 15:57:57 × adm_ quits (~adm@43.229.89.234) (Remote host closed the connection)
2020-11-26 16:01:15 lfa33 joins (3eb2f497@62-178-244-151.cable.dynamic.surfer.at)
2020-11-26 16:02:16 × lfa33 quits (3eb2f497@62-178-244-151.cable.dynamic.surfer.at) (Remote host closed the connection)
2020-11-26 16:02:34 adm_ joins (~adm@43.229.89.234)
2020-11-26 16:04:00 × jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection)
2020-11-26 16:04:24 jpds joins (~jpds@gateway/tor-sasl/jpds)
2020-11-26 16:05:18 × subttle quits (~anonymous@unaffiliated/subttle) (Quit: leaving)
2020-11-26 16:06:30 × knupfer quits (~Thunderbi@200116b82c0c5800d512095bbf5d3f0d.dip.versatel-1u1.de) (Quit: knupfer)
2020-11-26 16:06:39 knupfer joins (~Thunderbi@200116b82c0c5800c8e579458ff3eb4f.dip.versatel-1u1.de)
2020-11-26 16:07:08 mpereira joins (~mpereira@2a02:810d:f40:d96:857:5d24:8b16:e48)
2020-11-26 16:07:20 × adm_ quits (~adm@43.229.89.234) (Ping timeout: 265 seconds)
2020-11-26 16:08:37 vicfred joins (~vicfred@unaffiliated/vicfred)
2020-11-26 16:09:10 × raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds)
2020-11-26 16:09:50 Chi1thangoo joins (~Chi1thang@87.112.60.168)
2020-11-26 16:10:42 × acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 256 seconds)
2020-11-26 16:13:50 × royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed)
2020-11-26 16:14:14 royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9)
2020-11-26 16:16:43 × jonathanx quits (~jonathan@dyn-8-sc.cdg.chalmers.se) (Remote host closed the connection)
2020-11-26 16:18:36 × royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 240 seconds)
2020-11-26 16:18:49 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 264 seconds)
2020-11-26 16:20:38 <zfnmxt> I'm having some trouble with type families and ambiguous variables during type inference: https://www.pastery.net/gfxvnp/
2020-11-26 16:20:52 × Iceland_jack quits (~user@31.124.48.169) (Ping timeout: 265 seconds)
2020-11-26 16:21:40 <zfnmxt> I don't know how to constraint things further so that b0 can be resolved.
2020-11-26 16:21:55 geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr)
2020-11-26 16:22:00 hackage phonetic-languages-simplified-properties-lists 0.1.3.0 - A generalization of the uniqueness-periods-vector-properties package. https://hackage.haskell.org/package/phonetic-languages-simplified-properties-lists-0.1.3.0 (OleksandrZhabenko)
2020-11-26 16:22:02 <zfnmxt> s/constraint/constrain
2020-11-26 16:25:09 <boxscape> zfnmxt have you tried supplying b to left with -XTypeApplications?
2020-11-26 16:28:09 × andos quits (~dan@69-165-210-185.cable.teksavvy.com) (Quit: Leaving)
2020-11-26 16:29:35 danso joins (~dan@69-165-210-185.cable.teksavvy.com)
2020-11-26 16:29:40 p-core joins (~Thunderbi@2001:718:1e03:5128:2ab7:7f35:48a1:8515)
2020-11-26 16:31:07 × Yumasi quits (~guillaume@2a01:e0a:5cb:4430:5572:c108:3697:b06d) (Ping timeout: 260 seconds)
2020-11-26 16:33:44 santa_1 joins (~santa_@217.146.82.202)
2020-11-26 16:37:58 × geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 256 seconds)
2020-11-26 16:39:32 <zfnmxt> boxscape: Did you mean something like this? https://www.pastery.net/gfxvnp+sjqkje/#sjqkje
2020-11-26 16:40:00 hackage reflex-dom-retractable 0.1.7.0 - Routing and retractable back button for reflex-dom https://hackage.haskell.org/package/reflex-dom-retractable-0.1.7.0 (NCrashed)
2020-11-26 16:43:00 royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9)
2020-11-26 16:43:00 hackage reflex-localize 1.0.1.0 - Localization library for reflex https://hackage.haskell.org/package/reflex-localize-1.0.1.0 (NCrashed)
2020-11-26 16:43:32 <boxscape> zfnmxt is Func a type family?
2020-11-26 16:43:59 <boxscape> or a type?
2020-11-26 16:45:16 × raichoo quits (~raichoo@dslb-092-073-219-149.092.073.pools.vodafone-ip.de) (Quit: Lost terminal)
2020-11-26 16:45:35 <zfnmxt> boxscape: It's a GADT: https://github.com/aleatory-science/frechet-dsl/blob/c7185e3aa1894e2cf3f45be4ee7506b5ad695a7d/src/Frechet/Ast.hs#L15
2020-11-26 16:46:07 <boxscape> zfnmxt is that a private repository? I'm getting a 404
2020-11-26 16:46:08 × csaba_hruska quits (~csaba@188-167-252-60.dynamic.chello.sk) (Quit: leaving)
2020-11-26 16:46:47 machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca)
2020-11-26 16:47:02 <zfnmxt> Ah, crap. Forgot about that. Here's the relevant line: https://www.pastery.net/gfxvnp+sjqkje+xwaqdc/#xwaqdc
2020-11-26 16:48:48 × chele quits (~chele@ip5b416ea2.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2020-11-26 16:49:01 hackage reflex-localize 1.0.2.0 - Localization library for reflex https://hackage.haskell.org/package/reflex-localize-1.0.2.0 (NCrashed)
2020-11-26 16:50:56 × tabemann quits (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Ping timeout: 240 seconds)
2020-11-26 16:52:14 × avdb quits (~avdb@ip-81-11-215-86.dsl.scarlet.be) (Ping timeout: 272 seconds)
2020-11-26 16:52:36 <boxscape> zfnmxt so I think the problem right now is that it doesn't know that n is 0, because of how you're matching on the fromSing call. Let me see if I can remember how to do that better...
2020-11-26 16:52:40 coot joins (~coot@37.30.48.178.nat.umts.dynamic.t-mobile.pl)
2020-11-26 16:52:49 alp joins (~alp@2a01:e0a:58b:4920:2df3:524d:ce61:8fe1)
2020-11-26 16:53:11 avdb joins (~avdb@ip-81-11-215-86.dsl.scarlet.be)
2020-11-26 16:53:22 <zfnmxt> boxscape: I suspected that might be a problem (and I remain confused about `Nat` in general--why aren't there `SZero` and `SS` constructors to match on?)
2020-11-26 16:53:26 × Feuermagier quits (~Feuermagi@213.178.26.41) (Remote host closed the connection)
2020-11-26 16:53:42 <boxscape> zfnmxt yeah I tend to avoid the built-in Nats for that reason
2020-11-26 16:54:01 × ubert quits (~Thunderbi@2a02:8109:9880:303c:ca5b:76ff:fe29:f233) (Remote host closed the connection)
2020-11-26 16:54:06 <zfnmxt> Is there a reason the built-ins don't export (or...lack?) the constructors?
2020-11-26 16:54:16 acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net)
2020-11-26 16:54:19 maroloccio joins (~marolocci@2a02:8084:221:ce00:164f:8aff:fed8:411d)
2020-11-26 16:54:54 <boxscape> zfnmxt I believe they're built to be efficient, e.g., if you have 1000 :: Nat, you don't want to carry around 1000 constructors if you don't need them
2020-11-26 16:55:18 <boxscape> zfnmxt it might be worth switching to a library that provides Z/S nats though for this, or rolling your own
2020-11-26 16:55:24 × louisac quits (4d64ab42@cpc82915-enfi22-2-0-cust65.20-2.cable.virginm.net) (Remote host closed the connection)
2020-11-26 16:55:56 <boxscape> with that I believe you could just do `case n of SZ -> left`
2020-11-26 16:56:12 <zfnmxt> boxscape: I'll try!
2020-11-26 16:57:04 <boxscape> (zfnmxt: this for example, which has singletons integration https://hackage.haskell.org/package/singleton-nats-0.4.5/docs/Data-Nat.html)
2020-11-26 16:57:23 × coot quits (~coot@37.30.48.178.nat.umts.dynamic.t-mobile.pl) (Ping timeout: 256 seconds)
2020-11-26 16:58:14 coot joins (~coot@37.30.48.178.nat.umts.dynamic.t-mobile.pl)
2020-11-26 16:58:39 × aplainzetakind quits (~johndoe@captainludd.powered.by.lunarbnc.net) (Quit: Free ZNC ~ Powered by LunarBNC: https://LunarBNC.net)
2020-11-26 16:59:36 × merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds)
2020-11-26 17:00:13 aplainzetakind joins (~johndoe@captainludd.powered.by.lunarbnc.net)
2020-11-26 17:00:15 × christo quits (~chris@81.96.113.213) (Remote host closed the connection)
2020-11-26 17:01:15 merijn joins (~merijn@83-160-49-249.ip.xs4all.nl)
2020-11-26 17:01:44 × larou quits (5eae2591@gateway/web/cgi-irc/kiwiirc.com/ip.94.174.37.145) (Quit: Connection closed)
2020-11-26 17:02:24 <zfnmxt> boxscape: That fixed it :)
2020-11-26 17:02:29 <boxscape> nice
2020-11-26 17:02:45 <zfnmxt> Thanks a lot for the help!
2020-11-26 17:02:51 <boxscape> np
2020-11-26 17:03:36 × Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Ping timeout: 240 seconds)
2020-11-26 17:04:41 Sheilong joins (uid293653@gateway/web/irccloud.com/x-euqghorjjrswhrff)
2020-11-26 17:05:09 christo joins (~chris@81.96.113.213)
2020-11-26 17:08:31 × kritzefitz quits (~kritzefit@fw-front.credativ.com) (Remote host closed the connection)
2020-11-26 17:09:04 jonatanb joins (~jonatanb@83.24.220.252.ipv4.supernova.orange.pl)
2020-11-26 17:09:41 × christo quits (~chris@81.96.113.213) (Ping timeout: 265 seconds)
2020-11-26 17:09:43 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 240 seconds)
2020-11-26 17:10:39 × bifunc2 quits (bifunc2@gateway/vpn/protonvpn/bifunc2) (Quit: -)
2020-11-26 17:10:45 conal joins (~conal@64.71.133.70)
2020-11-26 17:11:05 raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2020-11-26 17:13:51 sord937 joins (~sord937@gateway/tor-sasl/sord937)
2020-11-26 17:14:06 Lycurgus joins (~niemand@98.4.114.74)
2020-11-26 17:18:50 × jonatanb quits (~jonatanb@83.24.220.252.ipv4.supernova.orange.pl) (Ping timeout: 272 seconds)
2020-11-26 17:19:00 <zfnmxt> boxscape: Unfortunately, I spoke too soon. It only works for the `n = SS SZ` case (I changed it so that `nth` is 1-indexed) if you type `nth` as `nth :: forall n x xs. Sing n -> HList (x ': xs) -> Lookup (x ': xs) n` (and it doesn't work for any case with a larger n). So it seems like the explicit `x ': xs` type pattern is what enabled the inference.
2020-11-26 17:19:12 <zfnmxt> https://www.pastery.net/gfxvnp+sjqkje+xwaqdc+rzupwz/#rzupwz

All times are in UTC.