Logs: liberachat/#haskell
| 2021-06-23 17:53:00 | <safinaskar> | ski: i think i will able to somehow extract "n" from this "exists n. NatIs n" and pass it somewhere |
| 2021-06-23 17:57:17 | <ski> | consider something like `zipWith :: forall a b c n. (a -> b -> c) -> (Vec a n -> Vec b n -> Vec c n)'. the point of using the `n' index here is to mention it multiple times in the type, linking the lengths of the three vectors together. if you instead go `zipWith :: forall a b c. (a -> b -> c) -> ((exists n. Vec a n) -> (exists n. Vec b n) -> (exists n. Vec c n))', you can do that, but that's not really any |
| 2021-06-23 17:57:23 | <ski> | better than `zipWith :: forall a b c. (a -> b -> c) -> ([a] -> [b] -> [c])' in the first place |
| 2021-06-23 17:58:35 | → | mikail__ joins (~mikail@2a02:c7f:bc9c:3100:ae93:93fc:603f:ceaf) |
| 2021-06-23 17:58:46 | <ski> | similarly, someList :: [exists n. NatIs n]' isn't really any better than `someList :: [Nat]'. if you ever want to perform such a conversion, you can always use a function `toSingNat :: Nat -> exists n. NatIs n' |
| 2021-06-23 17:59:51 | × | arjun_ quits (~arjun@160.202.37.101) (Ping timeout: 265 seconds) |
| 2021-06-23 18:00:06 | <jumper149> | I am currently trying to fix my usage of MonadBaseControl, because I was missing some `restoreM`s. So instead I came up with this: https://github.com/jumper149/blucontrol/blob/fix-control/src/Blucontrol/Main/Control.hs#L54 |
| 2021-06-23 18:00:58 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 2021-06-23 18:01:02 | <jumper149> | The problem is, that I need to call `unsafeCoerce` right here. But when HLS tells me the type of `unsafeCoerce` is just like `id` here. |
| 2021-06-23 18:01:11 | <safinaskar> | ski: i will show example |
| 2021-06-23 18:01:17 | <jumper149> | When trying to run the program everything works fine. |
| 2021-06-23 18:01:28 | ski | will have to leave rather soon |
| 2021-06-23 18:01:38 | <jumper149> | So why can't GHC just infer type equality here. I guess it has to do with type families somehow. |
| 2021-06-23 18:02:43 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-23 18:03:02 | <jumper149> | This is the error without `unsafeCoerce`: http://ix.io/3qU1 |
| 2021-06-23 18:03:53 | → | warnz joins (~warnz@2600:1700:77c0:5610:799f:ce24:eb20:cceb) |
| 2021-06-23 18:07:03 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 2021-06-23 18:08:04 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 2021-06-23 18:09:15 | × | fef quits (~thedawn@user/thedawn) (Ping timeout: 244 seconds) |
| 2021-06-23 18:09:20 | <safinaskar> | ski: here is example: https://paste.debian.net/1202170/ |
| 2021-06-23 18:09:50 | <safinaskar> | ski: as you can see, i was able to actually use existential "Foo". and as you can see, Foo is better than just Nat |
| 2021-06-23 18:09:54 | × | xkuru quits (~xkuru@user/xkuru) (Ping timeout: 252 seconds) |
| 2021-06-23 18:10:30 | <safinaskar> | ski: i was able to pattern match on Foo value and then (if it greater than zero) pass it as second argument to division |
| 2021-06-23 18:10:54 | <safinaskar> | thus, compiler proved that at calling point of "divide" its second argument is not zero |
| 2021-06-23 18:11:22 | <safinaskar> | this way we can finally remove partial functions, such as division, "head", etc |
| 2021-06-23 18:14:06 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-23 18:15:17 | × | chisui quits (~chisui@200116b866efc30078bec775310a636c.dip.versatel-1u1.de) (Quit: Client closed) |
| 2021-06-23 18:16:10 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 258 seconds) |
| 2021-06-23 18:17:33 | × | mikail__ quits (~mikail@2a02:c7f:bc9c:3100:ae93:93fc:603f:ceaf) (Quit: Leaving) |
| 2021-06-23 18:22:04 | → | involans joins (~alex@cpc92718-cmbg20-2-0-cust157.5-4.cable.virginm.net) |
| 2021-06-23 18:25:53 | ← | tusko parts (~yeurt@user/tusko) (Farewell) |
| 2021-06-23 18:26:07 | → | chisui joins (~chisui@200116b866efc300e1478aa720ae1876.dip.versatel-1u1.de) |
| 2021-06-23 18:27:07 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-23 18:27:46 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Quit: Leaving.) |
| 2021-06-23 18:31:09 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-23 18:32:30 | → | safinaskar97 joins (~safinaska@109.252.90.89) |
| 2021-06-23 18:35:10 | → | econo joins (uid147250@user/econo) |
| 2021-06-23 18:35:43 | × | safinaskar quits (~safinaska@109-252-90-89.nat.spd-mgts.ru) (Ping timeout: 246 seconds) |
| 2021-06-23 18:38:01 | × | yoctocell quits (~user@h87-96-130-155.cust.a3fiber.se) (Quit: ERC (IRC client for Emacs 28.0.50)) |
| 2021-06-23 18:40:19 | × | xsperry quits (~as@user/xsperry) (Ping timeout: 258 seconds) |
| 2021-06-23 18:42:20 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-06-23 18:43:30 | × | mcglk quits (~mcglk@131.191.49.120) (Quit: (seeya)) |
| 2021-06-23 18:43:54 | → | mcglk joins (~mcglk@131.191.49.120) |
| 2021-06-23 18:44:19 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 2021-06-23 18:45:53 | × | johnw quits (~johnw@2607:f6f0:3004:1:c8b4:50ff:fef8:6bf0) (Read error: Connection reset by peer) |
| 2021-06-23 18:46:27 | × | Morrow quits (~Morrow@bzq-110-168-31-106.red.bezeqint.net) (Ping timeout: 258 seconds) |
| 2021-06-23 18:47:18 | → | johnw joins (~johnw@2607:f6f0:3004:1:c8b4:50ff:fef8:6bf0) |
| 2021-06-23 18:48:48 | → | fef joins (~thedawn@user/thedawn) |
| 2021-06-23 18:52:26 | × | jespada quits (~jespada@90.254.247.46) (Ping timeout: 252 seconds) |
| 2021-06-23 18:53:35 | → | allbery_b joins (~geekosaur@xmonad/geekosaur) |
| 2021-06-23 18:53:35 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Killed (NickServ (GHOST command used by allbery_b))) |
| 2021-06-23 18:54:38 | × | dunkeln quits (~dunkeln@188.71.193.140) (Ping timeout: 252 seconds) |
| 2021-06-23 18:55:31 | × | fef quits (~thedawn@user/thedawn) (Quit: Leaving) |
| 2021-06-23 18:55:31 | → | jespada joins (~jespada@90.254.247.46) |
| 2021-06-23 19:00:25 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-06-23 19:01:44 | allbery_b | is now known as geekosaur |
| 2021-06-23 19:04:18 | → | fresheyeball joins (~fresheyeb@c-71-237-105-37.hsd1.co.comcast.net) |
| 2021-06-23 19:04:50 | × | tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2021-06-23 19:04:51 | → | dunkeln_ joins (~dunkeln@188.71.193.140) |
| 2021-06-23 19:05:14 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 250 seconds) |
| 2021-06-23 19:05:35 | × | turlando quits (~turlando@user/turlando) (Ping timeout: 265 seconds) |
| 2021-06-23 19:06:37 | → | myShoggoth joins (~myShoggot@75.164.29.44) |
| 2021-06-23 19:07:05 | ← | safinaskar97 parts (~safinaska@109.252.90.89) () |
| 2021-06-23 19:08:49 | → | turlando joins (~turlando@93-42-250-112.ip89.fastwebnet.it) |
| 2021-06-23 19:08:49 | × | turlando quits (~turlando@93-42-250-112.ip89.fastwebnet.it) (Changing host) |
| 2021-06-23 19:08:49 | → | turlando joins (~turlando@user/turlando) |
| 2021-06-23 19:11:44 | × | ubert quits (~Thunderbi@p200300ecdf259deac0d59fca0b69df22.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
| 2021-06-23 19:12:03 | → | ubert joins (~Thunderbi@p200300ecdf259dc2c0d59fca0b69df22.dip0.t-ipconnect.de) |
| 2021-06-23 19:18:40 | × | ubert quits (~Thunderbi@p200300ecdf259dc2c0d59fca0b69df22.dip0.t-ipconnect.de) (Ping timeout: 250 seconds) |
| 2021-06-23 19:22:58 | → | Deide joins (~Deide@wire.desu.ga) |
| 2021-06-23 19:22:58 | × | Deide quits (~Deide@wire.desu.ga) (Changing host) |
| 2021-06-23 19:22:58 | → | Deide joins (~Deide@user/deide) |
| 2021-06-23 19:25:27 | × | turlando quits (~turlando@user/turlando) (Read error: Connection reset by peer) |
| 2021-06-23 19:27:05 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 2021-06-23 19:28:14 | → | Guest9 joins (~Guest9@43.241.144.49) |
| 2021-06-23 19:32:02 | <Guest9> | i like a book called pragmatic programmer , which books do you like/recommend? |
| 2021-06-23 19:32:05 | <Guest9> | in general/specific |
| 2021-06-23 19:32:34 | → | tromp joins (~textual@dhcp-077-249-230-040.chello.nl) |
| 2021-06-23 19:34:06 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-06-23 19:37:34 | <opv> | Hi all. I am trying to build elm bc I need it on aarch64, and am failing miserably. I am very confused. Is this the right place to ask about cabal? |
| 2021-06-23 19:38:54 | → | peterhil_ joins (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) |
| 2021-06-23 19:39:44 | × | peterhil quits (~peterhil@dsl-hkibng32-54f849-252.dhcp.inet.fi) (Ping timeout: 258 seconds) |
| 2021-06-23 19:43:11 | → | tzar_bomba joins (~tzar_bomb@78-56-41-78.static.zebra.lt) |
| 2021-06-23 19:45:56 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-06-23 19:46:24 | <monochrom> | Yes. |
| 2021-06-23 19:47:05 | → | amahl joins (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) |
| 2021-06-23 19:54:52 | <maerwald> | Great question. |
| 2021-06-23 19:55:11 | → | turlando joins (~turlando@user/turlando) |
| 2021-06-23 19:56:43 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-06-23 19:59:08 | × | Guest9 quits (~Guest9@43.241.144.49) (Quit: Connection closed) |
| 2021-06-23 20:00:08 | → | hseg joins (~gesh@195.192.229.14) |
| 2021-06-23 20:01:08 | × | dunkeln_ quits (~dunkeln@188.71.193.140) (Ping timeout: 250 seconds) |
| 2021-06-23 20:01:46 | <dminuoso> | davean: Okay, so in hindsight, I was aware doJailbreak did exist. I did some research, it's possible you're perhaps thinking of a relatively recent idea to automatically jailbreak on hackage2nix, but from everything I gather not unconditionally, only if it leads to buildable plans. But it is indeed a very sorrow thing if nix breaks cabal bound induced boundaries. |
| 2021-06-23 20:02:13 | <davean> | Its not recent, this happened to me in 2016 |
| 2021-06-23 20:02:30 | <dminuoso> | Yeah, and I can already see how this on directory can cause really issues |
| 2021-06-23 20:02:39 | <dminuoso> | Even when its a transitive dependency |
| 2021-06-23 20:02:45 | <dminuoso> | This starts breaking other packages promises as well |
| 2021-06-23 20:02:49 | <davean> | Yep |
| 2021-06-23 20:02:55 | <davean> | It was a pretty deep big problem |
| 2021-06-23 20:03:03 | × | wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
All times are in UTC.