| 2024-08-27 00:02:30 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 00:02:40 +0200 | son0p | (~ff@186.121.18.131) (Quit: Leaving) |
| 2024-08-27 00:06:04 +0200 | Pixi` | (~Pixi@user/pixi) (Quit: Leaving) |
| 2024-08-27 00:06:58 +0200 | cpressey | (~weechat@176.254.71.203) (Quit: WeeChat 4.3.0) |
| 2024-08-27 00:07:30 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) |
| 2024-08-27 00:08:42 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) (Client Quit) |
| 2024-08-27 00:10:23 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 00:10:26 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) |
| 2024-08-27 00:12:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 00:17:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-08-27 00:20:54 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) (Quit: ash3en) |
| 2024-08-27 00:22:43 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) |
| 2024-08-27 00:28:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 00:30:04 +0200 | <zero> | i'm trying to get my head aroud the Tardis Monad. any good resource? |
| 2024-08-27 00:30:41 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-08-27 00:31:30 +0200 | <probie> | <joke>Yes, but they're all in the future</joke> |
| 2024-08-27 00:32:01 +0200 | <Rembane> | zero: Like this? https://blog.csongor.co.uk/time-travel-in-haskell-for-dummies/ |
| 2024-08-27 00:32:17 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) (Remote host closed the connection) |
| 2024-08-27 00:32:29 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) |
| 2024-08-27 00:34:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 00:35:29 +0200 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-02-184-145-10-5.dsl.bell.ca) |
| 2024-08-27 00:35:44 +0200 | AlexNoo | (~AlexNoo@178.34.150.250) (Read error: Connection reset by peer) |
| 2024-08-27 00:36:07 +0200 | AlexNoo | (~AlexNoo@178.34.150.250) |
| 2024-08-27 00:36:29 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3109-4750-f47c-92a3-9b35-3df5.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 00:36:52 +0200 | <dmj`> | when did "Just v <- M.lookup k m = v" become "non-standard" pattern guard usage |
| 2024-08-27 00:37:10 +0200 | <dmj`> | "| Just v <- " ... |
| 2024-08-27 00:38:21 +0200 | <probie> | context? |
| 2024-08-27 00:39:01 +0200 | finsternis | (~X@23.226.237.192) |
| 2024-08-27 00:41:09 +0200 | <dmj`> | just getting this warning |
| 2024-08-27 00:42:19 +0200 | ash3en | (~Thunderbi@2a02:3100:7e98:4100:89bf:d133:e52a:2d93) (Quit: ash3en) |
| 2024-08-27 00:42:27 +0200 | <dmj`> | but its clearly part of the 2010 spec |
| 2024-08-27 00:44:52 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 00:46:06 +0200 | <zero> | Rembane: that's the one i just read :) |
| 2024-08-27 00:46:19 +0200 | <haskellbridge> | <magic_rb> "Just value <- lookup key map = value` is weird, what i are you trying to achieve? |
| 2024-08-27 00:46:40 +0200 | <geekosaur> | looks sensible to me as a pattern guard |
| 2024-08-27 00:46:47 +0200 | <Rembane> | zero: Sweet, that's the only one I've seen so far. :) |
| 2024-08-27 00:47:04 +0200 | <haskellbridge> | <magic_rb> Inside a monadic assignment thingie? |
| 2024-08-27 00:47:08 +0200 | <geekosaur> | "if the result of `lookup key map` is `Just v`, produce `v`" |
| 2024-08-27 00:47:20 +0200 | <geekosaur> | it's not monadic assignment, it's a pttern guard |
| 2024-08-27 00:47:24 +0200 | <haskellbridge> | <magic_rb> Huh, what if it is not? Exception |
| 2024-08-27 00:47:40 +0200 | <geekosaur> | no, if it's not, the guard fails to match |
| 2024-08-27 00:47:50 +0200 | <geekosaur> | look up pattern guards |
| 2024-08-27 00:48:04 +0200 | <haskellbridge> | <magic_rb> I know about those, i just never seen that form, or im too tired |
| 2024-08-27 00:48:36 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
| 2024-08-27 00:48:41 +0200 | <haskellbridge> | <magic_rb> Okay i guess i dont know about those |
| 2024-08-27 00:48:48 +0200 | <haskellbridge> | <magic_rb> Well, TIL |
| 2024-08-27 00:50:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-08-27 00:52:21 +0200 | <zero> | why do we need parenthesis around Data.Map.!? in `:type (Data.Map.!?)` inside ghci? |
| 2024-08-27 00:53:21 +0200 | <zero> | ah i guess i get it |
| 2024-08-27 00:53:25 +0200 | <zero> | needs to be an expression |
| 2024-08-27 00:56:12 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 276 seconds) |
| 2024-08-27 00:57:53 +0200 | <jle`> | zero: fwiw :info Data.Map.!? works |
| 2024-08-27 01:00:08 +0200 | AlexNoo_ | (~AlexNoo@178.34.150.250) |
| 2024-08-27 01:00:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 01:03:16 +0200 | AlexNoo | (~AlexNoo@178.34.150.250) (Ping timeout: 252 seconds) |
| 2024-08-27 01:04:18 +0200 | <dmj`> | geekosaur: ghc 9.6.5 thinks otherwise :( |
| 2024-08-27 01:04:20 +0200 | son0p | (~ff@2800:e2:f80:ee7::1) |
| 2024-08-27 01:04:36 +0200 | <dmj`> | magic_rb: there's soft pattern match failures, like what catMaybes does |
| 2024-08-27 01:04:41 +0200 | <dmj`> | @src catMaybes |
| 2024-08-27 01:04:41 +0200 | <lambdabot> | catMaybes ls = [x | Just x <- ls] |
| 2024-08-27 01:05:17 +0200 | <dmj`> | pattern match failure in guards soft fail like the ones in list comps |
| 2024-08-27 01:05:51 +0200 | <dmj`> | | Just (TVar k) <- M.lookup t s = TVar k |
| 2024-08-27 01:06:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-08-27 01:07:00 +0200 | <zero> | jle`: yup, :info works with identifiers, :type works with expressions |
| 2024-08-27 01:07:17 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-08-27 01:08:23 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-08-27 01:10:54 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-08-27 01:16:45 +0200 | dorin | (~dorin@user/dorin) |
| 2024-08-27 01:17:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 01:17:45 +0200 | <dmj`> | foldl' finally made it into the Prelude, never thought I'd see the day |
| 2024-08-27 01:18:05 +0200 | <dmj`> | * fights back tears * |
| 2024-08-27 01:18:37 +0200 | <EvanR> | one down, like 900 other things that should be in prelude to go xD |
| 2024-08-27 01:20:07 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 2024-08-27 01:21:36 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-08-27 01:21:42 +0200 | <dmj`> | base should just eat mtl, transformers, text, aeson, time, haddock, cabal, etc. maybe more boot packages |
| 2024-08-27 01:21:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 01:24:45 +0200 | <EvanR> | batteries |
| 2024-08-27 01:26:12 +0200 | <probie> | I don't think aeson belongs on that list |
| 2024-08-27 01:27:13 +0200 | stef204 | (~stef204@user/stef204) (Quit: WeeChat 4.2.1) |
| 2024-08-27 01:27:41 +0200 | <dmj`> | EvanR: boom |
| 2024-08-27 01:27:45 +0200 | <probie> | It's too opinionated and has (what I consider to be) the wrong opinions (I'm not a fan of `ToJSON`/`FromJSON` typeclasses, because how to serialise depends on context and isn't a property a type itself) |
| 2024-08-27 01:29:42 +0200 | <EvanR> | what other json libraries are there |
| 2024-08-27 01:29:52 +0200 | <dmj`> | https://hackage.haskell.org/package/ghc-9.10.1/docs/GHC-Utils-Json.html |
| 2024-08-27 01:31:04 +0200 | <zero> | i dont think mtl, transformers, aeson and time belong on that list |
| 2024-08-27 01:31:12 +0200 | <zero> | not sure about haddock and cabal |
| 2024-08-27 01:31:32 +0200 | <probie> | https://hackage.haskell.org/package/waargonaut |
| 2024-08-27 01:32:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 01:33:07 +0200 | <glguy> | putting things into base just makes them harder to upgrade, not easier to use |
| 2024-08-27 01:33:46 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 2024-08-27 01:34:08 +0200 | <zero> | exactly |
| 2024-08-27 01:34:30 +0200 | <dolio> | mtl was split out of base long ago. |
| 2024-08-27 01:35:24 +0200 | <zero> | mtl serves a very opinionated pattern that many refuse to use |
| 2024-08-27 01:35:42 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-08-27 01:36:02 +0200 | <zero> | it would be like having lens libraries in base |
| 2024-08-27 01:36:55 +0200 | <dmj`> | if we could divorce ghc from base that might help, or base from ghc rather. I think parts of the rts depend on base |
| 2024-08-27 01:37:07 +0200 | <geekosaur> | it's in progress |
| 2024-08-27 01:37:13 +0200 | <zero> | that would be nice |
| 2024-08-27 01:37:39 +0200 | <dmj`> | well, well |
| 2024-08-27 01:37:48 +0200 | <geekosaur> | there are a very few things, mostly ghc wired-in things, that depend on base. those are being moved to ghc-base, which is intended to be minimal |
| 2024-08-27 01:38:06 +0200 | <geekosaur> | (you will see ghc-base already in 9.10 and I think 9.8) |
| 2024-08-27 01:38:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 01:38:29 +0200 | <dmj`> | is this the balkanization effort Ericson was / is working on |
| 2024-08-27 01:38:47 +0200 | <zero> | and hopefully updated once in a blue moon |
| 2024-08-27 01:39:14 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-08-27 01:40:00 +0200 | <geekosaur> | similarly there are things being moved to ghc-internal, but that's more complicated as it'll depend to some extent on the "actually standardize ghc-api" effort which is still in the planning phase |
| 2024-08-27 01:40:46 +0200 | <geekosaur> | don't recall who's working on it, have seen some discussion though |
| 2024-08-27 01:40:56 +0200 | <dmj`> | what if we just imported everything into a single module, and let the optimizer do it's thing, don't rely on interface files |
| 2024-08-27 01:41:41 +0200 | <geekosaur> | isn't that effectively WPC? |
| 2024-08-27 01:41:41 +0200 | <c_wraith> | there are some things in GHC that are superlinear in module size, but not in module count |
| 2024-08-27 01:41:45 +0200 | <zero> | things keep moving in a good direction |
| 2024-08-27 01:41:45 +0200 | <zero> | slowly but steadily |
| 2024-08-27 01:43:46 +0200 | <zero> | someone once explained in detail why WPC is not posssible in haskell |
| 2024-08-27 01:44:08 +0200 | <dmj`> | zero: do you have a link to that? |
| 2024-08-27 01:44:57 +0200 | <dmj`> | geekosaur: yea, but its still optimizations on a higher order IR, if we defunctionalized first we'd probably have better results with optimization |
| 2024-08-27 01:44:58 +0200 | <geekosaur> | the GRIN project was working on that. sadly I think it stalled, possibly over the superlinearity issue |
| 2024-08-27 01:45:14 +0200 | <zero> | unfortunately i lost most my IRC logs from that time, but maybe they can be found at ircbrowse.tomsmeding.com |
| 2024-08-27 01:45:22 +0200 | <zero> | it was a few years ago though |
| 2024-08-27 01:46:21 +0200 | <geekosaur> | sadly its search doesn't work and I think search engines and such are prohibited from indexing it? |
| 2024-08-27 01:46:53 +0200 | <dmj`> | zero: if its possible in ocaml w/ mlton, shouldn't be a problem w/ haskell |
| 2024-08-27 01:47:29 +0200 | <dmj`> | ocaml has gadts and higher order functions |
| 2024-08-27 01:49:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 01:49:35 +0200 | <geekosaur> | I'm not aware of any explanations of why WPC would be impossible. I am aware of an explanation of why even with WPC it's not possible to eliminate typeclass dictionaries at compile time; might that have been what you remember? |
| 2024-08-27 01:50:00 +0200 | <geekosaur> | (polymorphic recursion) |
| 2024-08-27 01:53:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-08-27 01:55:59 +0200 | <dmj`> | rust just disables polymorphic recursion iirc, for haskell we could compile it differently. Instead of just attempting to inline into oblivion, there is a technique called intensional type analysis (that oleg discusses) that detects polymorphic recursion and basically constructs a mini interpreter from the type language. Converts it into a recursive expression tree |
| 2024-08-27 01:56:05 +0200 | <dmj`> | https://okmij.org/ftp/Computation/typeclass.html#intensional |
| 2024-08-27 01:56:39 +0200 | <dmj`> | I think flix.dev disables it too, as a "feature" |
| 2024-08-27 01:56:51 +0200 | <dmj`> | since the gains from inlining are so huge |
| 2024-08-27 01:57:49 +0200 | <dmj`> | I'd just disable it first, see how much stuff breaks w/o it |
| 2024-08-27 02:01:11 +0200 | <Maxdamantus> | I don't think Rust necessarily disables it. I think it just gives up if the stack is too big. |
| 2024-08-27 02:01:15 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb41fdef54b6136c7789.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-08-27 02:01:33 +0200 | <Maxdamantus> | so you can trigger the same limitation without actual polymorphic recursion. |
| 2024-08-27 02:02:49 +0200 | <dmj`> | yea, you're right, it just fails at compile time, with a "won't fix" github issue |
| 2024-08-27 02:03:21 +0200 | <Maxdamantus> | I saw something on HN the other day about a Rust ABI that I think might be related to supporting things like polymorphic recursion. |
| 2024-08-27 02:04:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 02:04:51 +0200 | <dmj`> | Maxdamantus: that sounds interesting |
| 2024-08-27 02:05:17 +0200 | <Maxdamantus> | particularly, if there's a Rust ABI in the future and it supports generic functions, presumably that will be implemented in a way that would also support polymorphic recursion, since the lack od it is due to the compiler always monomorphising generic code. |
| 2024-08-27 02:06:39 +0200 | <Maxdamantus> | (eg, C++'s ABI doesn't support generics/templates aiui, since those always exist in headers and are always expanded at compile time) |
| 2024-08-27 02:08:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-08-27 02:10:27 +0200 | <dmj`> | yea seems like once you go polymorphic recursive you have to forego monomorphization, especially if its unbounded. |
| 2024-08-27 02:12:06 +0200 | ddellacosta | (~ddellacos@ool-44c73c8f.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 2024-08-27 02:12:26 +0200 | ddellacosta | (~ddellacos@ool-44c73c8f.dyn.optonline.net) |
| 2024-08-27 02:12:40 +0200 | <jle`> | it would be cool if TypeAbstraction'd names showed up in the error messages |
| 2024-08-27 02:14:52 +0200 | <zero> | geekosaur: maybe i mispoke. it was not about it being impossible in general, just about it not being possible right now because it's not that simple |
| 2024-08-27 02:15:55 +0200 | dorin | (~dorin@user/dorin) (Ping timeout: 256 seconds) |
| 2024-08-27 02:18:36 +0200 | <dmj`> | Maxdamantus: data monomorphization is the biggest win, I'd love to see how much code breaks w/o polymorphic recursion |
| 2024-08-27 02:18:50 +0200 | <dmj`> | jle`: hmmm maybe a type checker plugin ? |
| 2024-08-27 02:20:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 02:20:10 +0200 | <dmj`> | geekosaur: barring polymorphic recursion, it should be possible to inline all instances under WPC |
| 2024-08-27 02:20:20 +0200 | <geekosaur> | right |
| 2024-08-27 02:21:04 +0200 | <geekosaur> | hm, although as ghc currently is that presents some problems depending on when that inlining happens |
| 2024-08-27 02:21:44 +0200 | <geekosaur> | there's at least three bug reports on ghc's tracker that show what happens if IO gets inlined |
| 2024-08-27 02:23:37 +0200 | <geekosaur> | (all three rejected with "don't do that") |
| 2024-08-27 02:24:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 02:25:32 +0200 | <dmj`> | geekosaur: For typeclass instances that invoke other instances recursively that shouldn't be a problem since elaboration would produce a dictionary entailment constraint that would ensure the instance exists. But polymorphic recursion w/o a typeclass constraint, I'd like to see how much code exists with that. |
| 2024-08-27 02:26:31 +0200 | <geekosaur> | I'm not sure any does, since without a type witness (which in ghc is discharged by a typeclass dictionary) it wouldn't know what to do? |
| 2024-08-27 02:27:05 +0200 | <geekosaur> | maybe with some type level trickery which amounts to the same thing |
| 2024-08-27 02:27:16 +0200 | <dmj`> | there's that contrived example of the infinitely expanding tuple heh |
| 2024-08-27 02:29:24 +0200 | <dmj`> | sort of looks like (a,a) -> (a,(a,a)) -> (a,(a,(a,a))), but recursively looks like another call to (a,a) |
| 2024-08-27 02:30:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 02:31:03 +0200 | <geekosaur> | I thought ghc threw an infinite type error for things like that? |
| 2024-08-27 02:31:10 +0200 | <geekosaur> | a ~ (a,a) |
| 2024-08-27 02:33:18 +0200 | <Maxdamantus> | dmj`: by data monomorphisation, do you mean lack of a "universal representation" (eg, every generic field/variable is a pointer)? |
| 2024-08-27 02:33:33 +0200 | <Maxdamantus> | if so, I kind of think of that as a separate thing. |
| 2024-08-27 02:34:19 +0200 | <geekosaur> | I assumed the point of that was eliminating a lot of pointer chasing by inlining the unboxed versions/operations |
| 2024-08-27 02:34:34 +0200 | <Maxdamantus> | it's primarily functions that are generic. in order to support efficient data types, size/alignment will likely be passed at runtime to those generic functions, |
| 2024-08-27 02:34:36 +0200 | <geekosaur> | which you can only do if it's monomorphic |
| 2024-08-27 02:35:10 +0200 | <dmj`> | geekosaur: I know its possible somehow to do polymorphic recursion w/o typeclass constraints |
| 2024-08-27 02:35:58 +0200 | <Maxdamantus> | it might get a bit complicated for higher-kinded polymorphism, since at that point you're having to generate functions on size/alignment, but I feel like that is still feasibly solvable. |
| 2024-08-27 02:39:20 +0200 | <dmj`> | Maxdamantus: to geekosaur's point, I think the universal representation would still be necessary, since a type tag would still be required if it were a heap object. This would be required for the runtime system to allocate the right amount of space and the GC to deal with it the same as other objects, but the pointer indirections would be reduced significantly. Moreso w/ WPC since there are no more "unknown calls" which block opts |
| 2024-08-27 02:39:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 02:40:32 +0200 | <Maxdamantus> | Well, I think that would be solved the same way, but you just have a tracing function for every data type. |
| 2024-08-27 02:40:48 +0200 | <Maxdamantus> | if the data type is generic, that tracing function is generic. |
| 2024-08-27 02:40:53 +0200 | dtman34 | (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) (Ping timeout: 248 seconds) |
| 2024-08-27 02:41:27 +0200 | MattByName | (~Matthew@user/MattByName) () |
| 2024-08-27 02:43:00 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-08-27 02:43:15 +0200 | troojg | (~troojg@user/troojg) |
| 2024-08-27 02:43:27 +0200 | <Maxdamantus> | allocation is done by the calling function, which already knows the size of the type (again, might involve using that runtime size/alignment information) |
| 2024-08-27 02:47:38 +0200 | <dmj`> | yea that could work |
| 2024-08-27 02:50:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 02:52:40 +0200 | <dmj`> | or tracing function could just operate on tag type, byte count and treat all bytes as (void *) |
| 2024-08-27 02:54:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 02:56:48 +0200 | <Maxdamantus> | but then you're forcing all code to use the suboptimal representation. |
| 2024-08-27 02:58:04 +0200 | <Maxdamantus> | with what I'm suggesting, a function on `Vec<i32>` can use the optimal representation that has always been used, and can inline code to do with `i32` etc. |
| 2024-08-27 02:58:48 +0200 | <Maxdamantus> | and that's still compatible with a function on `Vec<T>`, which won't be as inlined, but still supports the same representation. |
| 2024-08-27 03:00:32 +0200 | dysthesis | (~dysthesis@user/dysthesis) |
| 2024-08-27 03:05:31 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 03:06:44 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2024-08-27 03:08:32 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-08-27 03:08:37 +0200 | <dmj`> | Maxdamantus: the Vec<i32> could live inside some struct that has a type tag, but the i32s themselves would be unboxed and have some kind of finalizer that the GC would invoke (on the entire Vec<i32>), where operations use SIMD and accesses to the Vec<i32> become amortized |
| 2024-08-27 03:10:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2024-08-27 03:10:53 +0200 | <Maxdamantus> | dmj`: what determines that there's a type tag? does a `Vec<Vec<i32>>` have a tag for each `Vec<i32>`? |
| 2024-08-27 03:13:44 +0200 | <Maxdamantus> | if it's for GC, you should only need to start deriving the types at the GC roots, ie the variables in currently live stack frames. |
| 2024-08-27 03:14:07 +0200 | <Maxdamantus> | so there shouldn't be a need to store tags in the heap itself. |
| 2024-08-27 03:15:53 +0200 | <dmj`> | Maxdamantus: depends on how the Vec is implemented. I would FFI into LLVM's SIMD vector type, and newtype wrap it for the various types, then make it ergonomic w/ parametric polymorphism |
| 2024-08-27 03:17:01 +0200 | <dmj`> | Maxdamantus: Depends on how your stack is implemented. If you're using green threads the TSOs live on the heap, along with their stacks. This is the shadow stack model iiuc |
| 2024-08-27 03:20:04 +0200 | <dmj`> | If you're using the LLVM FFI, the representation wouldn't have overhead |
| 2024-08-27 03:20:57 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 03:20:59 +0200 | krei-se | (~krei-se@p57af2d39.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 2024-08-27 03:21:02 +0200 | <dmj`> | you might able to alloca w/ Vec<i32> |
| 2024-08-27 03:25:32 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 03:34:36 +0200 | krei-se | (~krei-se@p57af29d2.dip0.t-ipconnect.de) |
| 2024-08-27 03:35:37 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-08-27 03:36:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 03:38:57 +0200 | <dmj`> | "clang only" |
| 2024-08-27 03:40:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 03:50:42 +0200 | darkstardevx | (~darkstard@50.53.3.2) |
| 2024-08-27 03:51:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 03:56:15 +0200 | troojg | (~troojg@user/troojg) (Ping timeout: 276 seconds) |
| 2024-08-27 03:56:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 04:04:21 +0200 | bilegeek | (~bilegeek@2600:1008:b017:c901:621d:4241:2804:e5ab) (Quit: Leaving) |
| 2024-08-27 04:06:35 +0200 | td_ | (~td@i53870916.versanet.de) (Ping timeout: 252 seconds) |
| 2024-08-27 04:07:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 04:08:35 +0200 | td_ | (~td@i53870933.versanet.de) |
| 2024-08-27 04:11:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 04:18:08 +0200 | slack1256 | (~slack1256@2803:c600:5111:8029:d2a9:631a:b025:6268) |
| 2024-08-27 04:21:57 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 244 seconds) |
| 2024-08-27 04:22:28 +0200 | poscat | (~poscat@user/poscat) (Quit: Bye) |
| 2024-08-27 04:22:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 04:26:31 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 04:27:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-08-27 04:30:48 +0200 | poscat | (~poscat@user/poscat) |
| 2024-08-27 04:34:28 +0200 | rekahsoft | (~rekahsoft@bras-base-orllon1103w-grc-02-184-145-10-5.dsl.bell.ca) (Ping timeout: 252 seconds) |
| 2024-08-27 04:37:06 +0200 | <dmj`> | Maxdamantus: https://llvm.org/docs/LangRef.html#t-vector |
| 2024-08-27 04:37:10 +0200 | drdo1 | (~drdo@bl5-29-74.dsl.telepac.pt) |
| 2024-08-27 04:38:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 04:39:14 +0200 | drdo | (~drdo@bl5-29-74.dsl.telepac.pt) (Ping timeout: 248 seconds) |
| 2024-08-27 04:39:14 +0200 | drdo1 | drdo |
| 2024-08-27 04:42:36 +0200 | drdo5 | (~drdo@bl5-29-74.dsl.telepac.pt) |
| 2024-08-27 04:42:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-08-27 04:43:59 +0200 | drdo | (~drdo@bl5-29-74.dsl.telepac.pt) (Ping timeout: 260 seconds) |
| 2024-08-27 04:43:59 +0200 | drdo5 | drdo |
| 2024-08-27 04:46:21 +0200 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-08-27 04:53:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 04:58:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-08-27 04:59:34 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-08-27 05:08:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 05:13:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 2024-08-27 05:20:15 +0200 | <haskellbridge> | <thirdofmay18081814goya> you have a recursive function that is constant after an unknown number of applications on "x" |
| 2024-08-27 05:20:23 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a way to get this value? |
| 2024-08-27 05:21:06 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2024-08-27 05:21:56 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-08-27 05:24:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 05:24:24 +0200 | <dmj`> | use Eq to check if you're at a fixpoint |
| 2024-08-27 05:28:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-08-27 05:30:44 +0200 | <Maxdamantus> | dmj`: I imagine it avoid refererring to that LLVM type as part of fundamentally representing the `Vec<_>` objects, since presumably you can always opportunistically reinterpret as an LLVM vector when you want to perform those operations. |
| 2024-08-27 05:31:05 +0200 | <Maxdamantus> | (assuming the elements are byte-sized) |
| 2024-08-27 05:31:47 +0200 | <Maxdamantus> | imagine it would make sense to avoid * |
| 2024-08-27 05:39:14 +0200 | cheater_ | (~Username@user/cheater) |
| 2024-08-27 05:39:44 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 05:39:44 +0200 | aforemny_ | (~aforemny@i59F516CA.versanet.de) |
| 2024-08-27 05:40:09 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 2024-08-27 05:40:19 +0200 | cheater_ | cheater |
| 2024-08-27 05:40:37 +0200 | aforemny | (~aforemny@i59F516F8.versanet.de) (Ping timeout: 248 seconds) |
| 2024-08-27 05:40:40 +0200 | cheater | (~Username@user/cheater) (Read error: Connection reset by peer) |
| 2024-08-27 05:41:26 +0200 | cheater_ | (~Username@user/cheater) |
| 2024-08-27 05:41:26 +0200 | cheater_ | cheater |
| 2024-08-27 05:44:48 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-08-27 05:55:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 06:00:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 06:06:38 +0200 | slack1256 | (~slack1256@2803:c600:5111:8029:d2a9:631a:b025:6268) (Remote host closed the connection) |
| 2024-08-27 06:07:57 +0200 | glguy | (glguy@libera/staff/glguy) (Read error: Connection reset by peer) |
| 2024-08-27 06:08:48 +0200 | glguy | (glguy@libera/staff/glguy) |
| 2024-08-27 06:10:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 06:15:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-08-27 06:26:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 06:30:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 06:41:22 +0200 | jinsun | (~jinsun@user/jinsun) () |
| 2024-08-27 06:41:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 06:46:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-08-27 06:54:28 +0200 | michalz | (~michalz@185.246.207.221) |
| 2024-08-27 06:56:52 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 07:05:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 07:09:36 +0200 | neuroevolutus | (~neuroevol@37.19.200.148) |
| 2024-08-27 07:15:56 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 07:18:39 +0200 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2024-08-27 07:20:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 07:21:29 +0200 | michalz | (~michalz@185.246.207.203) |
| 2024-08-27 07:27:09 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-08-27 07:30:06 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-08-27 07:31:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 07:34:30 +0200 | Square | (~Square@user/square) |
| 2024-08-27 07:35:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-08-27 07:36:21 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 07:36:58 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 07:39:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 07:40:07 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 07:41:23 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 07:43:59 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 07:46:01 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 07:46:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 07:49:32 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 07:50:47 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 07:51:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 07:54:57 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 07:56:31 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 08:02:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 08:03:16 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 08:06:11 +0200 | Square2 | (~Square4@user/square) |
| 2024-08-27 08:06:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-08-27 08:08:41 +0200 | Square | (~Square@user/square) (Ping timeout: 255 seconds) |
| 2024-08-27 08:12:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-08-27 08:17:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 08:21:11 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 2024-08-27 08:21:23 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb83c8b55ff2a9bbb599.dip0.t-ipconnect.de) |
| 2024-08-27 08:22:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 08:24:07 +0200 | akegalj | (~akegalj@197-208.dsl.iskon.hr) |
| 2024-08-27 08:24:43 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b9a0:3dc1:ba12:10da:4091) (Ping timeout: 252 seconds) |
| 2024-08-27 08:25:18 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b9a0:f873:c933:3c9b:237a) |
| 2024-08-27 08:31:26 +0200 | Inst | (~Inst@user/Inst) |
| 2024-08-27 08:32:58 +0200 | CiaoSen | (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) |
| 2024-08-27 08:33:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 08:33:38 +0200 | neuroevolutus | (~neuroevol@37.19.200.148) (Quit: Client closed) |
| 2024-08-27 08:34:47 +0200 | kalj | (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) |
| 2024-08-27 08:35:47 +0200 | kalj | (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) (Client Quit) |
| 2024-08-27 08:38:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-08-27 08:41:14 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-08-27 08:45:18 +0200 | oo_miguel | (~Thunderbi@78.10.207.45) |
| 2024-08-27 08:48:25 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 08:51:01 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 08:53:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 09:01:47 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 09:06:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 09:18:06 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 2024-08-27 09:19:50 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-08-27 09:35:55 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-08-27 09:55:58 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-08-27 09:58:57 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-08-27 10:04:10 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-08-27 10:06:07 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-08-27 10:06:40 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 2024-08-27 10:08:05 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-08-27 10:08:54 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2024-08-27 10:09:11 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-08-27 10:10:01 +0200 | dysthesis | (~dysthesis@user/dysthesis) (Ping timeout: 260 seconds) |
| 2024-08-27 10:12:10 +0200 | dysthesis | (~dysthesis@user/dysthesis) |
| 2024-08-27 10:20:33 +0200 | sroso | (~sroso@user/SrOso) |
| 2024-08-27 10:25:21 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-08-27 10:25:30 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-08-27 10:37:11 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-08-27 10:39:20 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-08-27 10:40:59 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 2024-08-27 10:43:16 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 2024-08-27 10:46:24 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-08-27 10:46:48 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 2024-08-27 10:47:36 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-08-27 10:52:27 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-08-27 10:53:50 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-08-27 10:56:38 +0200 | gehmehgeh | gmg |
| 2024-08-27 10:56:39 +0200 | gmg | (~user@user/gehmehgeh) (Client Quit) |
| 2024-08-27 11:00:51 +0200 | darkstarx | (darkstarde@gateway/vpn/protonvpn/darkstardevx) |
| 2024-08-27 11:03:19 +0200 | darkstardevx | (~darkstard@50.53.3.2) (Ping timeout: 260 seconds) |
| 2024-08-27 11:09:53 +0200 | darkstardev13 | (~darkstard@50.53.3.2) |
| 2024-08-27 11:10:50 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-08-27 11:11:02 +0200 | gehmehgeh | gmg |
| 2024-08-27 11:12:30 +0200 | darkstarx | (darkstarde@gateway/vpn/protonvpn/darkstardevx) (Ping timeout: 246 seconds) |
| 2024-08-27 11:14:35 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-08-27 11:15:51 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-98d8-b0b9-f0fb-b020.rev.sfr.net) |
| 2024-08-27 11:16:34 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-98d8-b0b9-f0fb-b020.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 11:18:23 +0200 | CiaoSen | (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) (Ping timeout: 244 seconds) |
| 2024-08-27 11:41:42 +0200 | CiaoSen | (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) |
| 2024-08-27 11:46:23 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: Ping timeout (120 seconds)) |
| 2024-08-27 11:46:40 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-08-27 11:58:00 +0200 | sam113101 | (~sam@24.157.253.231) (Ping timeout: 246 seconds) |
| 2024-08-27 11:58:04 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-08-27 11:59:46 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-08-27 12:01:29 +0200 | CiaoSen | (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 2024-08-27 12:01:56 +0200 | darkstardev13 | (~darkstard@50.53.3.2) (Quit: Leaving) |
| 2024-08-27 12:07:27 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-08-27 12:08:57 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 276 seconds) |
| 2024-08-27 12:09:42 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 2024-08-27 12:10:12 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-08-27 12:18:07 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 264 seconds) |
| 2024-08-27 12:22:17 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-08-27 12:28:05 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2024-08-27 12:28:47 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-08-27 12:34:21 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-08-27 12:40:34 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b9a0:f873:c933:3c9b:237a) (Ping timeout: 260 seconds) |
| 2024-08-27 12:41:18 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-08-27 12:41:28 +0200 | jcarpenter2 | (~lol@96.78.87.197) |
| 2024-08-27 12:42:42 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-08-27 12:44:33 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Ping timeout: 246 seconds) |
| 2024-08-27 13:02:41 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-08-27 13:03:41 +0200 | <haskellbridge> | <thirdofmay18081814goya> at dmj: ended up doing that, that's pretty much the only solution it seems |
| 2024-08-27 13:04:11 +0200 | <haskellbridge> | <thirdofmay18081814goya> unrelated: anyone use some recursion scheme in particular regularly? |
| 2024-08-27 13:13:47 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 2024-08-27 13:16:04 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Ping timeout: 272 seconds) |
| 2024-08-27 13:16:05 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-08-27 13:19:16 +0200 | CiaoSen | (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) |
| 2024-08-27 13:25:27 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 2024-08-27 13:30:31 +0200 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-08-27 13:32:25 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-08-27 13:38:16 +0200 | <haskellbridge> | <Bowuigi> No but technically yes, "cata" and "ana" are useful |
| 2024-08-27 13:40:07 +0200 | xff0x | (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) |
| 2024-08-27 13:40:45 +0200 | smalltalkman | (uid545680@2a03:5180:f:4::8:5390) |
| 2024-08-27 13:41:11 +0200 | <Rembane> | They in combination are pretty |
| 2024-08-27 13:49:09 +0200 | dsrt^ | (ciwoudofon@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 248 seconds) |
| 2024-08-27 13:55:51 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-08-27 13:56:01 +0200 | sam113101 | (~sam@24.157.253.231) |
| 2024-08-27 14:02:41 +0200 | son0p | (~ff@2800:e2:f80:ee7::1) (Ping timeout: 244 seconds) |
| 2024-08-27 14:03:58 +0200 | <dminuoso> | Yes, catanas are pretty - but sharp and dangerous. |
| 2024-08-27 14:09:57 +0200 | biberu\ | (~biberu@user/biberu) |
| 2024-08-27 14:11:21 +0200 | ZharMeny | (~user@user/ZharMeny) |
| 2024-08-27 14:12:28 +0200 | biberu | (~biberu@user/biberu) (Ping timeout: 245 seconds) |
| 2024-08-27 14:12:29 +0200 | biberu\ | biberu |
| 2024-08-27 14:13:16 +0200 | dysthesis | (~dysthesis@user/dysthesis) (Ping timeout: 260 seconds) |
| 2024-08-27 14:15:28 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-08-27 14:22:01 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-08-27 14:22:09 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-08-27 14:41:05 +0200 | ddellacosta | (~ddellacos@ool-44c73c8f.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 2024-08-27 14:45:29 +0200 | gehmehgeh | gmg |
| 2024-08-27 15:03:26 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-08-27 15:08:48 +0200 | CiaoSen | (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 2024-08-27 15:08:48 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 272 seconds) |
| 2024-08-27 15:11:14 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-08-27 15:12:49 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 2024-08-27 15:17:32 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-08-27 15:22:24 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) |
| 2024-08-27 15:24:32 +0200 | son0p | (~ff@2800:e6:4001:8da7:232f:489b:caf3:dc20) |
| 2024-08-27 15:29:42 +0200 | dtman34 | (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) |
| 2024-08-27 15:31:25 +0200 | srazkvt | (~sarah_@2a01:e0a:483:6900:b6d5:d9cd:2f20:2e49) |
| 2024-08-27 15:36:11 +0200 | spew | (~spew@201.141.102.132) |
| 2024-08-27 15:38:38 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-08-27 15:39:50 +0200 | srazkvt | (~sarah_@2a01:e0a:483:6900:b6d5:d9cd:2f20:2e49) (Quit: Leaving) |
| 2024-08-27 15:40:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-08-27 15:46:33 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb83c8b55ff2a9bbb599.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-08-27 15:48:24 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Ping timeout: 252 seconds) |
| 2024-08-27 15:49:01 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-08-27 15:54:15 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-08-27 15:56:34 +0200 | xff0x | (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) (Ping timeout: 260 seconds) |
| 2024-08-27 15:59:30 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Ping timeout: 265 seconds) |
| 2024-08-27 16:00:07 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-08-27 16:04:03 +0200 | xff0x | (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) |
| 2024-08-27 16:09:13 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 16:09:33 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) |
| 2024-08-27 16:10:22 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 16:10:41 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) |
| 2024-08-27 16:17:17 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 2024-08-27 16:20:47 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Client Quit) |
| 2024-08-27 16:23:12 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-08-27 16:34:56 +0200 | jcarpenter2 | (~lol@96.78.87.197) (Ping timeout: 255 seconds) |
| 2024-08-27 16:42:31 +0200 | dans90387 | (~danse-nr3@user/danse-nr3) |
| 2024-08-27 16:44:08 +0200 | arahael | (~arahael@user/arahael) (Ping timeout: 245 seconds) |
| 2024-08-27 16:44:37 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) (Ping timeout: 248 seconds) |
| 2024-08-27 16:49:07 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb83b0c9f42d7d842c79.dip0.t-ipconnect.de) |
| 2024-08-27 16:58:11 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-08-27 17:04:57 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-08-27 17:15:16 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-08-27 17:20:05 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 17:22:12 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 17:26:31 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Remote host closed the connection) |
| 2024-08-27 17:32:08 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) |
| 2024-08-27 17:32:39 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-08-27 17:38:46 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 17:39:19 +0200 | <haskellbridge> | <thirdofmay18081814goya> is there a mapping in either direction between a state monad and a histomorphism? |
| 2024-08-27 17:40:01 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-e069-9844-ae47-6e63.rev.sfr.net) |
| 2024-08-27 17:53:10 +0200 | <probie> | What sort of mapping would you expect? To my mind they are very different things |
| 2024-08-27 17:54:59 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 260 seconds) |
| 2024-08-27 17:56:05 +0200 | alexherbo2 | (~alexherbo@2a02-8440-311b-18ba-e069-9844-ae47-6e63.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 17:57:32 +0200 | <EvanR> | in some sense you can replace statefulness with access to history |
| 2024-08-27 17:58:42 +0200 | <EvanR> | a webapp server could use a database, or it could have no database but the entire history of requests up to that point (and perhaps recompute the logical state that it needs) |
| 2024-08-27 17:58:48 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) |
| 2024-08-27 17:59:04 +0200 | dans90387 | (~danse-nr3@user/danse-nr3) () |
| 2024-08-27 18:02:19 +0200 | <EvanR> | the etymological or practical relationship between history and histomorphisms if any is an exercise for the reader |
| 2024-08-27 18:06:49 +0200 | sam113101 | (~sam@24.157.253.231) (Ping timeout: 260 seconds) |
| 2024-08-27 18:10:34 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 2024-08-27 18:11:03 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 2024-08-27 18:11:58 +0200 | SovereignNoumena | (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 2024-08-27 18:15:03 +0200 | akegalj | (~akegalj@197-208.dsl.iskon.hr) (Remote host closed the connection) |
| 2024-08-27 18:15:21 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-08-27 18:16:09 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-08-27 18:19:40 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 18:21:21 +0200 | sam113101 | (~sam@modemcable220.199-203-24.mc.videotron.ca) |
| 2024-08-27 18:23:37 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit) |
| 2024-08-27 18:24:04 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 18:24:16 +0200 | <monochrom> | IMO recursion schemes are an ad hoc zoo except for cata, ana, and Ralf Hinze's generalization via adjoint functors. |
| 2024-08-27 18:26:00 +0200 | <c_wraith> | that sounds like an insult against primitive recursion! |
| 2024-08-27 18:26:45 +0200 | <c_wraith> | ... sure, cata and para are computationally equivalent. but not operationally, especially in Haskell |
| 2024-08-27 18:26:58 +0200 | <monochrom> | No! Primitive recursion is covered by cata or maybe sometimes we need adjoint cata. |
| 2024-08-27 18:27:56 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-08-27 18:28:15 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-08-27 18:28:22 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-08-27 18:31:27 +0200 | az181 | (~az181@bmly-12-b2-v4wan-164596-cust791.vm4.cable.virginm.net) |
| 2024-08-27 18:35:37 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 265 seconds) |
| 2024-08-27 18:36:07 +0200 | Pixi | (~Pixi@user/pixi) |
| 2024-08-27 18:38:05 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) |
| 2024-08-27 18:39:30 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-08-27 18:50:09 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-08-27 18:55:28 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 2024-08-27 18:56:21 +0200 | ubert | (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 248 seconds) |
| 2024-08-27 19:00:40 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) (Read error: Connection reset by peer) |
| 2024-08-27 19:01:05 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-08-27 19:03:41 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-08-27 19:03:46 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) |
| 2024-08-27 19:05:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 19:07:34 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-08-27 19:10:25 +0200 | son0p | (~ff@2800:e6:4001:8da7:232f:489b:caf3:dc20) (Ping timeout: 265 seconds) |
| 2024-08-27 19:10:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 19:12:30 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-08-27 19:14:53 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b960:a04f:145c:6e83:611e) |
| 2024-08-27 19:15:44 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2024-08-27 19:19:47 +0200 | <probie> | EvanR: A histomorphism is just the "complete induction" form of a catamorphism. If it can be mapped to/from the state monad, so can a catamorphism |
| 2024-08-27 19:20:57 +0200 | <probie> | Does anyone have strong opinions about defining numeric constants as patterns instead of variables? |
| 2024-08-27 19:21:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 19:26:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-08-27 19:26:56 +0200 | aforemny | (~aforemny@2001:9e8:6ceb:b200:7a4b:8b9f:cdb1:25bb) |
| 2024-08-27 19:27:18 +0200 | pavonia | (~user@user/siracusa) |
| 2024-08-27 19:27:39 +0200 | SovereignNoumena | (~Sovereign@24.79.228.157) |
| 2024-08-27 19:27:45 +0200 | aforemny_ | (~aforemny@i59F516CA.versanet.de) (Ping timeout: 246 seconds) |
| 2024-08-27 19:28:38 +0200 | SovereignNoumena | (~Sovereign@24.79.228.157) (Read error: Connection reset by peer) |
| 2024-08-27 19:32:13 +0200 | <monochrom> | Would that be using pattern synonyms? |
| 2024-08-27 19:33:43 +0200 | <probie> | yes |
| 2024-08-27 19:33:57 +0200 | <monochrom> | It feels like #define but better. :) |
| 2024-08-27 19:34:33 +0200 | <EvanR> | does it compile better |
| 2024-08-27 19:35:04 +0200 | Square | (~Square@user/square) |
| 2024-08-27 19:35:49 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 248 seconds) |
| 2024-08-27 19:36:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 19:41:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-08-27 19:42:59 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) |
| 2024-08-27 19:43:17 +0200 | <probie> | Is there something like `Data.Vector.Unboxed.Mutable` that can allocate more memory than elements and `grow` in place (if there's sufficient backing space)? Or do I have to build such a thing myself? |
| 2024-08-27 19:44:41 +0200 | <monochrom> | I haven't seen it in a library. |
| 2024-08-27 19:45:17 +0200 | <monochrom> | But I haven't looked for it really hard. |
| 2024-08-27 19:48:07 +0200 | <EvanR> | what happens if it tries to grow but ran out of space |
| 2024-08-27 19:48:50 +0200 | <monochrom> | I guess the same as trying to get a too-big array in the first place. |
| 2024-08-27 19:49:11 +0200 | <Franciman> | hi EvanR , i think it is allowed to grow only as far as the pre-allocated memory permits |
| 2024-08-27 19:49:50 +0200 | <EvanR> | hi Franciman |
| 2024-08-27 19:51:07 +0200 | <monochrom> | OK, that's fair. |
| 2024-08-27 19:51:50 +0200 | <EvanR> | since it's Mutable you can throw an exception |
| 2024-08-27 19:52:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 19:54:17 +0200 | Square | (~Square@user/square) (Ping timeout: 255 seconds) |
| 2024-08-27 19:54:25 +0200 | <mauke> | https://paste.tomsmeding.com/xgQtgjM8 clearly this is what PatternSynonyms were intended for |
| 2024-08-27 19:56:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 19:58:59 +0200 | Square | (~Square@user/square) |
| 2024-08-27 20:00:47 +0200 | <EvanR> | that's so cursed |
| 2024-08-27 20:05:11 +0200 | <Franciman> | is there any document formally defining how haskell to core translation works? |
| 2024-08-27 20:05:54 +0200 | Square | (~Square@user/square) (Ping timeout: 246 seconds) |
| 2024-08-27 20:06:05 +0200 | <probie> | <unhelpful>the source code of GHC</unhelpful> |
| 2024-08-27 20:06:37 +0200 | <mauke> | reflections on formalizing formalizers |
| 2024-08-27 20:07:00 +0200 | <monochrom> | That is evil. |
| 2024-08-27 20:07:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 20:08:05 +0200 | Square | (~Square@user/square) |
| 2024-08-27 20:08:31 +0200 | <mauke> | unfortunately it seems you can't inject variables from a pattern into the surrounding scope :-) |
| 2024-08-27 20:08:52 +0200 | <mauke> | Main = \argv -> do ... |
| 2024-08-27 20:12:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 20:12:52 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 20:14:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: there's no work on defining adjoint folds in haskell right? |
| 2024-08-27 20:21:11 +0200 | <[exa]> | mauke: perhaps it could interact with record wildcards? these kinda inject stuff |
| 2024-08-27 20:23:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2024-08-27 20:23:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 20:23:23 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 20:27:07 +0200 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2024-08-27 20:27:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-08-27 20:27:50 +0200 | zero | yin |
| 2024-08-27 20:30:05 +0200 | <monochrom> | mauke: That's the job of dynamic scoping and implicit parameters, right? >:) |
| 2024-08-27 20:30:37 +0200 | Square | (~Square@user/square) |
| 2024-08-27 20:35:45 +0200 | danse-nr3 | (~danse-nr3@user/danse-nr3) () |
| 2024-08-27 20:37:37 +0200 | Square | (~Square@user/square) (Ping timeout: 248 seconds) |
| 2024-08-27 20:38:05 +0200 | <dmj`> | Franciman: there's at least two good blog posts on desugaring, and then there's source |
| 2024-08-27 20:38:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 20:38:38 +0200 | <Franciman> | the source is not a formal semantics |
| 2024-08-27 20:38:46 +0200 | <Franciman> | I shall look up the blog posts, thanks dmj` ! |
| 2024-08-27 20:39:12 +0200 | <[exa]> | (==> blog posts are formal semantics) |
| 2024-08-27 20:39:26 +0200 | <Franciman> | lol, they may contain a formal semantics |
| 2024-08-27 20:39:40 +0200 | <Franciman> | it would be fun if a formal semantics wuold be considerd so only if presented on a specific medium |
| 2024-08-27 20:39:42 +0200 | <Franciman> | what would it be? |
| 2024-08-27 20:39:50 +0200 | <monochrom> | Code is as formal as one can get. You can call it unusable but you can't call it informal. |
| 2024-08-27 20:39:50 +0200 | <Franciman> | i imagine an ancient papir |
| 2024-08-27 20:40:03 +0200 | <[exa]> | journal of formal semantics |
| 2024-08-27 20:40:09 +0200 | <Franciman> | monochrom: then what's the point of formal semantics if we just can use code? |
| 2024-08-27 20:40:11 +0200 | <Franciman> | lol |
| 2024-08-27 20:40:13 +0200 | <Franciman> | cringe af |
| 2024-08-27 20:40:14 +0200 | <[exa]> | (coincides much with ancient paper, yes) |
| 2024-08-27 20:40:25 +0200 | <monochrom> | The problem with average programmers is not that they don't know any formal language but rather they know only one, their coding language. |
| 2024-08-27 20:40:25 +0200 | <Franciman> | so GCC is formalized |
| 2024-08-27 20:40:57 +0200 | <Franciman> | let us use GCC to formally reason about C |
| 2024-08-27 20:41:04 +0200 | <Franciman> | ja hoor |
| 2024-08-27 20:41:09 +0200 | <monochrom> | I already implied the answer. One wants a more usable, higher-level formal language. |
| 2024-08-27 20:41:15 +0200 | ars23 | (~ars23@79.113.95.110) |
| 2024-08-27 20:41:31 +0200 | ars23 | (~ars23@79.113.95.110) (Changing host) |
| 2024-08-27 20:41:31 +0200 | ars23 | (~ars23@user/ars23) |
| 2024-08-27 20:42:25 +0200 | <Franciman> | monochrom: there is a tiny issue in your reasoning. Circularity |
| 2024-08-27 20:42:28 +0200 | <Franciman> | ghc is written in haskell |
| 2024-08-27 20:42:37 +0200 | <Franciman> | what's ghc code semantics |
| 2024-08-27 20:42:52 +0200 | <Franciman> | if you are trying to understand haskell's semantics? |
| 2024-08-27 20:43:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-08-27 20:43:03 +0200 | <Franciman> | you must go back to the first bootstrappable version of ghc |
| 2024-08-27 20:43:08 +0200 | <Franciman> | and study its semantics |
| 2024-08-27 20:43:12 +0200 | <monochrom> | There is no circle if you include versioning. |
| 2024-08-27 20:43:14 +0200 | <haskellbridge> | <thirdofmay18081814goya> system hw |
| 2024-08-27 20:43:47 +0200 | <Franciman> | so this all boils down to: yes, haskell has a formal semantics, but to make sense of it, you must know GCC |
| 2024-08-27 20:43:53 +0200 | <Franciman> | and its a huge piece of software |
| 2024-08-27 20:43:56 +0200 | <Franciman> | but hey we got formal semantics ;) |
| 2024-08-27 20:43:58 +0200 | <monochrom> | I did say unusable. |
| 2024-08-27 20:44:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> * fw |
| 2024-08-27 20:44:22 +0200 | <dmj`> | Franciman: some people tried porting Core to Gallina, and then proving things there, but the "formalization gap" is known |
| 2024-08-27 20:44:37 +0200 | <monochrom> | Just showing you that requiring "formal" alone is not good enough. |
| 2024-08-27 20:44:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-08-27 20:44:56 +0200 | <monochrom> | The same way a lot of people here used to talk about "building a community". |
| 2024-08-27 20:45:10 +0200 | <probie> | Outside of SML (and maybe things like Dafny), which languages even have a formal semantics? |
| 2024-08-27 20:45:28 +0200 | <Franciman> | scheme too, and i'm not aware of other |
| 2024-08-27 20:45:30 +0200 | <monochrom> | The best way to build a community is mutual congratulation. Clearly no one actually wants that. |
| 2024-08-27 20:45:44 +0200 | <Franciman> | you are the first to not want that, monochrom |
| 2024-08-27 20:45:46 +0200 | <haskellbridge> | <thirdofmay18081814goya> why is system fw not good enough? there's even formalizations in coq |
| 2024-08-27 20:48:00 +0200 | <haskellbridge> | <thirdofmay18081814goya> often all you need to make convincing proofs is a small subset anyways |
| 2024-08-27 20:48:37 +0200 | <monochrom> | The same way a decade ago math people on IRC were dreaming of IRC clients that could render inline LaTeX. |
| 2024-08-27 20:48:52 +0200 | <monochrom> | Such a client actually existed during their time. It's Pidgin. |
| 2024-08-27 20:49:10 +0200 | <monochrom> | And of course the people were like "no that doesn't count". |
| 2024-08-27 20:49:42 +0200 | <monochrom> | And the same way https://ro-che.info/ccc/26 |
| 2024-08-27 20:49:53 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-08-27 20:49:55 +0200 | <monochrom> | Moving goalposts. |
| 2024-08-27 20:50:06 +0200 | <Franciman> | you are not making sense |
| 2024-08-27 20:50:24 +0200 | <monochrom> | Sure. But I'm also done. |
| 2024-08-27 20:50:29 +0200 | <Franciman> | thank god |
| 2024-08-27 20:50:33 +0200 | <[exa]> | monochrom: rofl the comic |
| 2024-08-27 20:50:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
| 2024-08-27 20:50:55 +0200 | <Franciman> | nobody here is requiring haskell to have formal semantics |
| 2024-08-27 20:51:06 +0200 | <Franciman> | i just asked whether there is a specification of how haskell is translated tocore |
| 2024-08-27 20:51:12 +0200 | <Franciman> | and you say ghc is the only specification |
| 2024-08-27 20:51:14 +0200 | <Franciman> | ok |
| 2024-08-27 20:51:43 +0200 | <Franciman> | and i ask you if I have a formal system to reason about ghc's code |
| 2024-08-27 20:51:49 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3205-4b2a-98fd-e867-2c7e-b6f1.rev.sfr.net) |
| 2024-08-27 20:51:50 +0200 | <Franciman> | and you say that you can just go back to previous versions |
| 2024-08-27 20:52:07 +0200 | <Franciman> | ok |
| 2024-08-27 20:52:08 +0200 | <[exa]> | Franciman: for the core haskell it's super easy, you just take any from the lambda calculi if it works. For the non-core, did you ever try to make a formal semantics for anything that is allowed to touch computer memory? |
| 2024-08-27 20:52:23 +0200 | <Franciman> | I am not requiring it |
| 2024-08-27 20:52:28 +0200 | <Franciman> | i'm just pondering monochrom's answer as nonsense |
| 2024-08-27 20:52:33 +0200 | <Franciman> | it's ok to not have it |
| 2024-08-27 20:52:44 +0200 | <Franciman> | i think 0.1% of PLs have a formal semantics |
| 2024-08-27 20:52:48 +0200 | <dmj`> | Franciman: its a touchy subject here |
| 2024-08-27 20:53:04 +0200 | Square | (~Square@user/square) |
| 2024-08-27 20:53:28 +0200 | <dmj`> | there's efforts though |
| 2024-08-27 20:53:30 +0200 | <dmj`> | https://www.cis.upenn.edu/~sweirich/talks/dsw18.pdf |
| 2024-08-27 20:53:41 +0200 | <Franciman> | what you feel hurt haskell doesn't have formal semantics? |
| 2024-08-27 20:53:51 +0200 | <Franciman> | well to quote monochrom USABLE formal semantics |
| 2024-08-27 20:53:54 +0200 | <Franciman> | or whatever else they mean |
| 2024-08-27 20:54:00 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 20:54:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> personally i feel hurt in my little feelings but that's just me |
| 2024-08-27 20:54:15 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Client Quit) |
| 2024-08-27 20:54:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> also just use system fw |
| 2024-08-27 20:54:28 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-08-27 20:54:38 +0200 | <Franciman> | monochrom: a very simple question for you. Is ghc's code for translating haskell to core bug free? |
| 2024-08-27 20:54:47 +0200 | <Franciman> | is it non-ambigous? |
| 2024-08-27 20:55:00 +0200 | <Franciman> | is there a non-abigous translation to non-ambigous machine code? |
| 2024-08-27 20:55:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> how can machine code be ambiguous |
| 2024-08-27 20:56:06 +0200 | <Franciman> | also monochrom, you say you can go back in time. Is any previous version always correct? |
| 2024-08-27 20:56:08 +0200 | <EvanR> | quantum machine code |
| 2024-08-27 20:56:11 +0200 | <Franciman> | or should i stop at some point? |
| 2024-08-27 20:56:16 +0200 | <Franciman> | well branch prediction and stuff |
| 2024-08-27 20:56:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: huh |
| 2024-08-27 20:56:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> quantum ghc when |
| 2024-08-27 20:56:48 +0200 | <EvanR> | we already have quantum computing monads |
| 2024-08-27 20:56:50 +0200 | <Franciman> | so many unanswered questions here, and you speak about moving the goalpost |
| 2024-08-27 20:56:52 +0200 | <Franciman> | SURE monochrom SURE |
| 2024-08-27 20:56:55 +0200 | <Franciman> | you are making TONS OF SENSE |
| 2024-08-27 20:57:08 +0200 | <Franciman> | always with your prejudice against me |
| 2024-08-27 20:57:10 +0200 | <Franciman> | i'm over this |
| 2024-08-27 20:57:35 +0200 | <EvanR> | is this what will happen when I go back to coffee at some point |
| 2024-08-27 20:58:26 +0200 | <[exa]> | lol |
| 2024-08-27 20:58:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> i don't know i forgot what a normal reaction to an issue about haskell semantics was |
| 2024-08-27 20:58:39 +0200 | <Franciman> | monochrom has strong prejudice against me and keeps answering in sarcastic and teasing ways |
| 2024-08-27 20:58:41 +0200 | <Franciman> | i'm over this |
| 2024-08-27 20:58:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 20:58:50 +0200 | <Franciman> | i can't stand it anymore |
| 2024-08-27 20:59:12 +0200 | <EvanR> | sir this is the internet |
| 2024-08-27 20:59:29 +0200 | <Franciman> | so i should expect being made fun of in the haskell community? |
| 2024-08-27 20:59:31 +0200 | <Franciman> | ok, thanks |
| 2024-08-27 21:00:02 +0200 | <yin> | aw. we're the haskell community |
| 2024-08-27 21:00:13 +0200 | <Franciman> | if i know it beforehand, i can adjust of course |
| 2024-08-27 21:00:31 +0200 | <EvanR> | the haskell report explains how to convert rich haskell to core haskell |
| 2024-08-27 21:00:33 +0200 | <Franciman> | yin: this channel is not part of the haskell community? |
| 2024-08-27 21:00:50 +0200 | <probie> | It's part of, but not the entire community |
| 2024-08-27 21:00:51 +0200 | <mauke> | I don't see the sarcasm |
| 2024-08-27 21:00:57 +0200 | <Franciman> | still a part |
| 2024-08-27 21:00:58 +0200 | <haskellbridge> | <thirdofmay18081814goya> no it is an extremist cell |
| 2024-08-27 21:01:04 +0200 | <EvanR> | hahahhaha |
| 2024-08-27 21:01:08 +0200 | <yin> | Franciman: yes i think so. that makes you also a part of the haskell community |
| 2024-08-27 21:01:16 +0200 | <EvanR> | we lie low biding our time |
| 2024-08-27 21:01:40 +0200 | <Franciman> | and according to EvanR it's ok to be sarcastic and teasing to others here |
| 2024-08-27 21:01:41 +0200 | <EvanR> | until the final battle against imperative programming |
| 2024-08-27 21:01:47 +0200 | <haskellbridge> | <thirdofmay18081814goya> _the implementation of functional programming languages_ has a section on converting miranda to lambda calculi |
| 2024-08-27 21:01:50 +0200 | <probie> | This IRC channel probably skews towards "old and bitter" more than other parts of the community |
| 2024-08-27 21:01:59 +0200 | <Franciman> | i just have to know that |
| 2024-08-27 21:02:06 +0200 | <Franciman> | i can start being sarcastic all the time too |
| 2024-08-27 21:02:07 +0200 | <mauke> | I don't think that's right |
| 2024-08-27 21:02:15 +0200 | <yin> | thirdofmay18081814giya: what would an example of extremist haskell opinion be? |
| 2024-08-27 21:02:18 +0200 | <Franciman> | like monochrom does to me |
| 2024-08-27 21:02:26 +0200 | <Franciman> | with their teasing answers |
| 2024-08-27 21:02:28 +0200 | <mauke> | also, can anyone explain to me which part was sarcasm? |
| 2024-08-27 21:02:32 +0200 | <mauke> | and/or teasing |
| 2024-08-27 21:02:37 +0200 | <[exa]> | +1 ^ |
| 2024-08-27 21:02:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-08-27 21:02:39 +0200 | <Franciman> | the whole goalmoving thing |
| 2024-08-27 21:02:41 +0200 | <monochrom> | Yeah that's false accusation. |
| 2024-08-27 21:02:45 +0200 | <Franciman> | the parallel with my question |
| 2024-08-27 21:02:47 +0200 | <Franciman> | and the pidgin thing |
| 2024-08-27 21:02:50 +0200 | <mauke> | what |
| 2024-08-27 21:02:58 +0200 | <Franciman> | read the scrollback |
| 2024-08-27 21:03:04 +0200 | <EvanR> | I tried, it's too long |
| 2024-08-27 21:03:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> yin: you only need conjugate hylomorphisms because all other recursion schemes are an instance of it |
| 2024-08-27 21:03:07 +0200 | <EvanR> | you sound crazy right now |
| 2024-08-27 21:03:11 +0200 | <[exa]> | I'd suggest we start over |
| 2024-08-27 21:03:14 +0200 | <mauke> | I will, but I remember what the pidgin part was about, and I don't see it |
| 2024-08-27 21:03:20 +0200 | <Franciman> | i will, but monochrom won't |
| 2024-08-27 21:03:20 +0200 | <yin> | :0 |
| 2024-08-27 21:03:25 +0200 | <Franciman> | they keep interacting with me in that way |
| 2024-08-27 21:03:28 +0200 | <Franciman> | and i can't stand it |
| 2024-08-27 21:05:09 +0200 | <mauke> | yeah, still don't see it |
| 2024-08-27 21:06:06 +0200 | Square | (~Square@user/square) (Ping timeout: 246 seconds) |
| 2024-08-27 21:06:12 +0200 | <yin> | Franciman: /ignore is a very useful IRC command. i'm considering using it as we speek |
| 2024-08-27 21:06:33 +0200 | <yin> | if someone is bothering you, there's no reason not to use it |
| 2024-08-27 21:06:34 +0200 | <haskellbridge> | <thirdofmay18081814goya> yin: typed lambda calculus is enough to model interesting properties of haskell |
| 2024-08-27 21:07:05 +0200 | <Franciman> | yin: you're right, thanks |
| 2024-08-27 21:07:07 +0200 | <mauke> | to me, monochrom's comments boil down to "you have unstated assumptions/requirements" |
| 2024-08-27 21:07:08 +0200 | <yin> | thirdofmay18081814giya: but we need a superior type system for recursion |
| 2024-08-27 21:07:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> told you, extreme |
| 2024-08-27 21:08:21 +0200 | <[exa]> | Franciman: btw just curious, what would you want to prove using the semantics? |
| 2024-08-27 21:08:30 +0200 | <yin> | thirdofmay18081814giya: we might discover that the extremist cell is actually a majority |
| 2024-08-27 21:08:46 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 21:08:59 +0200 | neuroevolutus | (~neuroevol@146.70.211.152) |
| 2024-08-27 21:09:01 +0200 | <Franciman> | [exa]: mostly have a sound compiler for haskell |
| 2024-08-27 21:09:17 +0200 | <haskellbridge> | <thirdofmay18081814goya> yin: but uh just make it recurse 10000 times and if it has no fixpoint by then just say it is bottom |
| 2024-08-27 21:09:27 +0200 | <Franciman> | to reason about Hoare Triples in haskell |
| 2024-08-27 21:09:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> and a few zeroes if the data structure is big |
| 2024-08-27 21:09:36 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
| 2024-08-27 21:09:45 +0200 | <[exa]> | Franciman: do you have some closer definition of the soundness? normally that's a property of logic systems, not compilers |
| 2024-08-27 21:09:57 +0200 | <EvanR> | 10,000 isn't enough when the recursion is used to implement a game loop, unless the game is turn based and has a turn limit |
| 2024-08-27 21:10:01 +0200 | <probie> | What even is Haskell? Haskell98? Haskell2010? Whatever GHC supports? |
| 2024-08-27 21:10:19 +0200 | <mauke> | does Core have semantics? |
| 2024-08-27 21:10:23 +0200 | <Franciman> | yes it does |
| 2024-08-27 21:10:27 +0200 | <Franciman> | not completely but it does |
| 2024-08-27 21:10:47 +0200 | <Franciman> | [exa]: it means it doesn't produce invalid outcomes, basically |
| 2024-08-27 21:10:56 +0200 | <Franciman> | so whatever evaluation happens, it respects the semantics |
| 2024-08-27 21:11:07 +0200 | <yin> | yes, but what even _is_ Haskell? *strokes beard* |
| 2024-08-27 21:11:30 +0200 | <Franciman> | yes that's the qeustion |
| 2024-08-27 21:11:35 +0200 | <yin> | haskell is a feeling inside |
| 2024-08-27 21:11:37 +0200 | <Franciman> | so pinpointing a ghc version could help |
| 2024-08-27 21:11:38 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: just play really fast and reduce the fps so you can prove your theorem before the recursion ends |
| 2024-08-27 21:11:46 +0200 | kaol | (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
| 2024-08-27 21:11:52 +0200 | <dmj`> | probie: back in my day, foldl' was still in Data.List |
| 2024-08-27 21:11:57 +0200 | <[exa]> | Franciman: ok we're getting somewhere. the "invalid" you mean as in that "bottom" (error/infinite loop/etc) does not happen when it shouldn't? or something else? |
| 2024-08-27 21:12:27 +0200 | <[exa]> | yin: haskell are many |
| 2024-08-27 21:13:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-08-27 21:14:06 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 244 seconds) |
| 2024-08-27 21:15:07 +0200 | <Franciman> | [exa]: that is the point i was trying to clarify for me. For me it is difficult to now say what it means to be sound wrt to haskell semantics |
| 2024-08-27 21:15:13 +0200 | <Franciman> | monochrom said we have a formal semantics |
| 2024-08-27 21:15:20 +0200 | Square | (~Square@user/square) |
| 2024-08-27 21:15:35 +0200 | <Franciman> | but how do I express the soundness of my method wrt this formal semantics that they are trying to refer to? |
| 2024-08-27 21:15:56 +0200 | <Franciman> | apparently it's not enough to read ghc code |
| 2024-08-27 21:16:06 +0200 | <Franciman> | you have to run GHC to make the formal semantics appear |
| 2024-08-27 21:16:52 +0200 | <haskellbridge> | <thirdofmay18081814goya> as a wise man once said the semantics can't be said, it must be seen |
| 2024-08-27 21:19:03 +0200 | <mauke> | IIRC monochrom just said we technically have a formal translation from haskell to core in the form of ghc code. is that the same as a semantics? |
| 2024-08-27 21:19:41 +0200 | <Franciman> | according to them yes |
| 2024-08-27 21:19:53 +0200 | <[exa]> | Franciman: ah. so the issue is that if you try to produce semantics for the whole haskell you're probably going to get something so complex that any nontrivial proof in that is going to be undecidable |
| 2024-08-27 21:20:16 +0200 | <Franciman> | i don't know [exa], sorry |
| 2024-08-27 21:20:19 +0200 | mauke | shrugs |
| 2024-08-27 21:20:28 +0200 | <dmj`> | thought we only had operational semantics, not denotational semantics. I think laziness makes it more difficult too |
| 2024-08-27 21:20:29 +0200 | <[exa]> | (because of the many usual problems of enumerability; e.g. if you didn't see Rice's theorem, please have a look) |
| 2024-08-27 21:20:57 +0200 | <Franciman> | thanks |
| 2024-08-27 21:21:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> Franciman: why can't you use polymorphic lambda calculus? what do you want to model for which this isn't enough? |
| 2024-08-27 21:21:23 +0200 | <[exa]> | Franciman: at that point the ghc's source _is_ a valid resource w.r.t. the complexity (which is sufficiently low there so that you can at leat run it and observe the results) |
| 2024-08-27 21:21:59 +0200 | <Franciman> | thirdofmay, because haskell is more practical |
| 2024-08-27 21:22:00 +0200 | <[exa]> | Franciman: btw for a simpler project, have a look at MicroHS, the source there is super small compared to GHC and might get you something much closer to math |
| 2024-08-27 21:22:04 +0200 | <Franciman> | thanks |
| 2024-08-27 21:22:07 +0200 | <Franciman> | i will try that |
| 2024-08-27 21:23:28 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-08-27 21:24:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 21:25:08 +0200 | <[exa]> | Franciman: anyway for proving anything practical, you will likely have to consider the syntax to core translation basically as a macro system, with the most formal definitions available spilled over the GHC's source again (unfortunately) |
| 2024-08-27 21:25:50 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-08-27 21:26:24 +0200 | <[exa]> | spoiler: proving things about the frontend of a compiler is usually an effort in vain, it's too hairy. I'd start with core and just triplecheck with simpler methods that your program gives the expected Core after passing through the frontend |
| 2024-08-27 21:27:51 +0200 | <Franciman> | yeah so indeed you have to run ghc |
| 2024-08-27 21:27:55 +0200 | <Franciman> | makes sense, ok |
| 2024-08-27 21:28:20 +0200 | ss4 | (~wootehfoo@user/wootehfoot) (Ping timeout: 255 seconds) |
| 2024-08-27 21:28:23 +0200 | <Franciman> | ty |
| 2024-08-27 21:28:53 +0200 | <[exa]> | Franciman: you might have luck with constructing a very small compiler frontend tht just fits your program and is (somehow provably) a strict subset of ghc |
| 2024-08-27 21:29:19 +0200 | <[exa]> | but yeah it's not super easy, that's why people tend to ignore this |
| 2024-08-27 21:29:26 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-08-27 21:29:44 +0200 | <Franciman> | so monochrom what was your point? |
| 2024-08-27 21:29:46 +0200 | <Franciman> | Can i know? |
| 2024-08-27 21:30:02 +0200 | <Franciman> | or are you so elevated for me to understand it |
| 2024-08-27 21:30:21 +0200 | <dmj`> | [exa]: typeclasses alone are very complicated to implement and prove, much less higher rank types and coercions |
| 2024-08-27 21:30:29 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-08-27 21:30:58 +0200 | <Franciman> | i see |
| 2024-08-27 21:31:03 +0200 | <Franciman> | keeps being very hostile |
| 2024-08-27 21:31:49 +0200 | <[exa]> | Franciman: (spoiler 2: quite many design choices in haskell are an outcome of dodging a forest of undecidability and complexity issues rather than something that people just decided to do because they thought it would be cool. There is a loooooooooooong story behind realizing all of that correctly, specifically see the pre-haskell papers.) |
| 2024-08-27 21:32:22 +0200 | Square | (~Square@user/square) (Remote host closed the connection) |
| 2024-08-27 21:32:47 +0200 | Square | (~Square@user/square) |
| 2024-08-27 21:33:58 +0200 | Square | (~Square@user/square) (Remote host closed the connection) |
| 2024-08-27 21:36:36 +0200 | <[exa]> | Franciman: btw as far as I can see, you were just showed counterexamples to guide your thinking. We do it kinda normally that way with math, it's _often_ more constructive than just spoiling the whole thing. But there both ends are ready for some mental gore; unprepared folk will freak out quite often, esp. if stuff gets involved. |
| 2024-08-27 21:37:45 +0200 | <Franciman> | [exa]: saying that haskell has a formal semantics that you obtain by running ghc |
| 2024-08-27 21:37:47 +0200 | <Franciman> | is very strange |
| 2024-08-27 21:38:02 +0200 | <Franciman> | it's like saying that all software in the world is formally specified, because you just have to run them and their semantics is their output |
| 2024-08-27 21:38:09 +0200 | <[exa]> | dmj`: well at least there are a few papers that show the system in a nice boxed figure :D |
| 2024-08-27 21:38:13 +0200 | <Franciman> | it seemed more like trying to turn tables |
| 2024-08-27 21:38:18 +0200 | <haskellbridge> | <thirdofmay18081814goya> Franciman: it's called operational semantics |
| 2024-08-27 21:38:54 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 244 seconds) |
| 2024-08-27 21:39:15 +0200 | <haskellbridge> | <thirdofmay18081814goya> in this sense yeah all programming languages are formally specified |
| 2024-08-27 21:39:16 +0200 | <[exa]> | Franciman: technically it's right, it's _some_ semantics, and it's ready and interpretable. Utility for various purposes might vary. |
| 2024-08-27 21:39:34 +0200 | <Franciman> | okay, i will accept this |
| 2024-08-27 21:39:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 21:40:27 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 21:41:04 +0200 | <[exa]> | Franciman: there's not a single "semantics" for anything, you can have many sensible ones and you can even automatically generate infinite incompatible ones for any system that can do numbers. The average levels of utility are quite low tho; good semantics take effort to develop (or find). |
| 2024-08-27 21:42:37 +0200 | <[exa]> | Franciman: ...so I kinda assume you came here expecting the happy kind of semantics that Just Answers hard questions (which might not ever exist for the general case). |
| 2024-08-27 21:43:15 +0200 | <[exa]> | Franciman: btw not sure if you had a look but there's the seL4 formal validation effort, which is a nice view of how all the issues have to be dodged |
| 2024-08-27 21:43:47 +0200 | <[exa]> | not really related to haskell but it's educative |
| 2024-08-27 21:44:11 +0200 | <dmj`> | [exa]: lmao |
| 2024-08-27 21:44:20 +0200 | <dmj`> | q.e.d |
| 2024-08-27 21:44:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-08-27 21:44:51 +0200 | <haskellbridge> | <thirdofmay18081814goya> [exa]: dodged only until chatgpt learns lean 4 |
| 2024-08-27 21:45:09 +0200 | <fr33domlover> | o/ If an IORef has 1 writer and multiple concurrent readers - does the writer need to use `atomicModifyIORef` ? Or does the non-atomic version work just as well? |
| 2024-08-27 21:45:44 +0200 | <[exa]> | dmj`: like, the typeclasses ain't that super hard, there's the THIH system which kinda does it for most folks, and the pluggy OutsideIn which does everything^TM quite sensibly |
| 2024-08-27 21:47:06 +0200 | <[exa]> | thirdofmay18081814goya: I heard it already knows lean4 tho. where's my semantics. |
| 2024-08-27 21:47:56 +0200 | <jle`> | fr33domlover: i don't think you need to worry about atomicity in that case then yeah |
| 2024-08-27 21:48:11 +0200 | <[exa]> | fr33domlover: I'd say no (the docs has a code sample that would work with a single writer even without the "atomic block") |
| 2024-08-27 21:48:13 +0200 | <haskellbridge> | <thirdofmay18081814goya> [exa]: it literally just learned it last month give it a sec |
| 2024-08-27 21:48:31 +0200 | <Franciman> | [exa]: ah i didn't know seL4, i will llook it up |
| 2024-08-27 21:48:36 +0200 | <Franciman> | ty again |
| 2024-08-27 21:49:02 +0200 | <[exa]> | Franciman: btw just curious, did you get any formal introduction to complexity/enumerability? |
| 2024-08-27 21:49:19 +0200 | <Franciman> | yes |
| 2024-08-27 21:50:09 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 248 seconds) |
| 2024-08-27 21:50:30 +0200 | <fr33domlover> | Thanks jle` , [exa] :) |
| 2024-08-27 21:50:42 +0200 | <[exa]> | ok so you may imagine that it's possible to encode some Godel shenanigans into any layer of ghc, right. :D |
| 2024-08-27 21:50:46 +0200 | <[exa]> | Franciman: ^ |
| 2024-08-27 21:50:51 +0200 | <Franciman> | yes |
| 2024-08-27 21:52:43 +0200 | <[exa]> | fr33domlover: from the other side, it would certainly be very weird to have stuff like a half-modified integer or pointer there or so, like you'd get in C's with "non-atomic write"s etc. AFAIK there is a pointer which has to be switched atomically everytime because of how the runtime works |
| 2024-08-27 21:52:52 +0200 | <monochrom> | fr33domlover: IIRC the docs actually explain a freak (IMO) scenerio where you need the atomic one as soon as the writer and the reader are in different threads. |
| 2024-08-27 21:53:13 +0200 | <mauke> | fr33domlover: as long as https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-IORef.html#memmodel is not a concern |
| 2024-08-27 21:53:42 +0200 | <mauke> | the issue is not a "half write", but re-ordering with other reads/writes from other threads |
| 2024-08-27 21:54:08 +0200 | <monochrom> | Yeah, that. |
| 2024-08-27 21:54:49 +0200 | <tomsmeding> | a half write might still be an issue on some platforms, though. |
| 2024-08-27 21:55:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 21:55:31 +0200 | <mauke> | tomsmeding: not according to the documentation |
| 2024-08-27 21:56:17 +0200 | <tomsmeding> | hm, I guess a "half write" would be bad news for the GC as well |
| 2024-08-27 21:56:19 +0200 | <dmj`> | [exa]: the THIH isn't as simple as it lets on imho, and the inference implementation is a little quirky. OutsideIn(x) doesn't really explain how to implement entailment for typeclasses, and it also breaks let generalization. TF and GADTs now require MonoLocalBinds. |
| 2024-08-27 21:57:38 +0200 | <dmj`> | [exa]: it's not clear how to transition from THIH unification to the HM(x) constrain gen + solving approach, but that's something I'm looking into |
| 2024-08-27 21:58:01 +0200 | Fooo | (~Square@user/square) |
| 2024-08-27 21:59:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 22:00:18 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-08-27 22:02:09 +0200 | alexherbo2 | (~alexherbo@2a02-8440-3205-4b2a-98fd-e867-2c7e-b6f1.rev.sfr.net) (Remote host closed the connection) |
| 2024-08-27 22:03:09 +0200 | <dmj`> | [exa]: it would be very nice to have a rebooted THIH that used HM(x), omitting existentials / higher rank types + GADTs |
| 2024-08-27 22:03:53 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-08-27 22:04:29 +0200 | <haskellbridge> | <Bowuigi> Is the row types paper saga enough to clarify how entailment works? |
| 2024-08-27 22:04:43 +0200 | <haskellbridge> | <Bowuigi> No mention of typeclasses, but it should do |
| 2024-08-27 22:04:46 +0200 | <[exa]> | tomsmeding: yeah, the logic is that other thread's GCs presence kinda forces it to behave well even without atomic* |
| 2024-08-27 22:04:55 +0200 | <[exa]> | dmj`: yeah I know |
| 2024-08-27 22:05:44 +0200 | <[exa]> | what's the actual typesystem of MicroHS btw? there's wild stuff implemented in that one |
| 2024-08-27 22:06:26 +0200 | <haskellbridge> | <Bowuigi> dmj` Also is going bidirectional a bad idea in the context of THIH? It seems to give easier to digest specs |
| 2024-08-27 22:06:45 +0200 | AlexZenon | (~alzenon@178.34.150.250) (Ping timeout: 248 seconds) |
| 2024-08-27 22:09:36 +0200 | <fr33domlover> | mauke, monochrom: In what way can the re-ordering cause damage? Like, if thread A writes, and thread B reads a second later, thread B might receive the old value from before the write? |
| 2024-08-27 22:09:45 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 22:10:21 +0200 | <fr33domlover> | I mean how big can that gap me (if I'm understanding correctly what re-ordering does) |
| 2024-08-27 22:10:22 +0200 | <monochrom> | It involves two IORef. |
| 2024-08-27 22:10:33 +0200 | AlexZenon | (~alzenon@178.34.150.250) |
| 2024-08-27 22:10:53 +0200 | <fr33domlover> | Ah I see |
| 2024-08-27 22:11:34 +0200 | female_student_5 | (~female_st@79.79.255.40) |
| 2024-08-27 22:11:40 +0200 | <female_student_5> | example2 = Apply(Lambda "v" (Variable"w") ) (Apply(Lambda "x"(Apply (Variable "x") (Variable "z")(Variable "y") ))(Variable "l"))) |
| 2024-08-27 22:11:56 +0200 | <female_student_5> | why is this line of code throwing an error |
| 2024-08-27 22:12:04 +0200 | <mauke> | what error |
| 2024-08-27 22:12:10 +0200 | <female_student_5> | says parse on error input and highlights the last bracket |
| 2024-08-27 22:12:15 +0200 | <monochrom> | IMO people shouldn't even write that kind of code, so it's a non-issue to me. |
| 2024-08-27 22:12:21 +0200 | <female_student_5> | im trying to write this: (λv.w) ((λx.(x z y)) l) |
| 2024-08-27 22:12:21 +0200 | <mauke> | time to count brackets, then |
| 2024-08-27 22:12:42 +0200 | <female_student_5> | I have Im still confused |
| 2024-08-27 22:12:55 +0200 | <mauke> | then maybe it's some outer context |
| 2024-08-27 22:13:10 +0200 | <mauke> | does the error still occur with 'example2 = 42'? |
| 2024-08-27 22:13:19 +0200 | neuroevolutus | (~neuroevol@146.70.211.152) (Quit: Client closed) |
| 2024-08-27 22:13:25 +0200 | <tomsmeding> | there are more ) than ( in that line of code |
| 2024-08-27 22:13:39 +0200 | <tomsmeding> | count again ;) |
| 2024-08-27 22:14:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-08-27 22:15:07 +0200 | <tomsmeding> | (also, please fix your spacing, extra or missing spaces everywhere don't make code easier to read) |
| 2024-08-27 22:15:24 +0200 | AlexZenon | (~alzenon@178.34.150.250) (Ping timeout: 246 seconds) |
| 2024-08-27 22:15:45 +0200 | <tomsmeding> | splitting the thing over multiple lines and using some indentation also makes things easier to count: https://paste.tomsmeding.com/bVH0Zsjv |
| 2024-08-27 22:16:03 +0200 | <dmj`> | Bowuigi: Qualified types, theory and practice does mention row types, but I think entailment is specific to superclass and instance detection. THIH has this byInst function that traverses an instance hierarchy by using a limited form of unification called "matching", if a match is found it walks the instance head constraints, with an applied substitution. |
| 2024-08-27 22:16:24 +0200 | AlexZenon | (~alzenon@178.34.150.250) |
| 2024-08-27 22:16:34 +0200 | <mauke> | tomsmeding: eh, that's still lisp-style ))))) soup |
| 2024-08-27 22:16:54 +0200 | <female_student_5> | i want to know what bracket is messing it up |
| 2024-08-27 22:17:36 +0200 | <tomsmeding> | female_student_5: count carefully: start with 0, and with every '(' that you encounter, do +1. For every ')', do -1. You should end with 0 at the end of your line of code |
| 2024-08-27 22:17:43 +0200 | <tomsmeding> | If you don't, then there is some mismatch. :) |
| 2024-08-27 22:18:22 +0200 | <tomsmeding> | many code editors highlight the matching parenthesis if your cursor is on or beside one; this is also quite helpful |
| 2024-08-27 22:18:39 +0200 | Fooo | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-08-27 22:18:45 +0200 | <mauke> | > filter (`elem` "()") "example2 = Apply(Lambda v (Variable w) ) (Apply(Lambda x(Apply (Variable x) (Variable z)(Variable y) ))(Variable l)))" |
| 2024-08-27 22:18:46 +0200 | <lambdabot> | "(())(((()()()))()))" |
| 2024-08-27 22:18:50 +0200 | <tomsmeding> | (if you're using a code editor that does not do this, consider switching to a more full-featured one) |
| 2024-08-27 22:19:30 +0200 | <tomsmeding> | > let s = "(())(((()()()))()))" in (length (filter (== '(')) s, length (filter (== ')')) s) |
| 2024-08-27 22:19:32 +0200 | <lambdabot> | error: |
| 2024-08-27 22:19:32 +0200 | <lambdabot> | • Couldn't match expected type ‘[Char] -> a’ with actual type ‘Int’ |
| 2024-08-27 22:19:32 +0200 | <lambdabot> | • The function ‘length’ is applied to two arguments, |
| 2024-08-27 22:19:43 +0200 | <tomsmeding> | > let s = "(())(((()()()))()))" in (length (filter (== '(') s), length (filter (== ')') s)) |
| 2024-08-27 22:19:44 +0200 | <lambdabot> | (9,10) |
| 2024-08-27 22:19:55 +0200 | <tomsmeding> | (the irony, making a parenthesis-matching error here) |
| 2024-08-27 22:20:32 +0200 | <probie> | > scanl (+) 0 $ map (\x -> if x == '(' then 1 else -1) $ filter (`elem` "()") "example2 = Apply(Lambda v (Variable w) ) (Apply(Lambda x(Apply (Variable x) (Variable z)(Variable y) ))(Variable l)))" |
| 2024-08-27 22:20:34 +0200 | <lambdabot> | [0,1,2,1,0,1,2,3,4,3,4,3,4,3,2,1,2,1,0,-1] |
| 2024-08-27 22:21:10 +0200 | <tomsmeding> | that, but then manually ;) |
| 2024-08-27 22:22:24 +0200 | <female_student_5> | still makes no sense |
| 2024-08-27 22:22:32 +0200 | <female_student_5> | literally just trying to add a simple variable into it |
| 2024-08-27 22:22:35 +0200 | <dmj`> | [exa]: MicroHS exposes the same type system (System FC), but internally it uses a very terse implementation, its the same AST for everything (Type, Constraint, Kind, all are type synonyms on Expr) |
| 2024-08-27 22:22:46 +0200 | <tomsmeding> | female_student_5: did you try to count the '(' and ')' in your line of code? |
| 2024-08-27 22:22:52 +0200 | <female_student_5> | yes but it doesnt help |
| 2024-08-27 22:22:59 +0200 | <tomsmeding> | what numbers did you end up with? |
| 2024-08-27 22:23:00 +0200 | <female_student_5> | because by the logic, im going to change the structure of the original line |
| 2024-08-27 22:23:05 +0200 | <female_student_5> | which is not what I want to do |
| 2024-08-27 22:23:19 +0200 | <mauke> | what did you get? |
| 2024-08-27 22:23:30 +0200 | <female_student_5> | Apply(Lambda "v" (Variable"w")) (Apply(Lambda "x"(Apply (Variable "x") (Variable "z") ))(Variable "l")) - THIS WORKS |
| 2024-08-27 22:23:30 +0200 | michalz | (~michalz@185.246.207.203) (Remote host closed the connection) |
| 2024-08-27 22:23:31 +0200 | <female_student_5> | BUT |
| 2024-08-27 22:23:34 +0200 | <female_student_5> | that is |
| 2024-08-27 22:23:45 +0200 | <female_student_5> | (λv.w) ((λx.(x z)) l) |
| 2024-08-27 22:23:59 +0200 | <female_student_5> | I want it to be: (λv.w) ((λx.(x z y)) l) |
| 2024-08-27 22:24:06 +0200 | <female_student_5> | but I insert the variable y |
| 2024-08-27 22:24:10 +0200 | <female_student_5> | and it causes problems |
| 2024-08-27 22:24:26 +0200 | <mauke> | female_student_5: no, what numbers did you get from your count? |
| 2024-08-27 22:24:36 +0200 | <female_student_5> | the same as you, im telling you, i dont find it helpful |
| 2024-08-27 22:24:44 +0200 | <female_student_5> | because it doesnt help me to tell me where to put the bracket |
| 2024-08-27 22:24:46 +0200 | son0p | (~ff@186.121.18.131) |
| 2024-08-27 22:24:49 +0200 | <female_student_5> | and ive put the brackets everywhere and nothing works |
| 2024-08-27 22:24:54 +0200 | <mauke> | what |
| 2024-08-27 22:25:03 +0200 | <tomsmeding> | female_student_5: https://tomsmeding.com/ss/get/tomsmeding/qIOjny |
| 2024-08-27 22:25:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 22:25:24 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) |
| 2024-08-27 22:25:29 +0200 | <tomsmeding> | green is what is added in your original line of code as compared to the "THIS WORKS" line you posted just now |
| 2024-08-27 22:25:57 +0200 | <tomsmeding> | did you intend to add all three of those things? |
| 2024-08-27 22:26:30 +0200 | <dmj`> | [exa]: MicroHs has the same MonoLocalBinds restriction that GHC has, so no let generalization :( |
| 2024-08-27 22:27:28 +0200 | <female_student_5> | tomsmeding, yes what you posted doesnt work either |
| 2024-08-27 22:27:31 +0200 | <mauke> | female_student_5: the problem is that you have more ')' than '('. the problem is not where to put the extra ')'; the problem is that you have an extra ')' at all |
| 2024-08-27 22:27:41 +0200 | <mauke> | you need to remove it |
| 2024-08-27 22:28:09 +0200 | <tomsmeding> | female_student_5: my screenshot is trying to show you that you have not only added the extra Variable, you have also added a ')' at the end |
| 2024-08-27 22:29:18 +0200 | <female_student_5> | ive put the bracket in 3 different index positions and have event ried without it |
| 2024-08-27 22:29:20 +0200 | <female_student_5> | tried* |
| 2024-08-27 22:29:22 +0200 | <female_student_5> | nothing works |
| 2024-08-27 22:29:31 +0200 | <tomsmeding> | female_student_5: did you read what mauke and I wrote? |
| 2024-08-27 22:29:36 +0200 | <mauke> | yes, but do you get a different error? |
| 2024-08-27 22:29:43 +0200 | <female_student_5> | yes, I feel like none of you are reading what I have wrote |
| 2024-08-27 22:29:50 +0200 | <mauke> | the code you're trying to write is a type error |
| 2024-08-27 22:29:53 +0200 | <tomsmeding> | what error do you get if you just remove the last ) on the line? |
| 2024-08-27 22:29:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 22:30:04 +0200 | <mauke> | the fixes we've suggested only get rid of the parse error |
| 2024-08-27 22:30:28 +0200 | <female_student_5> | I want to adjust this: Apply(Lambda "v" (Variable"w")) (Apply(Lambda "x"(Apply (Variable "x") (Variable "z") ))(Variable "l")) - which is (λv.w) ((λx.(x z)) l) |
| 2024-08-27 22:30:32 +0200 | <female_student_5> | to be (λv.w) ((λx.(x z y)) l) |
| 2024-08-27 22:30:42 +0200 | <tomsmeding> | right |
| 2024-08-27 22:30:46 +0200 | <tomsmeding> | what is the error you're now getting? |
| 2024-08-27 22:30:59 +0200 | <tomsmeding> | it's probably a different one from before |
| 2024-08-27 22:31:05 +0200 | <female_student_5> | None |
| 2024-08-27 22:31:08 +0200 | <female_student_5> | I am asking a question |
| 2024-08-27 22:31:18 +0200 | <female_student_5> | Apply(Lambda "v" (Variable"w")) (Apply(Lambda "x"(Apply (Variable "x") (Variable "z") ))(Variable "l")) - this line does not produce an error |
| 2024-08-27 22:31:33 +0200 | <mauke> | so when you said "nothing works", you mean "it works, there are no errors"? |
| 2024-08-27 22:31:37 +0200 | <mauke> | or what |
| 2024-08-27 22:31:50 +0200 | <female_student_5> | I said it does not produce an error so that means it works |
| 2024-08-27 22:31:58 +0200 | <tomsmeding> | yes, this one works |
| 2024-08-27 22:32:10 +0200 | <female_student_5> | yes so how do I adjust it to make it:(λv.w) ((λx.(x z y)) l) |
| 2024-08-27 22:32:11 +0200 | <tomsmeding> | but your modified line, with the additional Variable, doesn't work -- it gives an error |
| 2024-08-27 22:32:14 +0200 | <tomsmeding> | what error is that? |
| 2024-08-27 22:32:17 +0200 | <mauke> | oh, you're talking about different code again |
| 2024-08-27 22:32:24 +0200 | <tomsmeding> | the error will point you in the right direction |
| 2024-08-27 22:32:31 +0200 | <mauke> | female_student_5: this is super frustrating. you're not directly answering any of our questions |
| 2024-08-27 22:32:42 +0200 | <female_student_5> | mauke ok dont help me then |
| 2024-08-27 22:32:44 +0200 | <tomsmeding> | we're talking past each other here |
| 2024-08-27 22:32:47 +0200 | <female_student_5> | because I find it hard to talk to you |
| 2024-08-27 22:32:49 +0200 | <mauke> | you're always changing the topic, talking about something else, or venting frustration |
| 2024-08-27 22:33:02 +0200 | <tomsmeding> | mauke and I were under the impression that you were still working on the parentheses, and were getting the same parse error |
| 2024-08-27 22:33:15 +0200 | <female_student_5> | mauke, please dont accuse me of stuff, I am using" I feel " statements on purpose |
| 2024-08-27 22:33:20 +0200 | <tomsmeding> | but I now suspect that after you fixed the parse error (by removing the final ')'), you're getting a different error |
| 2024-08-27 22:33:23 +0200 | <female_student_5> | anyway, I am going to leave, this server is not helpful |
| 2024-08-27 22:33:27 +0200 | <dmj`> | Bowuigi: I think it's a great idea, there are actually some places where THIH doesn't infer the most general type, and bidirectional might solve that |
| 2024-08-27 22:33:28 +0200 | female_student_5 | (~female_st@79.79.255.40) () |
| 2024-08-27 22:33:39 +0200 | <tomsmeding> | (ok so much for trying to diagnose communication issues) |
| 2024-08-27 22:33:48 +0200 | ars23 | (~ars23@user/ars23) (Quit: Leaving) |
| 2024-08-27 22:34:07 +0200 | <tomsmeding> | lesson: read your error messages and note when they change |
| 2024-08-27 22:38:29 +0200 | <mauke> | also: don't just say "it doesn't work" (and especially not "nothing works"); ask a specific question and/or show a specific error |
| 2024-08-27 22:38:37 +0200 | <haskellbridge> | <Bowuigi> dmj` I see. So far I have only seen entailment as a way to carry around constraints (mostly from the Gaster and Jones, Leijen 2004 and Hubers 2023 papers), it could be useful for implementing SPTC but you need some "hacks" for it to work |
| 2024-08-27 22:39:35 +0200 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-08-27 22:39:41 +0200 | <mauke> | (the original question, "why is this line of code throwing a [parse] error", was answered fully and directly) |
| 2024-08-27 22:40:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 22:41:19 +0200 | <mauke> | also also: I feel like "this server is not helpful" is an overgeneralization when you've only been talking to two people (out of ~500) on a single channel |
| 2024-08-27 22:42:09 +0200 | <haskellbridge> | <Bowuigi> dmj` Also since Haskell users tend to provide the types of top level bindings, enforcing those and inferring as much as possible with bidirectional type checking should fix some of the problems GHC has had over the years without much pain |
| 2024-08-27 22:42:09 +0200 | <tomsmeding> | I think they were already quite frustrated, are very inexperienced with programming (otherwise the parentheses issue would not have stumped them), and hence also inexperienced with asking help about programming |
| 2024-08-27 22:42:59 +0200 | <tomsmeding> | unfortunately we miscommunicated (not least due to their inexperience in communicating in textual form about this stuff), but if they had persevered, I whink we would have gotten somewhere (at the cost of our wellbeing, possibly) |
| 2024-08-27 22:43:07 +0200 | <dmj`> | Bowuigi: re:entailment, that is actually fair because it can be expanded to encompass row types, not just classes (THIH mentions this extension). So THIH uses `Pred` which is the ||- operator in the theory of qualified types. MPJ thesis does include row types, it can work by adding a row type constructor to `Pred`. |
| 2024-08-27 22:43:46 +0200 | <constxd> | bro you are thinking way too hard about it |
| 2024-08-27 22:43:51 +0200 | ash3en | (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Quit: ash3en) |
| 2024-08-27 22:44:50 +0200 | <constxd> | they were impatient, uncooperative, and ungrateful. plain and simple. who cares that they didn't resolve the problem. good riddance |
| 2024-08-27 22:45:06 +0200 | <mauke> | I do |
| 2024-08-27 22:45:09 +0200 | gentauro | (~gentauro@user/gentauro) |
| 2024-08-27 22:45:15 +0200 | <dmj`> | Bowuigi: entailment in THIH is just superclass detection and instance traversal (byInst, bySuper). |
| 2024-08-27 22:45:37 +0200 | <haskellbridge> | <Bowuigi> Oh so it is already there |
| 2024-08-27 22:45:55 +0200 | <tomsmeding> | constxd: they were. And yet we spent a whole lot of words in miscommunication -- something that I (we) can learn from, at the very least to detect the miscommunication earlier |
| 2024-08-27 22:46:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 22:46:02 +0200 | <haskellbridge> | <Bowuigi> It makes sense, after all, both extensions share similar syntax and origins |
| 2024-08-27 22:46:07 +0200 | <constxd> | you couldn't have made it any clearer than the screenshot of the color-coded diff |
| 2024-08-27 22:46:55 +0200 | <[exa]> | mauke: helping people is hard. |
| 2024-08-27 22:46:56 +0200 | <tomsmeding> | constxd: I think that at that point they had already fixed the parenthesis, but got a different error (a type error due to Apply not taking 3 arguments) |
| 2024-08-27 22:47:10 +0200 | <tomsmeding> | and I suspect that they just didn't notice that the error had _changed_ |
| 2024-08-27 22:47:27 +0200 | <tomsmeding> | hence they didn't tell us that they now had a different problem, hence the miscommunication |
| 2024-08-27 22:47:56 +0200 | athan | (~athan@107.116.47.35) |
| 2024-08-27 22:48:07 +0200 | <dmj`> | Bowuigi: check and infer (for bidirectional) do exist, check is used when you have an explicit type, infer is where you implement a constraint solver and unify to the most general type. For infer you can generate type equality constraints, and entailment constraints w/ meta variables (elaboration) , then you solve the type equality constraints first, accumulating up the substitution, then solving entailment constraints is simplified |
| 2024-08-27 22:49:09 +0200 | <haskellbridge> | <Bowuigi> So synthesis is just a very focused constraint solver? |
| 2024-08-27 22:49:46 +0200 | <dmj`> | Bowuigi: I think row types are simpler to implement than classes, hence why elm and others have them. Rust has classes but I don't think they're as sophisticated |
| 2024-08-27 22:50:31 +0200 | <haskellbridge> | <Bowuigi> I prefer syntax directed specs over constraint-based ones because the first ones are usually clearer, but if they are somehow equivalent then that's helpful |
| 2024-08-27 22:50:39 +0200 | <mauke> | tomsmeding: that makes sense, unfortunately |
| 2024-08-27 22:52:07 +0200 | <haskellbridge> | <Bowuigi> Yes, row types are easier to implement than classes, specially easier MPTC (which requires a full relational solver). Rust only has SPTC, which is way simpler than MPTC |
| 2024-08-27 22:52:30 +0200 | <dmj`> | Bowuigi: yea ideally the elaboration is simple, but the solving becomes difficult as you add new extensions to HM, hence a general framework HM(x) for dealing with this, but I don't think extensions to hindley milner are really composable, nor their proofs |
| 2024-08-27 22:53:53 +0200 | athan | (~athan@107.116.47.35) (Read error: Connection reset by peer) |
| 2024-08-27 22:54:22 +0200 | athan | (~athan@2600:382:2d09:ef51:9785:f8c8:8da1:7865) |
| 2024-08-27 22:54:25 +0200 | <haskellbridge> | <Bowuigi> In fact, Leijen 2004's paper on first class labels implicitly describes how to implement SPTC (or rather, a slightly more powerful version) in row types. You need records, an "any" polymorphic label and "fix" (which may be replaced with another, total form of recursion given some constraints) |
| 2024-08-27 22:54:30 +0200 | <dmj`> | yea in theory MPTC would be simple to implement by extending `Pred` to operate on a list of types, THIH mentions this. THIH is pretty adhoc, people are using minikanren implementations to do constraint solving, the chameleon project kind of did this. It's like a prolog DSL, or you can just use prolog |
| 2024-08-27 22:55:38 +0200 | <haskellbridge> | <Bowuigi> If you add some of the constraints and primitives on Hubers 2023, you get fast generics, which is cool but at the moment I don't know how to compile those as efficiently as in Leijen2004 |
| 2024-08-27 22:57:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 22:57:29 +0200 | <haskellbridge> | <Bowuigi> dmj` re:HM(x) Hindley-Milner only seems to be composable in regards to small-ish extensions to the algorithms (entailment, rank 2 polymorphism, more primitive types, etc), most of the proofs don't carry over sadly |
| 2024-08-27 22:58:28 +0200 | <haskellbridge> | <Bowuigi> That's another reason to prefer syntax directed + bidirectional, which is more easily extensible and proofs are somewhat simpler (plug some extra cases in the main theorems and done) |
| 2024-08-27 22:59:45 +0200 | <haskellbridge> | <Bowuigi> re:MPTC Shen uses a custom prolog implementation for similar purposes (actually it is the whole type system), so it makes sense if you can use miniKanren for it too |
| 2024-08-27 23:01:09 +0200 | <dmj`> | yea using prolog is attractive because you get unification for free |
| 2024-08-27 23:01:55 +0200 | CrunchyFlakes | (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) (Read error: Connection reset by peer) |
| 2024-08-27 23:01:59 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-08-27 23:02:24 +0200 | <EvanR> | constxd, bro that's why this is #haskell and not #team-public-shaming |
| 2024-08-27 23:03:24 +0200 | <haskellbridge> | <thirdofmay18081814goya> is bartosz milewski's category theory for programmers the best resource for category theory in haskell? |
| 2024-08-27 23:03:35 +0200 | <EvanR> | is it even in haskell |
| 2024-08-27 23:03:44 +0200 | <EvanR> | it seems to be just basic category theory |
| 2024-08-27 23:03:49 +0200 | <EvanR> | with art |
| 2024-08-27 23:04:00 +0200 | <EvanR> | and not much programming at all |
| 2024-08-27 23:04:01 +0200 | <dmj`> | Bowuigi: I think once you add higher rank types your constraint solving becomes non-deterministic, hence the "wanteds" and "givens" in OutsideIn(x), but if you topo sort the definitions w/ HM + MPTC + Row types only, constraint solving should be deterministic. |
| 2024-08-27 23:04:10 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: that was my impression too |
| 2024-08-27 23:04:46 +0200 | <EvanR> | I liked this book which is apparently on arxiv https://arxiv.org/abs/1612.09375 |
| 2024-08-27 23:04:58 +0200 | <EvanR> | not much haskell either |
| 2024-08-27 23:04:59 +0200 | <dmj`> | Bowuigi: I'll check out the 2004 Leijen paperr |
| 2024-08-27 23:05:51 +0200 | <EvanR> | perhaps surprisingly for a haskeller, the book doesn't get around to monads |
| 2024-08-27 23:06:20 +0200 | <haskellbridge> | <thirdofmay18081814goya> wish there was less: prove this, more: this is the definition, do things with it |
| 2024-08-27 23:06:40 +0200 | <EvanR> | do things? |
| 2024-08-27 23:06:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-08-27 23:07:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> suddenly "do" |
| 2024-08-27 23:07:49 +0200 | <EvanR> | conal elliott has a few videos of his presentation on compiling via categories |
| 2024-08-27 23:08:06 +0200 | <EvanR> | this is ostensibly doing something |
| 2024-08-27 23:08:34 +0200 | <dmj`> | Bowuigi: do you have a link to your compiler? |
| 2024-08-27 23:10:14 +0200 | <haskellbridge> | <Bowuigi> dmj` re:higher-rank-types another win for bidirectional (given a predicative system), the "Complete and easy bidirectional typechecking for higher-rank polymorphism" paper details this one issue. Another source is "Spine local type inference" which is both more complex and more general, but the main idea is more or less the same |
| 2024-08-27 23:10:53 +0200 | <haskellbridge> | <Bowuigi> Wdym my compiler? |
| 2024-08-27 23:11:48 +0200 | <haskellbridge> | <Bowuigi> I'm designing a lang with these fancy row types but I haven't done much progress outside of that (last topic to decide on was recursion because the lang is total) |
| 2024-08-27 23:12:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 23:12:59 +0200 | <haskellbridge> | <Bowuigi> The initial prototype is probably going to be in Miranda because my computer broke and it works on my phone while being lightweight |
| 2024-08-27 23:13:36 +0200 | <dmj`> | Bowuigi: I'm not really sold on existentials / higher rank types tbh. They block optimizations, complicate inference and you lose decidability. But GHC uses them for typeclasses, exceptions, ST, etc. |
| 2024-08-27 23:14:11 +0200 | <haskellbridge> | <Bowuigi> Wait which optimizations does it block? |
| 2024-08-27 23:14:51 +0200 | <dmj`> | Bowuigi: monomorphization |
| 2024-08-27 23:15:06 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-08-27 23:15:26 +0200 | <haskellbridge> | <Bowuigi> Oh, it may be possible to adapt Lambda Set Specialization to those without much trouble |
| 2024-08-27 23:16:42 +0200 | <dmj`> | Bowuigi: hah, thats exactly what I'm looking into, but that's specifically for defunctionalization, an improvement on reynolds |
| 2024-08-27 23:17:55 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-08-27 23:19:09 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-08-27 23:20:24 +0200 | sw4n | (~sw4n@2605:59c0:40f0:9610:1416:5e9c:d850:b266) |
| 2024-08-27 23:21:34 +0200 | <dmj`> | Bowuigi: Maybe it can work somehow, I just can't see it right now. But, having the lambda set accumulation work with HM(x) would be really cool. |
| 2024-08-27 23:21:52 +0200 | <haskellbridge> | <Bowuigi> And re:category-theory once I understood the basics I watched a video by Richard Southwell (on Youtube) on Limits and now I think I have started to understand this lol. I couldn't get into any book but here are some more honorable mentions: "The Joy of Abstraction" (forgot the name of the author, sorry; very long explanations, probably what I would have tried if I wanted a book), "Category Theory in Context" by... |
| 2024-08-27 23:21:57 +0200 | <haskellbridge> | ... Riehl (assumes you are a mathematician, big brain stuff in there) |
| 2024-08-27 23:22:42 +0200 | <haskellbridge> | <Bowuigi> dmj` after defunctionalization, you don't have any more higher rank functions to worry about so monomorphization can work as usual |
| 2024-08-27 23:22:56 +0200 | <haskellbridge> | <Bowuigi> If I understood them correctly, that is |
| 2024-08-27 23:25:17 +0200 | <haskellbridge> | <Bowuigi> re:category-theory "The Joy of Abstraction" is by Eugenia Cheng, the Topos Institute offers a series of lectures on it as well. And if you happen to like type theory enough, "oo-category theory for undergraduates" is a good resource that covers a lot of topics very quickly |
| 2024-08-27 23:25:38 +0200 | Ptival | (~halloy449@64.16.51.186) |
| 2024-08-27 23:26:00 +0200 | sw4n | (~sw4n@2605:59c0:40f0:9610:1416:5e9c:d850:b266) (Remote host closed the connection) |
| 2024-08-27 23:27:47 +0200 | <dmj`> | I've read quite a few papers on functional compiler implementation and never felt like my understanding was limited by a knowledge of advanced category theory tbh |
| 2024-08-27 23:28:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 23:29:05 +0200 | <Ptival> | been playing with first-class-families, but I can't seem to find an equivalent of `testEquality` to help unblock some type-level computations, is there anything that would look vaguely like `testEquality :: Proxy a -> Proxy b -> Either (TyEqImpl a b :~: 'False) (TyEqImpl a b :~: 'True)`? |
| 2024-08-27 23:29:36 +0200 | <haskellbridge> | <Bowuigi> It intersects with type theory at some point, but other than that it is mostly a tool of thought |
| 2024-08-27 23:29:49 +0200 | <dmj`> | Bowuigi: regarding monomorphization, check this comment by Andras Kovacs https://www.reddit.com/r/haskell/comments/46lux3/comment/d064sts/?utm_source=share&utm_medium=web3… |
| 2024-08-27 23:31:07 +0200 | Ptival | (~halloy449@64.16.51.186) (Changing host) |
| 2024-08-27 23:31:07 +0200 | Ptival | (~halloy449@user/Ptival) |
| 2024-08-27 23:32:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-08-27 23:33:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-08-27 23:35:17 +0200 | <dmj`> | Bowuigi: existential types / higher rank polymorphism, polymorphic recursion all block specialization and therefore monomorphization |
| 2024-08-27 23:36:17 +0200 | <haskellbridge> | <Bowuigi> Oh you mean the one in datatypes, I meant the one in functions |
| 2024-08-27 23:36:30 +0200 | kimiamania2 | (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 2024-08-27 23:36:53 +0200 | <dmj`> | depending on the IR, closures and data types are represented identically, like in GRIN |
| 2024-08-27 23:37:21 +0200 | kimiamania2 | (~65804703@user/kimiamania) |
| 2024-08-27 23:37:40 +0200 | <haskellbridge> | <Bowuigi> Yeah no idea how to handle datatype monomorphization other than duplicating a lot of code |
| 2024-08-27 23:37:59 +0200 | <haskellbridge> | <Bowuigi> Oh wait row types sort of give you an entry point |
| 2024-08-27 23:38:30 +0200 | <dmj`> | code duping is fine if you can do DCE |
| 2024-08-27 23:39:02 +0200 | <haskellbridge> | <Bowuigi> Either Gaster and Jones or Leijen said something about compiling lacks constraints as evidence passing |
| 2024-08-27 23:40:27 +0200 | Guest25 | (~Guest25@176.106.34.161) |
| 2024-08-27 23:41:45 +0200 | <haskellbridge> | <Bowuigi> This evidence is essentially a pointer to the next block of data of the record. It is supposed to be stored as an unboxed tuple so it uses the size of the type as an offset |
| 2024-08-27 23:43:14 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-08-27 23:43:16 +0200 | <haskellbridge> | <Bowuigi> Since every monomorphic type instantiation performed is known before compilation (otherwise the types are ambiguous), you can specialize on both records and variants directly as needed |
| 2024-08-27 23:43:50 +0200 | <dmj`> | is that an alternative to dictionary passing? |
| 2024-08-27 23:44:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-08-27 23:47:17 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 2024-08-27 23:48:00 +0200 | <haskellbridge> | <Bowuigi> Technically, yes |
| 2024-08-27 23:48:04 +0200 | Guest25 | (~Guest25@176.106.34.161) (Quit: Client closed) |
| 2024-08-27 23:48:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-08-27 23:49:09 +0200 | son0p | (~ff@186.121.18.131) (Ping timeout: 248 seconds) |
| 2024-08-27 23:49:15 +0200 | <haskellbridge> | <Bowuigi> But also no, dictionary passing for typeclasses may still need the intersection type encoded by the record and "any" label. This one can be removed via inlining and simple-ish specialization |
| 2024-08-27 23:52:51 +0200 | <dmj`> | yea that static monomorphization for that would be a good alternative, but it would only work with WPC, and disabling polymorphic recursion |
| 2024-08-27 23:53:42 +0200 | <dmj`> | row types shouldn't pose any problem for monomorphization afaict |
| 2024-08-27 23:54:03 +0200 | <haskellbridge> | <Bowuigi> If specializing everything is too much (it definitely is), a SPECIALIZE pragma like in GHC that, when applied to a datatype derives the new sizes automagically, possibly giving you conversion functions with the non-specialized version and when applied to a function creates a shim of intersection type (record and "any" label) that when inlined resolves to either the specialized function(s) or to the polymorphic... |
| 2024-08-27 23:54:08 +0200 | <haskellbridge> | ... one. This one is more complex because you can't mix specialized types with non-specialized functions that easily (unless you do some trickery with evidence maybe), but maybe useful |
| 2024-08-27 23:54:45 +0200 | <haskellbridge> | <Bowuigi> I forgot some commas there (englishn't) but it should be clear enough lol |
| 2024-08-27 23:55:09 +0200 | <dmj`> | is it too much though |
| 2024-08-27 23:55:52 +0200 | <dmj`> | I think caching could help a lot |
| 2024-08-27 23:55:56 +0200 | <haskellbridge> | <Bowuigi> Yup, monomorphizing records and variants is pretty much creating C-style structs and unions respectively as needed |
| 2024-08-27 23:58:18 +0200 | <dmj`> | yea that sounds great, that's what all heap objects become |
| 2024-08-27 23:58:44 +0200 | <dmj`> | but just fewer pointer indirections this time |
| 2024-08-27 23:59:40 +0200 | <haskellbridge> | <Bowuigi> If monomorphization works on the Leijen2004 records, it likely works anywhere else as the main difference is in how they are compiled (w.r.t. constraints and evidence) and the amount of constraints (mostly, the has vs lacks discussion and row concatenation existence or lack thereof) |
| 2024-08-27 23:59:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-08-27 23:59:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |