Logs: freenode/#haskell
| 2020-11-18 12:00:09 | <dminuoso> | boxscape: https://hackage.haskell.org/package/constraints-0.12/docs/Data-Constraint.html#v:withDict |
| 2020-11-18 12:00:51 | <boxscape> | I'll take a look at that, thanks |
| 2020-11-18 12:02:32 | → | PacoV joins (~pcoves@16.194.31.93.rev.sfr.net) |
| 2020-11-18 12:02:35 | <PacoV> | Hi. |
| 2020-11-18 12:02:43 | <boxscape> | hi |
| 2020-11-18 12:02:45 | <dminuoso> | Mmm, promoted gadts... what are these constraints even? |
| 2020-11-18 12:02:54 | <dminuoso> | Does the kind system support constraints too? |
| 2020-11-18 12:03:13 | <boxscape> | dminuoso I don't really think so but it's where my path led me |
| 2020-11-18 12:03:32 | <dminuoso> | The diagnostic certainly reads strangely |
| 2020-11-18 12:04:15 | <dminuoso> | boxscape: Im curious, what are you trying to do here? What is that tyfam supposed to be used for? |
| 2020-11-18 12:05:03 | <PacoV> | I'm looking for someone who know the Hakyll library. I'd like to know if it's possible to use a url field to generate a route. I went to #hakyll but it's been dead for hours so I give here a shot. |
| 2020-11-18 12:05:05 | <nshepperd> | i don't think promoted GADTs are really a thing |
| 2020-11-18 12:05:36 | <boxscape> | dminuoso I'm trying to have an expression type that stores the free variables in that expression at the type level, in an ordered list. So if you combine two expressions, I take the union - and while trying to write that function I had to construct a new proof that one symbol is smaller than another |
| 2020-11-18 12:06:01 | <boxscape> | dminuoso though in retrospect maybe I wouldn't be able to construct a type-level value of that type to begin with |
| 2020-11-18 12:06:46 | <dminuoso> | % data Foo a where MkFoo Int -> Foo Int |
| 2020-11-18 12:06:46 | <yahb> | dminuoso: ; <interactive>:186:24: error: parse error on input `Int' |
| 2020-11-18 12:06:50 | <dminuoso> | % data Foo a where MkFoo :: Int -> Foo Int |
| 2020-11-18 12:06:50 | <yahb> | dminuoso: |
| 2020-11-18 12:07:18 | <nshepperd> | there's no type level equivalent of GADT case expressions so even if you could make that 'proof' it would be impossible to do anything useful with it |
| 2020-11-18 12:07:36 | <dminuoso> | % type family TyF (s :: *) :: Foo s |
| 2020-11-18 12:07:36 | <yahb> | dminuoso: |
| 2020-11-18 12:07:43 | <boxscape> | RIght, that makes sense, I thought that a case expression is basically needed here |
| 2020-11-18 12:07:45 | <merijn> | boxscape: RIP your sanity :p |
| 2020-11-18 12:08:09 | <dminuoso> | % type instance TyF Int = MkFoo 1 |
| 2020-11-18 12:08:10 | <yahb> | dminuoso: ; <interactive>:191:31: error:; * Expected kind `Int', but `1' has kind `GHC.Types.Nat'; * In the first argument of `MkFoo', namely `1'; In the type `MkFoo 1'; In the type instance declaration for `TyF' |
| 2020-11-18 12:08:11 | <dminuoso> | Mmm |
| 2020-11-18 12:08:18 | <dminuoso> | % data Foo a where MkFoo :: Foo Int |
| 2020-11-18 12:08:18 | <yahb> | dminuoso: |
| 2020-11-18 12:08:23 | <dminuoso> | % type family TyF (s :: *) :: Foo s |
| 2020-11-18 12:08:23 | <yahb> | dminuoso: |
| 2020-11-18 12:08:26 | <dminuoso> | % type instance TyF Int = MkFoo |
| 2020-11-18 12:08:26 | <yahb> | dminuoso: |
| 2020-11-18 12:08:33 | <boxscape> | merijn mind you, I would never use haskell type level machinery I'm not allowed to just give up on at the moment :) |
| 2020-11-18 12:08:47 | <boxscape> | for anything I'm not allowed * |
| 2020-11-18 12:08:50 | <dminuoso> | nshepperd: At least its liftable... |
| 2020-11-18 12:09:30 | <boxscape> | dminuoso is that even a GADS under the hood? |
| 2020-11-18 12:09:36 | <boxscape> | GADT, rather |
| 2020-11-18 12:09:45 | <boxscape> | or wait |
| 2020-11-18 12:09:48 | <boxscape> | yes it is |
| 2020-11-18 12:11:13 | <boxscape> | Hmmm maybe I could do it if I were to make my own type-level String type |
| 2020-11-18 12:13:06 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Remote host closed the connection) |
| 2020-11-18 12:13:21 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 2020-11-18 12:13:37 | × | johnw quits (~johnw@haskell/developer/johnw) (Ping timeout: 260 seconds) |
| 2020-11-18 12:15:38 | → | johnw joins (~johnw@haskell/developer/johnw) |
| 2020-11-18 12:16:50 | → | Tario joins (~Tario@201.192.165.173) |
| 2020-11-18 12:17:34 | → | da39a3ee5e6b4b0d joins (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) |
| 2020-11-18 12:19:49 | → | Stanley00 joins (~stanley00@unaffiliated/stanley00) |
| 2020-11-18 12:26:42 | → | omega8cc joins (~omega8cc@185.204.1.185) |
| 2020-11-18 12:27:40 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Ping timeout: 246 seconds) |
| 2020-11-18 12:28:17 | → | bliminse joins (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) |
| 2020-11-18 12:28:28 | <boxscape> | Is there an UnsafeCoerce for the type level? |
| 2020-11-18 12:28:39 | → | Entertainment joins (~entertain@104.246.132.210) |
| 2020-11-18 12:28:47 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Quit: My Laptop has gone to sleep. ZZZzzz…) |
| 2020-11-18 12:29:02 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 2020-11-18 12:29:07 | → | todda7 joins (~torstein@2a02:587:d96:adb6:c7fc:9428:5ead:614f) |
| 2020-11-18 12:29:17 | × | bliminse quits (~bliminse@host109-156-197-211.range109-156.btcentralplus.com) (Client Quit) |
| 2020-11-18 12:29:56 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 240 seconds) |
| 2020-11-18 12:36:42 | × | Tario quits (~Tario@201.192.165.173) (Read error: Connection reset by peer) |
| 2020-11-18 12:41:31 | × | britva quits (~britva@31-10-157-156.cgn.dynamic.upc.ch) (Quit: This computer has gone to sleep) |
| 2020-11-18 12:42:34 | → | vacm joins (~vacwm@70.23.92.191) |
| 2020-11-18 12:44:02 | tomsmeding | shudders |
| 2020-11-18 12:45:37 | → | alp joins (~alp@2a01:e0a:58b:4920:c9d2:961b:b0f5:7405) |
| 2020-11-18 12:46:07 | → | jakob_ joins (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) |
| 2020-11-18 12:46:15 | × | vacm quits (~vacwm@70.23.92.191) (Client Quit) |
| 2020-11-18 12:46:59 | × | Stanley00 quits (~stanley00@unaffiliated/stanley00) () |
| 2020-11-18 12:48:51 | → | Tario joins (~Tario@201.192.165.173) |
| 2020-11-18 12:49:23 | × | jakob_ quits (~textual@dynamic-093-135-025-031.93.135.pool.telefonica.de) (Client Quit) |
| 2020-11-18 12:49:47 | → | texasmynsted joins (~texasmyns@212.102.45.121) |
| 2020-11-18 12:51:27 | → | invaser joins (~Thunderbi@31.148.23.125) |
| 2020-11-18 12:54:39 | × | DavidEichmann quits (~david@62.110.198.146.dyn.plus.net) (Remote host closed the connection) |
| 2020-11-18 12:55:40 | → | DavidEichmann joins (~david@62.110.198.146.dyn.plus.net) |
| 2020-11-18 12:55:56 | × | servo quits (~servo@41.92.32.131) (Remote host closed the connection) |
| 2020-11-18 12:55:57 | <ziman> | is there an (probably associated) type family that would give me the inner type of a newtype? |
| 2020-11-18 12:57:57 | <ziman> | `Coercible` helps me only when I know the inner type already |
| 2020-11-18 12:59:07 | <idnar> | which crc32 lib do I want? |
| 2020-11-18 13:00:30 | <idnar> | ziman: https://hackage.haskell.org/package/lens-4.19.2/docs/Control-Lens-Wrapped.html#t:Unwrapped |
| 2020-11-18 13:00:58 | <ziman> | oh, right, generics, thanks! |
| 2020-11-18 13:01:17 | <dminuoso> | 13:28:28 boxscape | Is there an UnsafeCoerce for the type level? |
| 2020-11-18 13:01:34 | <dminuoso> | You want what? |
| 2020-11-18 13:02:05 | <boxscape> | I'm about 5% certain that it could help me out :) |
| 2020-11-18 13:02:27 | × | da39a3ee5e6b4b0d quits (~da39a3ee5@cm-171-98-78-149.revip7.asianet.co.th) (Ping timeout: 256 seconds) |
| 2020-11-18 13:02:28 | Uniaika | cocks her musket |
| 2020-11-18 13:03:26 | <hc> | idnar: depends on what you're trying to do |
| 2020-11-18 13:04:13 | × | sis7_ quits (~user@2001:15e8:110:473e::1) (Quit: sis7_) |
| 2020-11-18 13:04:30 | hackage | haskoin-store 0.38.3 - Storage and index for Bitcoin and Bitcoin Cash https://hackage.haskell.org/package/haskoin-store-0.38.3 (jprupp) |
| 2020-11-18 13:05:33 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 2020-11-18 13:06:58 | <hc> | idnar: the zip library seems to be using the digest package ( https://hackage.haskell.org/package/digest ) |
| 2020-11-18 13:07:30 | <idnar> | hc: I'm implementing this madness: https://docs.kraken.com/websockets/#book-checksum |
| 2020-11-18 13:08:12 | <hc> | ah okay, so you specifically need CRC32. Then I'd say what works for the best zip library available for haskell (afaict) might work for you as well :) |
| 2020-11-18 13:08:18 | × | danvet_ quits (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) (Quit: Leaving) |
| 2020-11-18 13:10:00 | <dminuoso> | Wait.. CRC32 is used as a poor mans MAC_ |
| 2020-11-18 13:10:11 | <dminuoso> | That's gross. |
| 2020-11-18 13:10:57 | × | britva quits (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) (Quit: This computer has gone to sleep) |
| 2020-11-18 13:11:56 | <idnar> | dminuoso: it's more of an actual checksum |
| 2020-11-18 13:13:10 | <hc> | dminuoso: "TLS with SNI (Server Name Indication) is required in order to establish a Kraken WebSockets API connection." |
| 2020-11-18 13:13:17 | → | britva joins (~britva@2a02:aa13:7240:2980:7da5:a1a0:c038:90b4) |
| 2020-11-18 13:13:28 | <hc> | I'd say one layer of transport security should be enough (though, arguably, tls might not be the best choice;=) |
| 2020-11-18 13:14:22 | <dminuoso> | Im honestly a bit unsure what the CRC32 even helps with. |
| 2020-11-18 13:14:30 | <hc> | nothing, afaict ;p |
| 2020-11-18 13:15:01 | hackage | subG 0.4.0.0 - Some extension to the Foldable and Monoid classes. https://hackage.haskell.org/package/subG-0.4.0.0 (OleksandrZhabenko) |
All times are in UTC.