Logs: freenode/#haskell
| 2021-04-26 15:34:27 | <ski> | sshine : also in `Vector' and `Array' |
| 2021-04-26 15:34:51 | → | rann joins (sid175221@gateway/web/irccloud.com/x-ispnvynichnxaxzh) |
| 2021-04-26 15:35:14 | <ski> | (OCaml calls it `init') |
| 2021-04-26 15:39:34 | → | justanotheruser joins (~justanoth@unaffiliated/justanotheruser) |
| 2021-04-26 15:40:04 | → | seven_three joins (~user@pool-96-233-64-53.bstnma.fios.verizon.net) |
| 2021-04-26 15:40:15 | <Athas> | sshine: yes, it's an homage to the Good ML. |
| 2021-04-26 15:40:32 | <Athas> | But it's a weird name, like so much else in SML. |
| 2021-04-26 15:42:18 | × | martin02 quits (~martin02@hund.fs.lmu.de) (Quit: WeeChat 2.3) |
| 2021-04-26 15:42:39 | ← | seven_three parts (~user@pool-96-233-64-53.bstnma.fios.verizon.net) () |
| 2021-04-26 15:43:48 | × | chomwitt quits (~alexander@2a02:587:dc0a:2700:dc6:16ac:a95:eabf) (Remote host closed the connection) |
| 2021-04-26 15:44:21 | <Franciman> | I have written the following liquid haskell constraints: https://bpa.st/7NVQ and they work |
| 2021-04-26 15:44:31 | <Franciman> | but now I'd like to state, at line 18 |
| 2021-04-26 15:44:35 | <Franciman> | the following: |
| 2021-04-26 15:44:39 | × | lleb quits (5c91ba7e@amarseille-158-1-23-126.w92-145.abo.wanadoo.fr) (Quit: Connection closed) |
| 2021-04-26 15:44:51 | <Franciman> | {-@ piecesSpan :: p:[Piece] -> {n:Int | len p > 0 <=> n > 0} @-} |
| 2021-04-26 15:44:56 | <Franciman> | but I can't make it type check |
| 2021-04-26 15:44:58 | <Franciman> | in any way |
| 2021-04-26 15:46:08 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:8cfe:e2c:fb24:3adc) |
| 2021-04-26 15:47:17 | → | ep1ctetus joins (~epictetus@ip72-194-54-201.sb.sd.cox.net) |
| 2021-04-26 15:47:49 | → | v01d4lph4 joins (~v01d4lph4@27.57.103.213) |
| 2021-04-26 15:48:45 | <Franciman> | I mean |
| 2021-04-26 15:49:01 | <Franciman> | I can typecheck something equivalent |
| 2021-04-26 15:49:03 | <Franciman> | but not this |
| 2021-04-26 15:49:03 | <Franciman> | lol |
| 2021-04-26 15:49:19 | → | idhugo_ joins (~idhugo@80-62-116-231-mobile.dk.customer.tdc.net) |
| 2021-04-26 15:49:25 | <Franciman> | I suppose it is because we don't have decidability |
| 2021-04-26 15:49:32 | <Franciman> | proved for > |
| 2021-04-26 15:49:59 | <Franciman> | I can type check this condition |
| 2021-04-26 15:50:01 | <Franciman> | (len p > 0 && n > 0) || (len p == 0 && n == 0) |
| 2021-04-26 15:50:03 | <Franciman> | but not |
| 2021-04-26 15:50:11 | <Franciman> | len p > 0 <=> n > 0 |
| 2021-04-26 15:50:41 | <Franciman> | <Franciman> I suppose it is because we don't have decidability <- *totality |
| 2021-04-26 15:50:53 | × | kritzefitz quits (~kritzefit@2003:5b:203b:200::10:49) (Remote host closed the connection) |
| 2021-04-26 15:51:50 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 2021-04-26 15:52:15 | → | ddellac__ joins (~ddellacos@83.143.246.104) |
| 2021-04-26 15:53:43 | × | Sgeo quits (~Sgeo@ool-18b9875e.dyn.optonline.net) (Read error: Connection reset by peer) |
| 2021-04-26 15:54:37 | <ski> | hm, `generate' sounds more weird, to me |
| 2021-04-26 15:55:53 | → | Ariakenom joins (~Ariakenom@2001:9b1:efb:fc00:31ab:25d9:5d24:c8be) |
| 2021-04-26 15:56:10 | → | Sgeo joins (~Sgeo@ool-18b9875e.dyn.optonline.net) |
| 2021-04-26 15:56:41 | × | ddellac__ quits (~ddellacos@83.143.246.104) (Ping timeout: 240 seconds) |
| 2021-04-26 15:57:18 | × | Sgeo quits (~Sgeo@ool-18b9875e.dyn.optonline.net) (Read error: Connection reset by peer) |
| 2021-04-26 15:57:32 | → | guest7682358928 joins (c9dbe902@gateway/web/cgi-irc/kiwiirc.com/ip.201.219.233.2) |
| 2021-04-26 15:57:33 | × | rj quits (~x@gateway/tor-sasl/rj) (Ping timeout: 240 seconds) |
| 2021-04-26 15:58:19 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 252 seconds) |
| 2021-04-26 15:58:41 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 240 seconds) |
| 2021-04-26 15:58:48 | → | Sgeo joins (~Sgeo@ool-18b9875e.dyn.optonline.net) |
| 2021-04-26 15:59:44 | → | rj joins (~x@gateway/tor-sasl/rj) |
| 2021-04-26 15:59:53 | × | nicholasbulka quits (~nicholasb@2601:900:4301:da0:58e6:3a0a:96a:ca2c) (Remote host closed the connection) |
| 2021-04-26 16:02:37 | → | Pickchea joins (~private@unaffiliated/pickchea) |
| 2021-04-26 16:04:07 | × | Sgeo quits (~Sgeo@ool-18b9875e.dyn.optonline.net) (Read error: Connection reset by peer) |
| 2021-04-26 16:05:14 | → | nicholasbulka joins (~nicholasb@2601:900:4301:da0:58e6:3a0a:96a:ca2c) |
| 2021-04-26 16:06:16 | → | Sgeo joins (~Sgeo@ool-18b9875e.dyn.optonline.net) |
| 2021-04-26 16:09:45 | × | coot quits (~coot@37.30.50.130.nat.umts.dynamic.t-mobile.pl) (Quit: coot) |
| 2021-04-26 16:10:19 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Ping timeout: 260 seconds) |
| 2021-04-26 16:11:00 | × | gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving) |
| 2021-04-26 16:15:25 | → | alexander joins (~alexander@2a02:587:dc0a:2700:39fb:67a3:1f47:16d) |
| 2021-04-26 16:15:36 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 2021-04-26 16:15:54 | alexander | is now known as Guest44573 |
| 2021-04-26 16:16:02 | → | Deide joins (~Deide@217.155.19.23) |
| 2021-04-26 16:18:06 | × | v01d4lph4 quits (~v01d4lph4@27.57.103.213) (Remote host closed the connection) |
| 2021-04-26 16:18:35 | × | jgt quits (~jgt@78.162.43.217) (Ping timeout: 246 seconds) |
| 2021-04-26 16:23:47 | × | kuribas quits (~user@ptr-25vy0i9m572fxrivl24.18120a2.ip6.access.telenet.be) (Quit: ERC (IRC client for Emacs 26.3)) |
| 2021-04-26 16:29:10 | → | proofofkeags joins (~proofofke@205.209.28.54) |
| 2021-04-26 16:29:25 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-04-26 16:29:32 | → | ddellac__ joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-04-26 16:30:14 | <proofofkeags> | I'm having trouble building a docker container that is capable of emitting binaries for armv7 linux. I'm currently stuck on an issue where ghc-pkg can't lock a file and it fails with "Invalid Argument" |
| 2021-04-26 16:30:39 | → | esp32_prog joins (esp32_prog@gateway/vpn/mullvad/esp32prog/x-46565127) |
| 2021-04-26 16:31:05 | <proofofkeags> | what's interesting is that this issue does not appear natively on the raspberry pi when I use the pi to build stuff, but it does appear when I try to do the same thing inside the vm/container |
| 2021-04-26 16:32:31 | <maerwald> | proofofkeags: https://github.com/haskell/cabal/issues/6715#issuecomment-678370267 ? |
| 2021-04-26 16:32:47 | <proofofkeags> | yeah pretty much exactly that |
| 2021-04-26 16:32:54 | <proofofkeags> | though I don't see any solutions/workarounds |
| 2021-04-26 16:33:25 | <proofofkeags> | worth noting also that I need armv7 builds not armv8, but the symptom is identical |
| 2021-04-26 16:33:52 | × | ddellac__ quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 240 seconds) |
| 2021-04-26 16:34:06 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 2021-04-26 16:34:49 | → | vicfred joins (~vicfred@unaffiliated/vicfred) |
| 2021-04-26 16:36:54 | <maerwald> | also consider asking in #ghc |
| 2021-04-26 16:40:41 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-04-26 16:40:42 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 240 seconds) |
| 2021-04-26 16:41:26 | <Athas> | ski: 'generate' makes sense when you have a fairly general notion of the structure you're generating. E.g. in Haskell it is polymorphic over the shape vector. |
| 2021-04-26 16:44:49 | → | v01d4lph4 joins (~v01d4lph4@27.57.103.213) |
| 2021-04-26 16:44:50 | × | v01d4lph4 quits (~v01d4lph4@27.57.103.213) (Read error: Connection reset by peer) |
| 2021-04-26 16:45:24 | → | v01d4lph4 joins (~v01d4lph4@27.57.103.213) |
| 2021-04-26 16:45:50 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:71f6:aee0:3a4e:496c) () |
| 2021-04-26 16:47:41 | → | horatiohb joins (~horatiohb@159.65.170.201) |
| 2021-04-26 16:48:48 | <ski> | Athas : `generate' sounds to me like it could be one of many different ways to generate a structure, not necessarily generating each element independently from its coordinates/path |
| 2021-04-26 16:50:01 | × | v01d4lph4 quits (~v01d4lph4@27.57.103.213) (Ping timeout: 252 seconds) |
| 2021-04-26 16:50:46 | × | heatsink quits (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 2021-04-26 16:52:46 | × | s00pcan quits (~chris@107.181.165.217) (Ping timeout: 240 seconds) |
| 2021-04-26 16:52:53 | → | jgt joins (~jgt@78.162.43.217) |
| 2021-04-26 16:53:39 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 2021-04-26 16:55:02 | → | s00pcan joins (~chris@075-133-056-178.res.spectrum.com) |
| 2021-04-26 16:55:54 | → | P_B1 joins (~P_B@139.28.218.148) |
| 2021-04-26 16:56:02 | → | heatsink joins (~heatsink@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-04-26 16:56:10 | → | gnumonic joins (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) |
| 2021-04-26 16:59:22 | × | jgt quits (~jgt@78.162.43.217) (Ping timeout: 252 seconds) |
| 2021-04-26 16:59:57 | × | Gardy quits (51f4b066@102.176-244-81.adsl-dyn.isp.belgacom.be) (Quit: Connection closed) |
| 2021-04-26 17:00:01 | → | coot joins (~coot@37.30.50.130.nat.umts.dynamic.t-mobile.pl) |
| 2021-04-26 17:00:01 | → | frozenErebus joins (~frozenEre@37.231.244.249) |
| 2021-04-26 17:02:42 | → | ddellac__ joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-04-26 17:05:23 | × | frozenErebus quits (~frozenEre@37.231.244.249) (Ping timeout: 268 seconds) |
All times are in UTC.