Logs: freenode/#haskell
| 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.