Logs: liberachat/#haskell
| 2026-02-17 13:02:16 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2026-02-17 13:02:50 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 2026-02-17 13:09:02 | → | haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 2026-02-17 13:09:02 | × | haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 2026-02-17 13:09:02 | → | haritz joins (~hrtz@user/haritz) |
| 2026-02-17 13:24:05 | → | petrichor joins (~jez@user/petrichor) |
| 2026-02-17 13:25:28 | → | lol_ joins (~lol@2603:3016:1e01:b940:9441:c46b:69b3:7076) |
| 2026-02-17 13:29:12 | × | lol__ quits (~lol@2603:3016:1e01:b940:9441:c46b:69b3:7076) (Ping timeout: 264 seconds) |
| 2026-02-17 13:40:43 | → | Googulator joins (~Googulato@185.199.28.81) |
| 2026-02-17 13:44:02 | → | bwe joins (~bwe@2a01:4f8:1c1c:4878::2) |
| 2026-02-17 13:51:01 | → | Enrico63 joins (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) |
| 2026-02-17 13:53:38 | → | emaczen joins (~user@user/emaczen) |
| 2026-02-17 13:59:26 | <kaol> | I came up with a fun function: bitraverse <*> traverse. For manipulating that bothersome Either a (b,a). |
| 2026-02-17 14:04:54 | <haskellbridge> | <Morj> Since when is Bitraversable in base |
| 2026-02-17 14:04:54 | <haskellbridge> | <Morj> It says 4.10.0.0 on the hackage, but what year is that |
| 2026-02-17 14:07:56 | <kaol> | Since GHC 8.2, released in 2017. |
| 2026-02-17 14:18:22 | <hadronized> | anyone has enough ATS knowledge and/or Linear Haskell? |
| 2026-02-17 14:18:51 | <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 14:32:22 | → | rekahsoft joins (~rekahsoft@76.67.111.168) |
| 2026-02-17 14:32:58 | → | Arvin joins (~Arvin@182.48.215.160) |
| 2026-02-17 14:38:35 | × | user363627 quits (~user@user/user363627) (Remote host closed the connection) |
| 2026-02-17 15:02:53 | × | Arvin quits (~Arvin@182.48.215.160) (Quit: Client closed) |
| 2026-02-17 15:04:40 | → | spew joins (~spew@user/spew) |
| 2026-02-17 15:07:51 | × | fp quits (~Thunderbi@2001:708:20:1406::1370) (Ping timeout: 252 seconds) |
| 2026-02-17 15:15:25 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2026-02-17 15:15:48 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 2026-02-17 15:33:33 | × | Googulator quits (~Googulato@185.199.28.81) (Ping timeout: 272 seconds) |
| 2026-02-17 15:37:17 | × | spew quits (~spew@user/spew) (Quit: nyaa~) |
| 2026-02-17 15:48:51 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 2026-02-17 15:52:49 | × | prdak quits (~Thunderbi@user/prdak) (Ping timeout: 264 seconds) |
| 2026-02-17 15:54:11 | <[exa]> | @mad: underrated view |
| 2026-02-17 15:54:11 | <lambdabot> | Unknown command, try @list |
| 2026-02-17 15:54:53 | <[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:00:26 | <tomsmeding> | Morj: base versions are listed in `ghcup list -t ghc` (or `ghcup tui`) |
| 2026-02-17 16:00:38 | <tomsmeding> | also https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/libraries/version-history |
| 2026-02-17 16:01:18 | <hadronized> | I asked on proglangdesign, to no avail [exa] |
| 2026-02-17 16:01:55 | <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 16:02:34 | <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 16:02:36 | <hadronized> | instance |
| 2026-02-17 16:02:36 | <tomsmeding> | hadronized: if more long-form, you could ask here https://langdev.stackexchange.com/ |
| 2026-02-17 16:02:49 | <hadronized> | with {l: addr} ptr(i32) l | alloc(i32, l) |
| 2026-02-17 16:03:48 | <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 16:03:50 | <hadronized> | instance* |
| 2026-02-17 16:04:10 | <tomsmeding> | it's unclear to me what `{l: addr} ptr(i32) l` means; presumably `∃(l : addr).`, but what's the juxtaposition? |
| 2026-02-17 16:04:21 | <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 16:04:29 | <hadronized> | it does tomsmeding |
| 2026-02-17 16:04:35 | <hadronized> | the juxtaposition is the same as ATS |
| 2026-02-17 16:04:47 | tomsmeding | has no clue about ATS |
| 2026-02-17 16:05:02 | <hadronized> | it’s a way to state that the proof is only at the static level |
| 2026-02-17 16:05:13 | <hadronized> | you can imagine that as a tuple where the right side never appears at runtime |
| 2026-02-17 16:06:05 | <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 16:06:25 | tomsmeding | . o O ( agda syntax: ∃[ l ∈ addr ] (ptr i32 × @0 l), or something ) |
| 2026-02-17 16:07:30 | <tomsmeding> | is that `|` a sum type? |
| 2026-02-17 16:15:23 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2026-02-17 16:16:29 | → | prdak joins (~Thunderbi@user/prdak) |
| 2026-02-17 16:17:07 | → | wickedjargon joins (~user@24.83.46.194) |
| 2026-02-17 16:17:09 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-02-17 16:17:58 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2026-02-17 16:20:45 | × | prdak quits (~Thunderbi@user/prdak) (Ping timeout: 244 seconds) |
| 2026-02-17 16:20:57 | → | merijn joins (~merijn@77.242.116.146) |
| 2026-02-17 16:21:01 | × | foul_owl quits (~kerry@94.156.149.92) (Ping timeout: 264 seconds) |
| 2026-02-17 16:23:01 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-02-17 16:25:12 | jmcantrell_ | is now known as jmcantrell |
| 2026-02-17 16:34:58 | → | foul_owl joins (~kerry@94.156.149.94) |
| 2026-02-17 16:35:42 | → | mxs9 joins (~mxs@user/mxs) |
| 2026-02-17 16:35:42 | × | mxs9 quits (~mxs@user/mxs) (Client Quit) |
| 2026-02-17 16:39:33 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 2026-02-17 16:40:41 | × | Enrico63 quits (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) (Ping timeout: 272 seconds) |
| 2026-02-17 16:47:12 | → | wickedja` joins (~user@24.83.46.194) |
| 2026-02-17 16:48:39 | × | wickedjargon quits (~user@24.83.46.194) (Ping timeout: 244 seconds) |
| 2026-02-17 16:49:34 | → | skinkitten joins (~skinkitte@user/skinkitten) |
| 2026-02-17 16:57:05 | → | Enrico63 joins (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) |
| 2026-02-17 16:58:00 | × | Enrico63 quits (~Enrico63@host-79-56-90-180.retail.telecomitalia.it) (Client Quit) |
| 2026-02-17 17:03:00 | → | wickedjargon joins (~user@24.83.46.194) |
| 2026-02-17 17:04:13 | × | wickedja` quits (~user@24.83.46.194) (Ping timeout: 264 seconds) |
| 2026-02-17 17:04:39 | → | wickedja` joins (~user@24.83.46.194) |
| 2026-02-17 17:05:48 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 2026-02-17 17:08:57 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-02-17 17:13:36 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-02-17 17:14:15 | → | oneeyedalien joins (~oneeyedal@user/oneeyedalien) |
| 2026-02-17 17:19:00 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-02-17 17:20:44 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2026-02-17 17:21:42 | × | oneeyedalien quits (~oneeyedal@user/oneeyedalien) (Quit: Leaving) |
| 2026-02-17 17:23:33 | × | skinkitten quits (~skinkitte@user/skinkitten) (Quit: Client closed) |
| 2026-02-17 17:24:25 | → | Googulator joins (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) |
| 2026-02-17 17:25:54 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2026-02-17 17:36:09 | × | Googulator quits (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-02-17 17:36:17 | → | Googulator3 joins (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) |
| 2026-02-17 17:36:31 | Googulator3 | is now known as Googulator |
| 2026-02-17 17:38:18 | → | prdak joins (~Thunderbi@user/prdak) |
| 2026-02-17 17:39:09 | × | Googulator quits (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) (Client Quit) |
| 2026-02-17 17:39:23 | → | Googulator joins (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) |
| 2026-02-17 17:40:34 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Read error: No route to host) |
| 2026-02-17 17:43:00 | × | prdak quits (~Thunderbi@user/prdak) (Ping timeout: 264 seconds) |
| 2026-02-17 17:44:05 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 2026-02-17 17:44:19 | → | Square3 joins (~Square@user/square) |
| 2026-02-17 17:44:33 | → | Googulator28 joins (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) |
| 2026-02-17 17:44:54 | × | Googulator quits (~Googulato@2a01-036d-0106-499d-6164-ec92-51a0-9cde.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-02-17 17:46:24 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2026-02-17 17:50:43 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Read error: No route to host) |
All times are in UTC.