Newest at the top
| 2024-11-18 16:34:56 +0100 | <Wygulmage> | Right. I think we're talking past each other. My understanding is that a ByteArray# is a pointer to another pointer to flat memory that consists of length in bytes and then the bytes. I'm wondering whether unpacking the ByteArray# lifts gets rid of that first pointer, |
| 2024-11-18 16:33:38 +0100 | <dolio> | I don't know exactly how it's represented, though. I guess the structure could be all packed together instead of involving another pointer. |
| 2024-11-18 16:32:26 +0100 | <dolio> | It's a structure. |
| 2024-11-18 16:32:08 +0100 | <dolio> | It's not just a pointer to the beginning of the bytes, because byte arrays e.g. know their length. |
| 2024-11-18 16:30:34 +0100 | <Wygulmage> | The byte array structure as in the actual memory region, or another pointer (to GC-managed memory if unpinned and pinned memory if pinned) to the actual allocated memory? |
| 2024-11-18 16:28:40 +0100 | <dolio> | Basically, Bar contains two words (I think), one of which is the Int# and one which is the pointer to the byte array structure. |
| 2024-11-18 16:28:22 +0100 | <Wygulmage> | For what it's worth, GHC does not complain about an UNPACK pragma on a ByteArray#. And I assume that if I define my own unlifted types, I can unpack them (because they are still boxed). |
| 2024-11-18 16:25:49 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-11-18 16:25:19 +0100 | <dolio> | In a manner of speaking. |
| 2024-11-18 16:25:19 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-11-18 16:24:50 +0100 | <dolio> | So the ByteArray# will still be an indirection. |
| 2024-11-18 16:24:27 +0100 | <dolio> | I'm not sure what you're asking. You can't unpack the ByteArray# stuff directly into the constructor of another type (to my knowledge) if that's what you mean. |
| 2024-11-18 16:24:24 +0100 | <Wygulmage> | Is there a way to check by looking at the dumped .simpl file for the module? |
| 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 |