Newest at the top
| 2024-11-18 16:40:44 +0100 | <Wygulmage> | That's exactly what I wanted to know. |
| 2024-11-18 16:40:35 +0100 | <Wygulmage> | OK, thanks. |
| 2024-11-18 16:40:16 +0100 | Alleria_ | (~Alleria@user/alleria) Alleria |
| 2024-11-18 16:40:09 +0100 | <dolio> | If you're asking about a data definition with a specified kind of UnliftedType, then I'm less certain. I think the answer might still be no. |
| 2024-11-18 16:39:24 +0100 | <dolio> | Are you asking about ByteArray#? Then the answer is no, because it's not defined with data. It's a built-in. |
| 2024-11-18 16:38:24 +0100 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2024-11-18 16:37:35 +0100 | <Wygulmage> | Right. So UnliftedTypes are inside strict boxes (pointers) that allow the garbage collector to manage them. Does unpacking an unlifted type get rid of that box? |
| 2024-11-18 16:36:01 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2024-11-18 16:35:59 +0100 | <dolio> | You can only unpack data types. |
| 2024-11-18 16:35:31 +0100 | <Wygulmage> | (because GC can rewrite the pointer to actual memory inside the lifted structure that it's been unpacked into) |
| 2024-11-18 16:35:29 +0100 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 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. |