Newest at the top
| 2024-11-18 16:20:52 +0100 | <Wygulmage> | GC-managed reference to a memory region of metadata and bytes? Or is it a reference to ( an `Int#` and a reference to a GC managed...)? |
| 2024-11-18 16:20:51 +0100 | <Wygulmage> | So here's a semirelated question: Do UNPACK pragmas do anything to UnliftedTypes? For example, my understanding is that `ByteArray#` is a reference to a GC-managed reference to a memory region of metadata and bytes. If you try to UNPACK the `ByteArray` into a lifted constructor `Bar Int# !ByteArray#` , is the result a reference to an `Int#` and a |
| 2024-11-18 16:20:37 +0100 | housemate | (~housemate@2a04:9dc0:0:162::5d91:d7ed) housemate |
| 2024-11-18 16:15:38 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-11-18 16:15:08 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-11-18 16:11:25 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2024-11-18 16:08:23 +0100 | <Wygulmage> | Anyway, that works perfectly. |
| 2024-11-18 16:08:01 +0100 | <Wygulmage> | I'm pretty ignorant of view pattern syntax. I only use them when I need smart constructors in pattern synonyms. |
| 2024-11-18 16:08:00 +0100 | <dolio> | If you put it all in a function, then the function won't be returning the evidence unless you give it a more complicated return type. |
| 2024-11-18 16:07:35 +0100 | <dolio> | That way the Foo__ match gets you the evidence. |
| 2024-11-18 16:07:17 +0100 | <dolio> | It's just using a view pattern nested under a normal pattern. |
| 2024-11-18 16:06:59 +0100 | <Wygulmage> | dolio: Thank you! I did not know that was legal syntax! |
| 2024-11-18 16:05:41 +0100 | <dolio> | Maybe you want `Foo u <- Foo_ (unpack -> u)` |
| 2024-11-18 16:05:28 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-11-18 16:05:22 +0100 | <Wygulmage> | Does a view pattern like that not bring `Foo__` 's constraints into scope? Do I need to return something like `(# b, Refl #)` ? |
| 2024-11-18 16:04:56 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-11-18 16:03:33 +0100 | <Wygulmage> | Sorry, sorry, I had messed this up at the beginning. In desperation I had changed the pattern to `Foo b <- (\ (Foo_ i) -> unpack i -> b` |
| 2024-11-18 16:01:45 +0100 | <dolio> | The right type is something like `Foo a -> Witness (a ~ Bool) ...` |
| 2024-11-18 16:00:14 +0100 | <dolio> | You could, but that's not the right type. |
| 2024-11-18 15:59:58 +0100 | <Wygulmage> | Right. Can I give it a type like `Int# -> (a ~ Bool)=> a` ? |
| 2024-11-18 15:59:24 +0100 | <dolio> | Okay, so, it only returns a Bool, not evidence that `a ~ Int`. |
| 2024-11-18 15:59:09 +0100 | <Wygulmage> | `unpack :: Int# -> Bool` |
| 2024-11-18 15:58:49 +0100 | <dolio> | It does in unpack. But what is the type of unpack ? |
| 2024-11-18 15:57:51 +0100 | <Wygulmage> | I assumed that strictly matching the GADT constructor Foo__ in the view pattern would bring the constraint into scope. |
| 2024-11-18 15:57:12 +0100 | <Wygulmage> | (actually `Int# -> Bool`, if that matters.) |
| 2024-11-18 15:57:10 +0100 | <dolio> | Oh I see. Anyway, it doesn't matter. It just swaps around the problem. |
| 2024-11-18 15:56:39 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) (Ping timeout: 252 seconds) |
| 2024-11-18 15:55:56 +0100 | <dolio> | Right, but what type is `unpack`? |
| 2024-11-18 15:55:38 +0100 | <Wygulmage> | type of unpack is Int -> Bool |
| 2024-11-18 15:55:21 +0100 | <Wygulmage> | Sorry, so the GADT is `data Foo a where Foo__ :: Int -> Foo Bool |
| 2024-11-18 15:55:18 +0100 | lol_ | jcarpenter2 |
| 2024-11-18 15:54:12 +0100 | <dolio> | Like `data Witness c a where Wit :: c => a -> Witness c a` |
| 2024-11-18 15:53:14 +0100 | <dolio> | You need it to produce a type that is a Boolean with evidence that you're going to match on. |
| 2024-11-18 15:52:43 +0100 | <dolio> | Presumably the problem is that it just returns a boolean, which means that it doesn't actually get you the a ~ Int evidence that you say it has. |
| 2024-11-18 15:52:41 +0100 | Wygulmage | (~k`@user/Wygulmage) Wygulmage |
| 2024-11-18 15:52:41 +0100 | Wygulmage | (~k`@152.7.255.193) (Changing host) |
| 2024-11-18 15:50:16 +0100 | k` | Wygulmage |
| 2024-11-18 15:50:11 +0100 | <dolio> | What is the type of unpack? |
| 2024-11-18 15:49:41 +0100 | misterfish | (~misterfis@31-161-39-137.biz.kpn.net) misterfish |
| 2024-11-18 15:44:15 +0100 | <k`> | The GHC docs seem to imply that that's how the second set of constraints works, but I can't get the type to check. |
| 2024-11-18 15:43:58 +0100 | euleritian | (~euleritia@176.2.4.196) |
| 2024-11-18 15:43:32 +0100 | euleritian | (~euleritia@77.22.252.159) (Ping timeout: 252 seconds) |
| 2024-11-18 15:41:56 +0100 | <k`> | Is it possible to include GADT constraints in a pattern synonym? I'm trying to do something like `pattern ()=> (a ~ Int)=> Bool -> Foo a ; pattern Foo b <- (unpack -> b) where Foo x = Foo__ (pack x)`, and I get type error "Couldn't match type 'a' with 'Bool'". |
| 2024-11-18 15:39:49 +0100 | willscripted | (~willscrip@user/willscripted) willscripted |
| 2024-11-18 15:38:18 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-11-18 15:37:24 +0100 | k` | (~k`@152.7.255.193) |
| 2024-11-18 15:22:12 +0100 | alexherbo2 | (~alexherbo@2a02-8440-3113-e8b3-4dc5-4d20-737c-18a7.rev.sfr.net) alexherbo2 |
| 2024-11-18 15:11:21 +0100 | ystael | (~ystael@user/ystael) ystael |
| 2024-11-18 15:07:56 +0100 | euleritian | (~euleritia@77.22.252.159) |
| 2024-11-18 15:07:35 +0100 | euleritian | (~euleritia@ip4d16fc9f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |