Newest at the top
| 2026-02-17 18:21:42 +0100 | oneeyedalien | (~oneeyedal@user/oneeyedalien) (Quit: Leaving) |
| 2026-02-17 18:20:44 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2026-02-17 18:19:00 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-02-17 18:14:15 +0100 | oneeyedalien | (~oneeyedal@user/oneeyedalien) oneeyedalien |
| 2026-02-17 18:13:36 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-02-17 18:08:57 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-02-17 18:05:48 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 2026-02-17 18:04:39 +0100 | wickedja` | (~user@24.83.46.194) |
| 2026-02-17 18:04:13 +0100 | wickedja` | (~user@24.83.46.194) (Ping timeout: 264 seconds) |
| 2026-02-17 18:03:00 +0100 | wickedjargon | (~user@24.83.46.194) wickedjargon |
| 2026-02-17 17:58:00 +0100 | Enrico63 | (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) (Client Quit) |
| 2026-02-17 17:57:05 +0100 | Enrico63 | (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) Enrico63 |
| 2026-02-17 17:49:34 +0100 | skinkitten | (~skinkitte@user/skinkitten) skinkitten |
| 2026-02-17 17:48:39 +0100 | wickedjargon | (~user@24.83.46.194) (Ping timeout: 244 seconds) |
| 2026-02-17 17:47:12 +0100 | wickedja` | (~user@24.83.46.194) |
| 2026-02-17 17:40:41 +0100 | Enrico63 | (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) (Ping timeout: 272 seconds) |
| 2026-02-17 17:39:33 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-02-17 17:35:42 +0100 | mxs9 | (~mxs@user/mxs) (Client Quit) |
| 2026-02-17 17:35:42 +0100 | mxs9 | (~mxs@user/mxs) mxs |
| 2026-02-17 17:34:58 +0100 | foul_owl | (~kerry@94.156.149.94) foul_owl |
| 2026-02-17 17:25:12 +0100 | jmcantrell_ | jmcantrell |
| 2026-02-17 17:23:01 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-02-17 17:21:01 +0100 | foul_owl | (~kerry@94.156.149.92) (Ping timeout: 264 seconds) |
| 2026-02-17 17:20:57 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-02-17 17:20:45 +0100 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 244 seconds) |
| 2026-02-17 17:17:58 +0100 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2026-02-17 17:17:09 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-02-17 17:17:07 +0100 | wickedjargon | (~user@24.83.46.194) wickedjargon |
| 2026-02-17 17:16:29 +0100 | prdak | (~Thunderbi@user/prdak) prdak |
| 2026-02-17 17:15:23 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2026-02-17 17:07:30 +0100 | <tomsmeding> | is that `|` a sum type? |
| 2026-02-17 17:06:25 +0100 | tomsmeding | . o O ( agda syntax: ∃[ l ∈ addr ] (ptr i32 × @0 l), or something ) |
| 2026-02-17 17:06:05 +0100 | <hadronized> | so yes, it tells that we have a pointer indexed by l: addr, and the alloc(i32, l) means that we have the proof that there is an allocation of type i32 at that existential l address |
| 2026-02-17 17:05:13 +0100 | <hadronized> | you can imagine that as a tuple where the right side never appears at runtime |
| 2026-02-17 17:05:02 +0100 | <hadronized> | it’s a way to state that the proof is only at the static level |
| 2026-02-17 17:04:47 +0100 | tomsmeding | has no clue about ATS |
| 2026-02-17 17:04:35 +0100 | <hadronized> | the juxtaposition is the same as ATS |
| 2026-02-17 17:04:29 +0100 | <hadronized> | it does tomsmeding |
| 2026-02-17 17:04:21 +0100 | <hadronized> | so I guess I would instead need to store the items as dynarr(ptr(i32)), and unsafely generate the deref proofs |
| 2026-02-17 17:04:10 +0100 | <tomsmeding> | it's unclear to me what `{l: addr} ptr(i32) l` means; presumably `∃(l : addr).`, but what's the juxtaposition? |
| 2026-02-17 17:03:50 +0100 | <hadronized> | instance* |
| 2026-02-17 17:03:48 +0100 | <hadronized> | if I store that in a dynamic array, I get dynarr({l: addr} ptr(i32) l | alloc(i32, l)), which by definition, only allows to know that the existential pair can be used, but you cannot for instance transformed an alloc linear proof into a deref proof by doing a get(3) -> option(ptr(i32) | deref) for instacne |
| 2026-02-17 17:02:49 +0100 | <hadronized> | with {l: addr} ptr(i32) l | alloc(i32, l) |
| 2026-02-17 17:02:36 +0100 | <tomsmeding> | hadronized: if more long-form, you could ask here https://langdev.stackexchange.com/ |
| 2026-02-17 17:02:36 +0100 | <hadronized> | instance |
| 2026-02-17 17:02:34 +0100 | <hadronized> | my question is basically about how proofs work when moving items in containers; for instance, consider a dynamic array (dynarr) type which takes pointers to stuff, like ptr(i32); my language supports existentials, so {l: addr} ptr(i32) l are pointers pointing to some l address, we just do not which; I use that syntax to introduce allocation proofs, to prove a pointer comes from a malloc for |
| 2026-02-17 17:01:55 +0100 | <tomsmeding> | there are some people here familiar with Linear Haskell (such as me, kindof), but I don't think you'll find much ATS here |
| 2026-02-17 17:01:18 +0100 | <hadronized> | I asked on proglangdesign, to no avail [exa] |
| 2026-02-17 17:00:38 +0100 | <tomsmeding> | also https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history |
| 2026-02-17 17:00:26 +0100 | <tomsmeding> | Morj: base versions are listed in `ghcup list -t ghc` (or `ghcup tui`) |