Newest at the top
| 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`) |
| 2026-02-17 16:54:53 +0100 | <[exa]> | hadronized: anything specific? (this isn't a very good channel for a long writeup but perhaps people will point you in the right direction) |
| 2026-02-17 16:54:11 +0100 | <lambdabot> | Unknown command, try @list |
| 2026-02-17 16:54:11 +0100 | <[exa]> | @mad: underrated view |
| 2026-02-17 16:52:49 +0100 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 264 seconds) |
| 2026-02-17 16:48:51 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) machinedgod |
| 2026-02-17 16:37:17 +0100 | spew | (~spew@user/spew) (Quit: nyaa~) |
| 2026-02-17 16:33:33 +0100 | Googulator | (~Googulato@185.199.28.81) (Ping timeout: 272 seconds) |
| 2026-02-17 16:15:48 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2026-02-17 16:15:25 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2026-02-17 16:07:51 +0100 | fp | (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 252 seconds) |
| 2026-02-17 16:04:40 +0100 | spew | (~spew@user/spew) spew |
| 2026-02-17 16:02:53 +0100 | Arvin | (~Arvin@182.48.215.160) (Quit: Client closed) |
| 2026-02-17 15:38:35 +0100 | user363627 | (~user@user/user363627) (Remote host closed the connection) |
| 2026-02-17 15:32:58 +0100 | Arvin | (~Arvin@182.48.215.160) |
| 2026-02-17 15:32:22 +0100 | rekahsoft | (~rekahsoft@76.67.111.168) rekahsoft |
| 2026-02-17 15:18:51 +0100 | <hadronized> | I’m designing my own language and I’m struggling to understand a couple ideas regarding linear proof transformationsd with regards to container type |
| 2026-02-17 15:18:22 +0100 | <hadronized> | anyone has enough ATS knowledge and/or Linear Haskell? |
| 2026-02-17 15:07:56 +0100 | <kaol> | Since GHC 8.2, released in 2017. |
| 2026-02-17 15:04:54 +0100 | <haskellbridge> | <Morj> It says 4.10.0.0 on the hackage, but what year is that |