Logs on 2024-08-27 (liberachat/#haskell)
| 00:01:11 | <Maxdamantus> | I don't think Rust necessarily disables it. I think it just gives up if the stack is too big. |
| 00:01:15 | × | acidjnk_new quits (~acidjnk@p200300d6e72cfb41fdef54b6136c7789.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 00:01:33 | <Maxdamantus> | so you can trigger the same limitation without actual polymorphic recursion. |
| 00:02:49 | <dmj`> | yea, you're right, it just fails at compile time, with a "won't fix" github issue |
| 00:03:21 | <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. |
| 00:04:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:04:51 | <dmj`> | Maxdamantus: that sounds interesting |
| 00:05:17 | <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. |
| 00:06:39 | <Maxdamantus> | (eg, C++'s ABI doesn't support generics/templates aiui, since those always exist in headers and are always expanded at compile time) |
| 00:08:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 00:10:27 | <dmj`> | yea seems like once you go polymorphic recursive you have to forego monomorphization, especially if its unbounded. |
| 00:12:06 | × | ddellacosta quits (~ddellacos@ool-44c73c8f.dyn.optonline.net) (Ping timeout: 246 seconds) |
| 00:12:26 | → | ddellacosta joins (~ddellacos@ool-44c73c8f.dyn.optonline.net) |
| 00:12:40 | <jle`> | it would be cool if TypeAbstraction'd names showed up in the error messages |
| 00:14:52 | <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 |
| 00:15:55 | × | dorin quits (~dorin@user/dorin) (Ping timeout: 256 seconds) |
| 00:18:36 | <dmj`> | Maxdamantus: data monomorphization is the biggest win, I'd love to see how much code breaks w/o polymorphic recursion |
| 00:18:50 | <dmj`> | jle`: hmmm maybe a type checker plugin ? |
| 00:20:08 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:20:10 | <dmj`> | geekosaur: barring polymorphic recursion, it should be possible to inline all instances under WPC |
| 00:20:20 | <geekosaur> | right |
| 00:21:04 | <geekosaur> | hm, although as ghc currently is that presents some problems depending on when that inlining happens |
| 00:21:44 | <geekosaur> | there's at least three bug reports on ghc's tracker that show what happens if IO gets inlined |
| 00:23:37 | <geekosaur> | (all three rejected with "don't do that") |
| 00:24:57 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:25:32 | <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. |
| 00:26:31 | <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? |
| 00:27:05 | <geekosaur> | maybe with some type level trickery which amounts to the same thing |
| 00:27:16 | <dmj`> | there's that contrived example of the infinitely expanding tuple heh |
| 00:29:24 | <dmj`> | sort of looks like (a,a) -> (a,(a,a)) -> (a,(a,(a,a))), but recursively looks like another call to (a,a) |
| 00:30:42 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:31:03 | <geekosaur> | I thought ghc threw an infinite type error for things like that? |
| 00:31:10 | <geekosaur> | a ~ (a,a) |
| 00:33:18 | <Maxdamantus> | dmj`: by data monomorphisation, do you mean lack of a "universal representation" (eg, every generic field/variable is a pointer)? |
| 00:33:33 | <Maxdamantus> | if so, I kind of think of that as a separate thing. |
| 00:34:19 | <geekosaur> | I assumed the point of that was eliminating a lot of pointer chasing by inlining the unboxed versions/operations |
| 00:34:34 | <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, |
| 00:34:36 | <geekosaur> | which you can only do if it's monomorphic |
| 00:35:10 | <dmj`> | geekosaur: I know its possible somehow to do polymorphic recursion w/o typeclass constraints |
| 00:35:58 | <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. |
| 00:39:20 | <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 |
| 00:39:35 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 00:40:32 | <Maxdamantus> | Well, I think that would be solved the same way, but you just have a tracing function for every data type. |
| 00:40:48 | <Maxdamantus> | if the data type is generic, that tracing function is generic. |
| 00:40:53 | × | dtman34 quits (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) (Ping timeout: 248 seconds) |
| 00:41:27 | ← | MattByName parts (~Matthew@user/MattByName) () |
| 00:43:00 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 00:43:15 | → | troojg joins (~troojg@user/troojg) |
| 00:43:27 | <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) |
| 00:47:38 | <dmj`> | yea that could work |
| 00:50:06 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 00:52:40 | <dmj`> | or tracing function could just operate on tag type, byte count and treat all bytes as (void *) |
| 00:54:43 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:56:48 | <Maxdamantus> | but then you're forcing all code to use the suboptimal representation. |
| 00:58:04 | <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. |
| 00:58:48 | <Maxdamantus> | and that's still compatible with a function on `Vec<T>`, which won't be as inlined, but still supports the same representation. |
| 01:00:32 | → | dysthesis joins (~dysthesis@user/dysthesis) |
| 01:05:31 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:06:44 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 01:08:32 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 01:08:37 | <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 |
| 01:10:19 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 01:10:53 | <Maxdamantus> | dmj`: what determines that there's a type tag? does a `Vec<Vec<i32>>` have a tag for each `Vec<i32>`? |
| 01:13:44 | <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. |
| 01:14:07 | <Maxdamantus> | so there shouldn't be a need to store tags in the heap itself. |
| 01:15:53 | <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 |
| 01:17:01 | <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 |
| 01:20:04 | <dmj`> | If you're using the LLVM FFI, the representation wouldn't have overhead |
| 01:20:57 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:20:59 | × | krei-se quits (~krei-se@p57af2d39.dip0.t-ipconnect.de) (Ping timeout: 244 seconds) |
| 01:21:02 | <dmj`> | you might able to alloca w/ Vec<i32> |
| 01:25:32 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:34:36 | → | krei-se joins (~krei-se@p57af29d2.dip0.t-ipconnect.de) |
| 01:35:37 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 01:36:22 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:38:57 | <dmj`> | "clang only" |
| 01:40:55 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:50:42 | → | darkstardevx joins (~darkstard@50.53.3.2) |
| 01:51:47 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 01:56:15 | × | troojg quits (~troojg@user/troojg) (Ping timeout: 276 seconds) |
| 01:56:19 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:04:21 | × | bilegeek quits (~bilegeek@2600:1008:b017:c901:621d:4241:2804:e5ab) (Quit: Leaving) |
| 02:06:35 | × | td_ quits (~td@i53870916.versanet.de) (Ping timeout: 252 seconds) |
| 02:07:12 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:08:35 | → | td_ joins (~td@i53870933.versanet.de) |
| 02:11:44 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 02:18:08 | → | slack1256 joins (~slack1256@2803:c600:5111:8029:d2a9:631a:b025:6268) |
| 02:21:57 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 244 seconds) |
| 02:22:28 | × | poscat quits (~poscat@user/poscat) (Quit: Bye) |
| 02:22:37 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:26:31 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 02:27:01 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 02:30:48 | → | poscat joins (~poscat@user/poscat) |
| 02:34:28 | × | rekahsoft quits (~rekahsoft@bras-base-orllon1103w-grc-02-184-145-10-5.dsl.bell.ca) (Ping timeout: 252 seconds) |
| 02:37:06 | <dmj`> | Maxdamantus: https://llvm.org/docs/LangRef.html#t-vector |
| 02:37:10 | → | drdo1 joins (~drdo@bl5-29-74.dsl.telepac.pt) |
| 02:38:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:39:14 | × | drdo quits (~drdo@bl5-29-74.dsl.telepac.pt) (Ping timeout: 248 seconds) |
| 02:39:14 | drdo1 | is now known as drdo |
| 02:42:36 | → | drdo5 joins (~drdo@bl5-29-74.dsl.telepac.pt) |
| 02:42:37 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 02:43:59 | × | drdo quits (~drdo@bl5-29-74.dsl.telepac.pt) (Ping timeout: 260 seconds) |
| 02:43:59 | drdo5 | is now known as drdo |
| 02:46:21 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 02:53:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 02:58:16 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 02:59:34 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 03:08:53 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:13:55 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds) |
| 03:20:15 | <haskellbridge> | <thirdofmay18081814goya> you have a recursive function that is constant after an unknown number of applications on "x" |
| 03:20:23 | <haskellbridge> | <thirdofmay18081814goya> what's a way to get this value? |
| 03:21:06 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 03:21:56 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 03:24:19 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:24:24 | <dmj`> | use Eq to check if you're at a fixpoint |
| 03:28:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 03:30:44 | <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. |
| 03:31:05 | <Maxdamantus> | (assuming the elements are byte-sized) |
| 03:31:47 | <Maxdamantus> | imagine it would make sense to avoid * |
| 03:39:14 | → | cheater_ joins (~Username@user/cheater) |
| 03:39:44 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 03:39:44 | → | aforemny_ joins (~aforemny@i59F516CA.versanet.de) |
| 03:40:09 | × | cheater quits (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 03:40:19 | cheater_ | is now known as cheater |
| 03:40:37 | × | aforemny quits (~aforemny@i59F516F8.versanet.de) (Ping timeout: 248 seconds) |
| 03:40:40 | × | cheater quits (~Username@user/cheater) (Read error: Connection reset by peer) |
| 03:41:26 | → | cheater_ joins (~Username@user/cheater) |
| 03:41:26 | cheater_ | is now known as cheater |
| 03:44:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 03:55:10 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:00:10 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 04:06:38 | × | slack1256 quits (~slack1256@2803:c600:5111:8029:d2a9:631a:b025:6268) (Remote host closed the connection) |
| 04:07:57 | × | glguy quits (glguy@libera/staff/glguy) (Read error: Connection reset by peer) |
| 04:08:48 | → | glguy joins (glguy@libera/staff/glguy) |
| 04:10:36 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:15:17 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 04:26:01 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:30:42 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 04:41:22 | × | jinsun quits (~jinsun@user/jinsun) () |
| 04:41:27 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 04:46:33 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 04:54:28 | → | michalz joins (~michalz@185.246.207.221) |
| 04:56:52 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:05:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:09:36 | → | neuroevolutus joins (~neuroevol@37.19.200.148) |
| 05:15:56 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:18:39 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 05:20:29 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 05:21:29 | → | michalz joins (~michalz@185.246.207.203) |
| 05:27:09 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 05:30:06 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 05:31:21 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:34:30 | → | Square joins (~Square@user/square) |
| 05:35:50 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 05:36:21 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 05:36:58 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 05:39:45 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:40:07 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 05:41:23 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 05:43:59 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 05:46:01 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 05:46:46 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 05:49:32 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 05:50:47 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 05:51:39 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:54:57 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 05:56:31 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 06:02:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:03:16 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 06:06:11 | → | Square2 joins (~Square4@user/square) |
| 06:06:45 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 06:08:41 | × | Square quits (~Square@user/square) (Ping timeout: 255 seconds) |
| 06:12:54 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 06:17:36 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:21:11 | → | ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 06:21:23 | → | acidjnk_new joins (~acidjnk@p200300d6e72cfb83c8b55ff2a9bbb599.dip0.t-ipconnect.de) |
| 06:22:09 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 06:24:07 | → | akegalj joins (~akegalj@197-208.dsl.iskon.hr) |
| 06:24:43 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b9a0:3dc1:ba12:10da:4091) (Ping timeout: 252 seconds) |
| 06:25:18 | → | jcarpenter2 joins (~lol@2603:3016:1e01:b9a0:f873:c933:3c9b:237a) |
| 06:31:26 | → | Inst joins (~Inst@user/Inst) |
| 06:32:58 | → | CiaoSen joins (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) |
| 06:33:00 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:33:38 | × | neuroevolutus quits (~neuroevol@37.19.200.148) (Quit: Client closed) |
| 06:34:47 | → | kalj joins (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) |
| 06:35:47 | × | kalj quits (~kalj@h-158-174-207-174.NA.cust.bahnhof.se) (Client Quit) |
| 06:38:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 06:41:14 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:45:18 | → | oo_miguel joins (~Thunderbi@78.10.207.45) |
| 06:48:25 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 06:51:01 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 06:53:14 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 07:01:47 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 07:06:40 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 07:18:06 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 07:19:50 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 07:35:55 | → | cfricke joins (~cfricke@user/cfricke) |
| 07:55:58 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:58:57 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 08:04:10 | → | merijn joins (~merijn@77.242.116.146) |
| 08:06:07 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:06:40 | → | ash3en joins (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 08:08:05 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 08:08:54 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 08:09:11 | → | merijn joins (~merijn@77.242.116.146) |
| 08:10:01 | × | dysthesis quits (~dysthesis@user/dysthesis) (Ping timeout: 260 seconds) |
| 08:12:10 | → | dysthesis joins (~dysthesis@user/dysthesis) |
| 08:20:33 | → | sroso joins (~sroso@user/SrOso) |
| 08:25:21 | × | ft quits (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving) |
| 08:25:30 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:37:11 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 08:39:20 | → | gmg joins (~user@user/gehmehgeh) |
| 08:40:59 | × | ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 08:43:16 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 08:46:24 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 08:46:48 | → | ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 08:47:36 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 08:52:27 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 08:53:50 | → | danse-nr3 joins (~danse-nr3@user/danse-nr3) |
| 08:56:38 | gehmehgeh | is now known as gmg |
| 08:56:39 | × | gmg quits (~user@user/gehmehgeh) (Client Quit) |
| 09:00:51 | → | darkstarx joins (darkstarde@gateway/vpn/protonvpn/darkstardevx) |
| 09:03:19 | × | darkstardevx quits (~darkstard@50.53.3.2) (Ping timeout: 260 seconds) |
| 09:09:53 | → | darkstardev13 joins (~darkstard@50.53.3.2) |
| 09:10:50 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:11:02 | gehmehgeh | is now known as gmg |
| 09:12:30 | × | darkstarx quits (darkstarde@gateway/vpn/protonvpn/darkstardevx) (Ping timeout: 246 seconds) |
| 09:14:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:15:51 | → | alexherbo2 joins (~alexherbo@2a02-8440-311b-18ba-98d8-b0b9-f0fb-b020.rev.sfr.net) |
| 09:16:34 | × | alexherbo2 quits (~alexherbo@2a02-8440-311b-18ba-98d8-b0b9-f0fb-b020.rev.sfr.net) (Remote host closed the connection) |
| 09:18:23 | × | CiaoSen quits (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) (Ping timeout: 244 seconds) |
| 09:41:42 | → | CiaoSen joins (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) |
| 09:46:23 | × | Luj9 quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: Ping timeout (120 seconds)) |
| 09:46:40 | → | Luj9 joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 09:58:00 | × | sam113101 quits (~sam@24.157.253.231) (Ping timeout: 246 seconds) |
| 09:58:04 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 09:59:46 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 10:01:29 | × | CiaoSen quits (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 10:01:56 | × | darkstardev13 quits (~darkstard@50.53.3.2) (Quit: Leaving) |
| 10:07:27 | → | __monty__ joins (~toonn@user/toonn) |
| 10:08:57 | × | ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 276 seconds) |
| 10:09:42 | → | ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 10:10:12 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 10:18:07 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 264 seconds) |
| 10:22:17 | → | merijn joins (~merijn@77.242.116.146) |
| 10:28:05 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 10:28:47 | → | merijn joins (~merijn@77.242.116.146) |
| 10:34:21 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 10:40:34 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b9a0:f873:c933:3c9b:237a) (Ping timeout: 260 seconds) |
| 10:41:18 | → | merijn joins (~merijn@77.242.116.146) |
| 10:41:28 | → | jcarpenter2 joins (~lol@96.78.87.197) |
| 10:42:42 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 10:44:33 | × | danse-nr3 quits (~danse-nr3@user/danse-nr3) (Ping timeout: 246 seconds) |
| 11:02:41 | → | rosco joins (~rosco@175.136.158.234) |
| 11:03:41 | <haskellbridge> | <thirdofmay18081814goya> at dmj: ended up doing that, that's pretty much the only solution it seems |
| 11:04:11 | <haskellbridge> | <thirdofmay18081814goya> unrelated: anyone use some recursion scheme in particular regularly? |
| 11:13:47 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 255 seconds) |
| 11:16:04 | × | ash3en quits (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Ping timeout: 272 seconds) |
| 11:16:05 | → | merijn joins (~merijn@77.242.116.146) |
| 11:19:16 | → | CiaoSen joins (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) |
| 11:25:27 | → | ash3en joins (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 11:30:31 | × | sroso quits (~sroso@user/SrOso) (Quit: Leaving :)) |
| 11:32:25 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:38:16 | <haskellbridge> | <Bowuigi> No but technically yes, "cata" and "ana" are useful |
| 11:40:07 | → | xff0x joins (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) |
| 11:40:45 | → | smalltalkman joins (uid545680@2a03:5180:f:4::8:5390) |
| 11:41:11 | <Rembane> | They in combination are pretty |
| 11:49:09 | × | dsrt^ quits (ciwoudofon@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 248 seconds) |
| 11:55:51 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 11:56:01 | → | sam113101 joins (~sam@24.157.253.231) |
| 12:02:41 | × | son0p quits (~ff@2800:e2:f80:ee7::1) (Ping timeout: 244 seconds) |
| 12:03:58 | <dminuoso> | Yes, catanas are pretty - but sharp and dangerous. |
| 12:09:57 | → | biberu\ joins (~biberu@user/biberu) |
| 12:11:21 | → | ZharMeny joins (~user@user/ZharMeny) |
| 12:12:28 | × | biberu quits (~biberu@user/biberu) (Ping timeout: 245 seconds) |
| 12:12:29 | biberu\ | is now known as biberu |
| 12:13:16 | × | dysthesis quits (~dysthesis@user/dysthesis) (Ping timeout: 260 seconds) |
| 12:15:28 | → | gmg joins (~user@user/gehmehgeh) |
| 12:22:01 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 12:22:09 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 12:41:05 | × | ddellacosta quits (~ddellacos@ool-44c73c8f.dyn.optonline.net) (Ping timeout: 255 seconds) |
| 12:45:29 | gehmehgeh | is now known as gmg |
| 13:03:26 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 13:08:48 | × | CiaoSen quits (~Jura@2a05:5800:42f:e600:ca4b:d6ff:fec1:99da) (Ping timeout: 272 seconds) |
| 13:08:48 | × | ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 272 seconds) |
| 13:11:14 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:12:49 | → | ubert joins (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) |
| 13:17:32 | → | danse-nr3 joins (~danse-nr3@user/danse-nr3) |
| 13:22:24 | → | alexherbo2 joins (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) |
| 13:24:32 | → | son0p joins (~ff@2800:e6:4001:8da7:232f:489b:caf3:dc20) |
| 13:29:42 | → | dtman34 joins (~dtman34@c-174-53-203-90.hsd1.mn.comcast.net) |
| 13:31:25 | → | srazkvt joins (~sarah_@2a01:e0a:483:6900:b6d5:d9cd:2f20:2e49) |
| 13:36:11 | → | spew joins (~spew@201.141.102.132) |
| 13:38:38 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 13:39:50 | × | srazkvt quits (~sarah_@2a01:e0a:483:6900:b6d5:d9cd:2f20:2e49) (Quit: Leaving) |
| 13:40:03 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:46:33 | × | acidjnk_new quits (~acidjnk@p200300d6e72cfb83c8b55ff2a9bbb599.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 13:48:24 | × | danse-nr3 quits (~danse-nr3@user/danse-nr3) (Ping timeout: 252 seconds) |
| 13:49:01 | × | rosco quits (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 13:54:15 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 13:56:34 | × | xff0x quits (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) (Ping timeout: 260 seconds) |
| 13:59:30 | × | ash3en quits (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Ping timeout: 265 seconds) |
| 14:00:07 | → | danse-nr3 joins (~danse-nr3@user/danse-nr3) |
| 14:04:03 | → | xff0x joins (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) |
| 14:09:13 | × | alexherbo2 quits (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) (Remote host closed the connection) |
| 14:09:33 | → | alexherbo2 joins (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) |
| 14:10:22 | × | alexherbo2 quits (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) (Remote host closed the connection) |
| 14:10:41 | → | alexherbo2 joins (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) |
| 14:17:17 | → | ash3en joins (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 14:20:47 | × | ash3en quits (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Client Quit) |
| 14:23:12 | → | gmg joins (~user@user/gehmehgeh) |
| 14:34:56 | × | jcarpenter2 quits (~lol@96.78.87.197) (Ping timeout: 255 seconds) |
| 14:42:31 | → | dans90387 joins (~danse-nr3@user/danse-nr3) |
| 14:44:08 | × | arahael quits (~arahael@user/arahael) (Ping timeout: 245 seconds) |
| 14:44:37 | × | danse-nr3 quits (~danse-nr3@user/danse-nr3) (Ping timeout: 248 seconds) |
| 14:49:07 | → | acidjnk_new joins (~acidjnk@p200300d6e72cfb83b0c9f42d7d842c79.dip0.t-ipconnect.de) |
| 14:58:11 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:04:57 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 15:15:16 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 15:20:05 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 15:22:12 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 15:26:31 | × | sprout quits (~sprout@84-80-106-227.fixed.kpn.net) (Remote host closed the connection) |
| 15:32:08 | → | sprout joins (~sprout@84-80-106-227.fixed.kpn.net) |
| 15:32:39 | × | petrichor quits (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:38:46 | × | alexherbo2 quits (~alexherbo@2a02-8440-311b-18ba-4d3e-ed9a-139e-775f.rev.sfr.net) (Remote host closed the connection) |
| 15:39:19 | <haskellbridge> | <thirdofmay18081814goya> is there a mapping in either direction between a state monad and a histomorphism? |
| 15:40:01 | → | alexherbo2 joins (~alexherbo@2a02-8440-311b-18ba-e069-9844-ae47-6e63.rev.sfr.net) |
| 15:53:10 | <probie> | What sort of mapping would you expect? To my mind they are very different things |
| 15:54:59 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 260 seconds) |
| 15:56:05 | × | alexherbo2 quits (~alexherbo@2a02-8440-311b-18ba-e069-9844-ae47-6e63.rev.sfr.net) (Remote host closed the connection) |
| 15:57:32 | <EvanR> | in some sense you can replace statefulness with access to history |
| 15:58:42 | <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) |
| 15:58:48 | → | CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) |
| 15:59:04 | × | dans90387 quits (~danse-nr3@user/danse-nr3) () |
| 16:02:19 | <EvanR> | the etymological or practical relationship between history and histomorphisms if any is an exercise for the reader |
| 16:06:49 | × | sam113101 quits (~sam@24.157.253.231) (Ping timeout: 260 seconds) |
| 16:10:34 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 272 seconds) |
| 16:11:03 | → | SovereignNoumena joins (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) |
| 16:11:58 | × | SovereignNoumena quits (~Sovereign@68-69-210-238.sktn.hsdb.sasknet.sk.ca) (Read error: Connection reset by peer) |
| 16:15:03 | × | akegalj quits (~akegalj@197-208.dsl.iskon.hr) (Remote host closed the connection) |
| 16:15:21 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 16:16:09 | × | machinedgod quits (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 16:19:40 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 16:21:21 | → | sam113101 joins (~sam@modemcable220.199-203-24.mc.videotron.ca) |
| 16:23:37 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit) |
| 16:24:04 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 16:24:16 | <monochrom> | IMO recursion schemes are an ad hoc zoo except for cata, ana, and Ralf Hinze's generalization via adjoint functors. |
| 16:26:00 | <c_wraith> | that sounds like an insult against primitive recursion! |
| 16:26:45 | <c_wraith> | ... sure, cata and para are computationally equivalent. but not operationally, especially in Haskell |
| 16:26:58 | <monochrom> | No! Primitive recursion is covered by cata or maybe sometimes we need adjoint cata. |
| 16:27:56 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:28:15 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 16:28:22 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 16:31:27 | → | az181 joins (~az181@bmly-12-b2-v4wan-164596-cust791.vm4.cable.virginm.net) |
| 16:35:37 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 265 seconds) |
| 16:36:07 | → | Pixi joins (~Pixi@user/pixi) |
| 16:38:05 | → | ft joins (~ft@p4fc2a393.dip0.t-ipconnect.de) |
| 16:39:30 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 16:50:09 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 16:55:28 | → | ash3en joins (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) |
| 16:56:21 | × | ubert quits (~Thunderbi@178.165.178.117.wireless.dyn.drei.com) (Ping timeout: 248 seconds) |
| 17:00:40 | × | CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) (Read error: Connection reset by peer) |
| 17:01:05 | → | gmg joins (~user@user/gehmehgeh) |
| 17:03:41 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:03:46 | → | CrunchyFlakes joins (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) |
| 17:05:58 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:07:34 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 17:10:25 | × | son0p quits (~ff@2800:e6:4001:8da7:232f:489b:caf3:dc20) (Ping timeout: 265 seconds) |
| 17:10:54 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 17:12:30 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 17:14:53 | → | jcarpenter2 joins (~lol@2603:3016:1e01:b960:a04f:145c:6e83:611e) |
| 17:15:44 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 265 seconds) |
| 17:19:47 | <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 |
| 17:20:57 | <probie> | Does anyone have strong opinions about defining numeric constants as patterns instead of variables? |
| 17:21:29 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:26:00 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 17:26:56 | → | aforemny joins (~aforemny@2001:9e8:6ceb:b200:7a4b:8b9f:cdb1:25bb) |
| 17:27:18 | → | pavonia joins (~user@user/siracusa) |
| 17:27:39 | → | SovereignNoumena joins (~Sovereign@24.79.228.157) |
| 17:27:45 | × | aforemny_ quits (~aforemny@i59F516CA.versanet.de) (Ping timeout: 246 seconds) |
| 17:28:38 | × | SovereignNoumena quits (~Sovereign@24.79.228.157) (Read error: Connection reset by peer) |
| 17:32:13 | <monochrom> | Would that be using pattern synonyms? |
| 17:33:43 | <probie> | yes |
| 17:33:57 | <monochrom> | It feels like #define but better. :) |
| 17:34:33 | <EvanR> | does it compile better |
| 17:35:04 | → | Square joins (~Square@user/square) |
| 17:35:49 | × | Square2 quits (~Square4@user/square) (Ping timeout: 248 seconds) |
| 17:36:54 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:41:41 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 17:42:59 | → | danse-nr3 joins (~danse-nr3@user/danse-nr3) |
| 17:43:17 | <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? |
| 17:44:41 | <monochrom> | I haven't seen it in a library. |
| 17:45:17 | <monochrom> | But I haven't looked for it really hard. |
| 17:48:07 | <EvanR> | what happens if it tries to grow but ran out of space |
| 17:48:50 | <monochrom> | I guess the same as trying to get a too-big array in the first place. |
| 17:49:11 | <Franciman> | hi EvanR , i think it is allowed to grow only as far as the pre-allocated memory permits |
| 17:49:50 | <EvanR> | hi Franciman |
| 17:51:07 | <monochrom> | OK, that's fair. |
| 17:51:50 | <EvanR> | since it's Mutable you can throw an exception |
| 17:52:20 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 17:54:17 | × | Square quits (~Square@user/square) (Ping timeout: 255 seconds) |
| 17:54:25 | <mauke> | https://paste.tomsmeding.com/xgQtgjM8 clearly this is what PatternSynonyms were intended for |
| 17:56:54 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 17:58:59 | → | Square joins (~Square@user/square) |
| 18:00:47 | <EvanR> | that's so cursed |
| 18:05:11 | <Franciman> | is there any document formally defining how haskell to core translation works? |
| 18:05:54 | × | Square quits (~Square@user/square) (Ping timeout: 246 seconds) |
| 18:06:05 | <probie> | <unhelpful>the source code of GHC</unhelpful> |
| 18:06:37 | <mauke> | reflections on formalizing formalizers |
| 18:07:00 | <monochrom> | That is evil. |
| 18:07:43 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:08:05 | → | Square joins (~Square@user/square) |
| 18:08:31 | <mauke> | unfortunately it seems you can't inject variables from a pattern into the surrounding scope :-) |
| 18:08:52 | <mauke> | Main = \argv -> do ... |
| 18:12:14 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 18:12:52 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:14:08 | <haskellbridge> | <thirdofmay18081814goya> monochrom: there's no work on defining adjoint folds in haskell right? |
| 18:21:11 | <[exa]> | mauke: perhaps it could interact with record wildcards? these kinda inject stuff |
| 18:23:06 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 18:23:10 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:23:23 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:27:07 | × | Square quits (~Square@user/square) (Ping timeout: 264 seconds) |
| 18:27:35 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 18:27:50 | zero | is now known as yin |
| 18:30:05 | <monochrom> | mauke: That's the job of dynamic scoping and implicit parameters, right? >:) |
| 18:30:37 | → | Square joins (~Square@user/square) |
| 18:35:45 | × | danse-nr3 quits (~danse-nr3@user/danse-nr3) () |
| 18:37:37 | × | Square quits (~Square@user/square) (Ping timeout: 248 seconds) |
| 18:38:05 | <dmj`> | Franciman: there's at least two good blog posts on desugaring, and then there's source |
| 18:38:35 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:38:38 | <Franciman> | the source is not a formal semantics |
| 18:38:46 | <Franciman> | I shall look up the blog posts, thanks dmj` ! |
| 18:39:12 | <[exa]> | (==> blog posts are formal semantics) |
| 18:39:26 | <Franciman> | lol, they may contain a formal semantics |
| 18:39:40 | <Franciman> | it would be fun if a formal semantics wuold be considerd so only if presented on a specific medium |
| 18:39:42 | <Franciman> | what would it be? |
| 18:39:50 | <monochrom> | Code is as formal as one can get. You can call it unusable but you can't call it informal. |
| 18:39:50 | <Franciman> | i imagine an ancient papir |
| 18:40:03 | <[exa]> | journal of formal semantics |
| 18:40:09 | <Franciman> | monochrom: then what's the point of formal semantics if we just can use code? |
| 18:40:11 | <Franciman> | lol |
| 18:40:13 | <Franciman> | cringe af |
| 18:40:14 | <[exa]> | (coincides much with ancient paper, yes) |
| 18:40:25 | <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. |
| 18:40:25 | <Franciman> | so GCC is formalized |
| 18:40:57 | <Franciman> | let us use GCC to formally reason about C |
| 18:41:04 | <Franciman> | ja hoor |
| 18:41:09 | <monochrom> | I already implied the answer. One wants a more usable, higher-level formal language. |
| 18:41:15 | → | ars23 joins (~ars23@79.113.95.110) |
| 18:41:31 | × | ars23 quits (~ars23@79.113.95.110) (Changing host) |
| 18:41:31 | → | ars23 joins (~ars23@user/ars23) |
| 18:42:25 | <Franciman> | monochrom: there is a tiny issue in your reasoning. Circularity |
| 18:42:28 | <Franciman> | ghc is written in haskell |
| 18:42:37 | <Franciman> | what's ghc code semantics |
| 18:42:52 | <Franciman> | if you are trying to understand haskell's semantics? |
| 18:43:00 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 18:43:03 | <Franciman> | you must go back to the first bootstrappable version of ghc |
| 18:43:08 | <Franciman> | and study its semantics |
| 18:43:12 | <monochrom> | There is no circle if you include versioning. |
| 18:43:14 | <haskellbridge> | <thirdofmay18081814goya> system hw |
| 18:43:47 | <Franciman> | so this all boils down to: yes, haskell has a formal semantics, but to make sense of it, you must know GCC |
| 18:43:53 | <Franciman> | and its a huge piece of software |
| 18:43:56 | <Franciman> | but hey we got formal semantics ;) |
| 18:43:58 | <monochrom> | I did say unusable. |
| 18:44:01 | <haskellbridge> | <thirdofmay18081814goya> * fw |
| 18:44:22 | <dmj`> | Franciman: some people tried porting Core to Gallina, and then proving things there, but the "formalization gap" is known |
| 18:44:37 | <monochrom> | Just showing you that requiring "formal" alone is not good enough. |
| 18:44:47 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:44:56 | <monochrom> | The same way a lot of people here used to talk about "building a community". |
| 18:45:10 | <probie> | Outside of SML (and maybe things like Dafny), which languages even have a formal semantics? |
| 18:45:28 | <Franciman> | scheme too, and i'm not aware of other |
| 18:45:30 | <monochrom> | The best way to build a community is mutual congratulation. Clearly no one actually wants that. |
| 18:45:44 | <Franciman> | you are the first to not want that, monochrom |
| 18:45:46 | <haskellbridge> | <thirdofmay18081814goya> why is system fw not good enough? there's even formalizations in coq |
| 18:48:00 | <haskellbridge> | <thirdofmay18081814goya> often all you need to make convincing proofs is a small subset anyways |
| 18:48:37 | <monochrom> | The same way a decade ago math people on IRC were dreaming of IRC clients that could render inline LaTeX. |
| 18:48:52 | <monochrom> | Such a client actually existed during their time. It's Pidgin. |
| 18:49:10 | <monochrom> | And of course the people were like "no that doesn't count". |
| 18:49:42 | <monochrom> | And the same way https://ro-che.info/ccc/26 |
| 18:49:53 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 18:49:55 | <monochrom> | Moving goalposts. |
| 18:50:06 | <Franciman> | you are not making sense |
| 18:50:24 | <monochrom> | Sure. But I'm also done. |
| 18:50:29 | <Franciman> | thank god |
| 18:50:33 | <[exa]> | monochrom: rofl the comic |
| 18:50:48 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
| 18:50:55 | <Franciman> | nobody here is requiring haskell to have formal semantics |
| 18:51:06 | <Franciman> | i just asked whether there is a specification of how haskell is translated tocore |
| 18:51:12 | <Franciman> | and you say ghc is the only specification |
| 18:51:14 | <Franciman> | ok |
| 18:51:43 | <Franciman> | and i ask you if I have a formal system to reason about ghc's code |
| 18:51:49 | → | alexherbo2 joins (~alexherbo@2a02-8440-3205-4b2a-98fd-e867-2c7e-b6f1.rev.sfr.net) |
| 18:51:50 | <Franciman> | and you say that you can just go back to previous versions |
| 18:52:07 | <Franciman> | ok |
| 18:52:08 | <[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? |
| 18:52:23 | <Franciman> | I am not requiring it |
| 18:52:28 | <Franciman> | i'm just pondering monochrom's answer as nonsense |
| 18:52:33 | <Franciman> | it's ok to not have it |
| 18:52:44 | <Franciman> | i think 0.1% of PLs have a formal semantics |
| 18:52:48 | <dmj`> | Franciman: its a touchy subject here |
| 18:53:04 | → | Square joins (~Square@user/square) |
| 18:53:28 | <dmj`> | there's efforts though |
| 18:53:30 | <dmj`> | https://www.cis.upenn.edu/~sweirich/talks/dsw18.pdf |
| 18:53:41 | <Franciman> | what you feel hurt haskell doesn't have formal semantics? |
| 18:53:51 | <Franciman> | well to quote monochrom USABLE formal semantics |
| 18:53:54 | <Franciman> | or whatever else they mean |
| 18:54:00 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 18:54:06 | <haskellbridge> | <thirdofmay18081814goya> personally i feel hurt in my little feelings but that's just me |
| 18:54:15 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Client Quit) |
| 18:54:26 | <haskellbridge> | <thirdofmay18081814goya> also just use system fw |
| 18:54:28 | → | athan joins (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 18:54:38 | <Franciman> | monochrom: a very simple question for you. Is ghc's code for translating haskell to core bug free? |
| 18:54:47 | <Franciman> | is it non-ambigous? |
| 18:55:00 | <Franciman> | is there a non-abigous translation to non-ambigous machine code? |
| 18:55:52 | <haskellbridge> | <thirdofmay18081814goya> how can machine code be ambiguous |
| 18:56:06 | <Franciman> | also monochrom, you say you can go back in time. Is any previous version always correct? |
| 18:56:08 | <EvanR> | quantum machine code |
| 18:56:11 | <Franciman> | or should i stop at some point? |
| 18:56:16 | <Franciman> | well branch prediction and stuff |
| 18:56:29 | <haskellbridge> | <thirdofmay18081814goya> EvanR: huh |
| 18:56:35 | <haskellbridge> | <thirdofmay18081814goya> quantum ghc when |
| 18:56:48 | <EvanR> | we already have quantum computing monads |
| 18:56:50 | <Franciman> | so many unanswered questions here, and you speak about moving the goalpost |
| 18:56:52 | <Franciman> | SURE monochrom SURE |
| 18:56:55 | <Franciman> | you are making TONS OF SENSE |
| 18:57:08 | <Franciman> | always with your prejudice against me |
| 18:57:10 | <Franciman> | i'm over this |
| 18:57:35 | <EvanR> | is this what will happen when I go back to coffee at some point |
| 18:58:26 | <[exa]> | lol |
| 18:58:29 | <haskellbridge> | <thirdofmay18081814goya> i don't know i forgot what a normal reaction to an issue about haskell semantics was |
| 18:58:39 | <Franciman> | monochrom has strong prejudice against me and keeps answering in sarcastic and teasing ways |
| 18:58:41 | <Franciman> | i'm over this |
| 18:58:41 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 18:58:50 | <Franciman> | i can't stand it anymore |
| 18:59:12 | <EvanR> | sir this is the internet |
| 18:59:29 | <Franciman> | so i should expect being made fun of in the haskell community? |
| 18:59:31 | <Franciman> | ok, thanks |
| 19:00:02 | <yin> | aw. we're the haskell community |
| 19:00:13 | <Franciman> | if i know it beforehand, i can adjust of course |
| 19:00:31 | <EvanR> | the haskell report explains how to convert rich haskell to core haskell |
| 19:00:33 | <Franciman> | yin: this channel is not part of the haskell community? |
| 19:00:50 | <probie> | It's part of, but not the entire community |
| 19:00:51 | <mauke> | I don't see the sarcasm |
| 19:00:57 | <Franciman> | still a part |
| 19:00:58 | <haskellbridge> | <thirdofmay18081814goya> no it is an extremist cell |
| 19:01:04 | <EvanR> | hahahhaha |
| 19:01:08 | <yin> | Franciman: yes i think so. that makes you also a part of the haskell community |
| 19:01:16 | <EvanR> | we lie low biding our time |
| 19:01:40 | <Franciman> | and according to EvanR it's ok to be sarcastic and teasing to others here |
| 19:01:41 | <EvanR> | until the final battle against imperative programming |
| 19:01:47 | <haskellbridge> | <thirdofmay18081814goya> _the implementation of functional programming languages_ has a section on converting miranda to lambda calculi |
| 19:01:50 | <probie> | This IRC channel probably skews towards "old and bitter" more than other parts of the community |
| 19:01:59 | <Franciman> | i just have to know that |
| 19:02:06 | <Franciman> | i can start being sarcastic all the time too |
| 19:02:07 | <mauke> | I don't think that's right |
| 19:02:15 | <yin> | thirdofmay18081814giya: what would an example of extremist haskell opinion be? |
| 19:02:18 | <Franciman> | like monochrom does to me |
| 19:02:26 | <Franciman> | with their teasing answers |
| 19:02:28 | <mauke> | also, can anyone explain to me which part was sarcasm? |
| 19:02:32 | <mauke> | and/or teasing |
| 19:02:37 | <[exa]> | +1 ^ |
| 19:02:38 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 19:02:39 | <Franciman> | the whole goalmoving thing |
| 19:02:41 | <monochrom> | Yeah that's false accusation. |
| 19:02:45 | <Franciman> | the parallel with my question |
| 19:02:47 | <Franciman> | and the pidgin thing |
| 19:02:50 | <mauke> | what |
| 19:02:58 | <Franciman> | read the scrollback |
| 19:03:04 | <EvanR> | I tried, it's too long |
| 19:03:06 | <haskellbridge> | <thirdofmay18081814goya> yin: you only need conjugate hylomorphisms because all other recursion schemes are an instance of it |
| 19:03:07 | <EvanR> | you sound crazy right now |
| 19:03:11 | <[exa]> | I'd suggest we start over |
| 19:03:14 | <mauke> | I will, but I remember what the pidgin part was about, and I don't see it |
| 19:03:20 | <Franciman> | i will, but monochrom won't |
| 19:03:20 | <yin> | :0 |
| 19:03:25 | <Franciman> | they keep interacting with me in that way |
| 19:03:28 | <Franciman> | and i can't stand it |
| 19:05:09 | <mauke> | yeah, still don't see it |
| 19:06:06 | × | Square quits (~Square@user/square) (Ping timeout: 246 seconds) |
| 19:06:12 | <yin> | Franciman: /ignore is a very useful IRC command. i'm considering using it as we speek |
| 19:06:33 | <yin> | if someone is bothering you, there's no reason not to use it |
| 19:06:34 | <haskellbridge> | <thirdofmay18081814goya> yin: typed lambda calculus is enough to model interesting properties of haskell |
| 19:07:05 | <Franciman> | yin: you're right, thanks |
| 19:07:07 | <mauke> | to me, monochrom's comments boil down to "you have unstated assumptions/requirements" |
| 19:07:08 | <yin> | thirdofmay18081814giya: but we need a superior type system for recursion |
| 19:07:29 | <haskellbridge> | <thirdofmay18081814goya> told you, extreme |
| 19:08:21 | <[exa]> | Franciman: btw just curious, what would you want to prove using the semantics? |
| 19:08:30 | <yin> | thirdofmay18081814giya: we might discover that the extremist cell is actually a majority |
| 19:08:46 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:08:59 | → | neuroevolutus joins (~neuroevol@146.70.211.152) |
| 19:09:01 | <Franciman> | [exa]: mostly have a sound compiler for haskell |
| 19:09:17 | <haskellbridge> | <thirdofmay18081814goya> yin: but uh just make it recurse 10000 times and if it has no fixpoint by then just say it is bottom |
| 19:09:27 | <Franciman> | to reason about Hoare Triples in haskell |
| 19:09:29 | <haskellbridge> | <thirdofmay18081814goya> and a few zeroes if the data structure is big |
| 19:09:36 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 246 seconds) |
| 19:09:45 | <[exa]> | Franciman: do you have some closer definition of the soundness? normally that's a property of logic systems, not compilers |
| 19:09:57 | <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 |
| 19:10:01 | <probie> | What even is Haskell? Haskell98? Haskell2010? Whatever GHC supports? |
| 19:10:19 | <mauke> | does Core have semantics? |
| 19:10:23 | <Franciman> | yes it does |
| 19:10:27 | <Franciman> | not completely but it does |
| 19:10:47 | <Franciman> | [exa]: it means it doesn't produce invalid outcomes, basically |
| 19:10:56 | <Franciman> | so whatever evaluation happens, it respects the semantics |
| 19:11:07 | <yin> | yes, but what even _is_ Haskell? *strokes beard* |
| 19:11:30 | <Franciman> | yes that's the qeustion |
| 19:11:35 | <yin> | haskell is a feeling inside |
| 19:11:37 | <Franciman> | so pinpointing a ghc version could help |
| 19:11:38 | <haskellbridge> | <thirdofmay18081814goya> EvanR: just play really fast and reduce the fps so you can prove your theorem before the recursion ends |
| 19:11:46 | → | kaol joins (~kaol@94-237-42-30.nl-ams1.upcloud.host) |
| 19:11:52 | <dmj`> | probie: back in my day, foldl' was still in Data.List |
| 19:11:57 | <[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? |
| 19:12:27 | <[exa]> | yin: haskell are many |
| 19:13:29 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 19:14:06 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 244 seconds) |
| 19:15:07 | <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 |
| 19:15:13 | <Franciman> | monochrom said we have a formal semantics |
| 19:15:20 | → | Square joins (~Square@user/square) |
| 19:15:35 | <Franciman> | but how do I express the soundness of my method wrt this formal semantics that they are trying to refer to? |
| 19:15:56 | <Franciman> | apparently it's not enough to read ghc code |
| 19:16:06 | <Franciman> | you have to run GHC to make the formal semantics appear |
| 19:16:52 | <haskellbridge> | <thirdofmay18081814goya> as a wise man once said the semantics can't be said, it must be seen |
| 19:19:03 | <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? |
| 19:19:41 | <Franciman> | according to them yes |
| 19:19:53 | <[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 |
| 19:20:16 | <Franciman> | i don't know [exa], sorry |
| 19:20:19 | mauke | shrugs |
| 19:20:28 | <dmj`> | thought we only had operational semantics, not denotational semantics. I think laziness makes it more difficult too |
| 19:20:29 | <[exa]> | (because of the many usual problems of enumerability; e.g. if you didn't see Rice's theorem, please have a look) |
| 19:20:57 | <Franciman> | thanks |
| 19:21:01 | <haskellbridge> | <thirdofmay18081814goya> Franciman: why can't you use polymorphic lambda calculus? what do you want to model for which this isn't enough? |
| 19:21:23 | <[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) |
| 19:21:59 | <Franciman> | thirdofmay, because haskell is more practical |
| 19:22:00 | <[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 |
| 19:22:04 | <Franciman> | thanks |
| 19:22:07 | <Franciman> | i will try that |
| 19:23:28 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 19:24:11 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:25:08 | <[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) |
| 19:25:50 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 19:26:24 | <[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 |
| 19:27:51 | <Franciman> | yeah so indeed you have to run ghc |
| 19:27:55 | <Franciman> | makes sense, ok |
| 19:28:20 | × | ss4 quits (~wootehfoo@user/wootehfoot) (Ping timeout: 255 seconds) |
| 19:28:23 | <Franciman> | ty |
| 19:28:53 | <[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 |
| 19:29:19 | <[exa]> | but yeah it's not super easy, that's why people tend to ignore this |
| 19:29:26 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 19:29:44 | <Franciman> | so monochrom what was your point? |
| 19:29:46 | <Franciman> | Can i know? |
| 19:30:02 | <Franciman> | or are you so elevated for me to understand it |
| 19:30:21 | <dmj`> | [exa]: typeclasses alone are very complicated to implement and prove, much less higher rank types and coercions |
| 19:30:29 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 19:30:58 | <Franciman> | i see |
| 19:31:03 | <Franciman> | keeps being very hostile |
| 19:31:49 | <[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.) |
| 19:32:22 | × | Square quits (~Square@user/square) (Remote host closed the connection) |
| 19:32:47 | → | Square joins (~Square@user/square) |
| 19:33:58 | × | Square quits (~Square@user/square) (Remote host closed the connection) |
| 19:36:36 | <[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. |
| 19:37:45 | <Franciman> | [exa]: saying that haskell has a formal semantics that you obtain by running ghc |
| 19:37:47 | <Franciman> | is very strange |
| 19:38:02 | <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 |
| 19:38:09 | <[exa]> | dmj`: well at least there are a few papers that show the system in a nice boxed figure :D |
| 19:38:13 | <Franciman> | it seemed more like trying to turn tables |
| 19:38:18 | <haskellbridge> | <thirdofmay18081814goya> Franciman: it's called operational semantics |
| 19:38:54 | × | athan quits (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 244 seconds) |
| 19:39:15 | <haskellbridge> | <thirdofmay18081814goya> in this sense yeah all programming languages are formally specified |
| 19:39:16 | <[exa]> | Franciman: technically it's right, it's _some_ semantics, and it's ready and interpretable. Utility for various purposes might vary. |
| 19:39:34 | <Franciman> | okay, i will accept this |
| 19:39:37 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:40:27 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 19:41:04 | <[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). |
| 19:42:37 | <[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). |
| 19:43:15 | <[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 |
| 19:43:47 | <[exa]> | not really related to haskell but it's educative |
| 19:44:11 | <dmj`> | [exa]: lmao |
| 19:44:20 | <dmj`> | q.e.d |
| 19:44:21 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 19:44:51 | <haskellbridge> | <thirdofmay18081814goya> [exa]: dodged only until chatgpt learns lean 4 |
| 19:45:09 | <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? |
| 19:45:44 | <[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 |
| 19:47:06 | <[exa]> | thirdofmay18081814goya: I heard it already knows lean4 tho. where's my semantics. |
| 19:47:56 | <jle`> | fr33domlover: i don't think you need to worry about atomicity in that case then yeah |
| 19:48:11 | <[exa]> | fr33domlover: I'd say no (the docs has a code sample that would work with a single writer even without the "atomic block") |
| 19:48:13 | <haskellbridge> | <thirdofmay18081814goya> [exa]: it literally just learned it last month give it a sec |
| 19:48:31 | <Franciman> | [exa]: ah i didn't know seL4, i will llook it up |
| 19:48:36 | <Franciman> | ty again |
| 19:49:02 | <[exa]> | Franciman: btw just curious, did you get any formal introduction to complexity/enumerability? |
| 19:49:19 | <Franciman> | yes |
| 19:50:09 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 248 seconds) |
| 19:50:30 | <fr33domlover> | Thanks jle` , [exa] :) |
| 19:50:42 | <[exa]> | ok so you may imagine that it's possible to encode some Godel shenanigans into any layer of ghc, right. :D |
| 19:50:46 | <[exa]> | Franciman: ^ |
| 19:50:51 | <Franciman> | yes |
| 19:52:43 | <[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 |
| 19:52:52 | <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. |
| 19:53:13 | <mauke> | fr33domlover: as long as https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-IORef.html#memmodel is not a concern |
| 19:53:42 | <mauke> | the issue is not a "half write", but re-ordering with other reads/writes from other threads |
| 19:54:08 | <monochrom> | Yeah, that. |
| 19:54:49 | <tomsmeding> | a half write might still be an issue on some platforms, though. |
| 19:55:02 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 19:55:31 | <mauke> | tomsmeding: not according to the documentation |
| 19:56:17 | <tomsmeding> | hm, I guess a "half write" would be bad news for the GC as well |
| 19:56:19 | <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. |
| 19:57:38 | <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 |
| 19:58:01 | → | Fooo joins (~Square@user/square) |
| 19:59:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 20:00:18 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 20:02:09 | × | alexherbo2 quits (~alexherbo@2a02-8440-3205-4b2a-98fd-e867-2c7e-b6f1.rev.sfr.net) (Remote host closed the connection) |
| 20:03:09 | <dmj`> | [exa]: it would be very nice to have a rebooted THIH that used HM(x), omitting existentials / higher rank types + GADTs |
| 20:03:53 | → | machinedgod joins (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 20:04:29 | <haskellbridge> | <Bowuigi> Is the row types paper saga enough to clarify how entailment works? |
| 20:04:43 | <haskellbridge> | <Bowuigi> No mention of typeclasses, but it should do |
| 20:04:46 | <[exa]> | tomsmeding: yeah, the logic is that other thread's GCs presence kinda forces it to behave well even without atomic* |
| 20:04:55 | <[exa]> | dmj`: yeah I know |
| 20:05:44 | <[exa]> | what's the actual typesystem of MicroHS btw? there's wild stuff implemented in that one |
| 20:06:26 | <haskellbridge> | <Bowuigi> dmj` Also is going bidirectional a bad idea in the context of THIH? It seems to give easier to digest specs |
| 20:06:45 | × | AlexZenon quits (~alzenon@178.34.150.250) (Ping timeout: 248 seconds) |
| 20:09:36 | <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? |
| 20:09:45 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:10:21 | <fr33domlover> | I mean how big can that gap me (if I'm understanding correctly what re-ordering does) |
| 20:10:22 | <monochrom> | It involves two IORef. |
| 20:10:33 | → | AlexZenon joins (~alzenon@178.34.150.250) |
| 20:10:53 | <fr33domlover> | Ah I see |
| 20:11:34 | → | female_student_5 joins (~female_st@79.79.255.40) |
| 20:11:40 | <female_student_5> | example2 = Apply(Lambda "v" (Variable"w") ) (Apply(Lambda "x"(Apply (Variable "x") (Variable "z")(Variable "y") ))(Variable "l"))) |
| 20:11:56 | <female_student_5> | why is this line of code throwing an error |
| 20:12:04 | <mauke> | what error |
| 20:12:10 | <female_student_5> | says parse on error input and highlights the last bracket |
| 20:12:15 | <monochrom> | IMO people shouldn't even write that kind of code, so it's a non-issue to me. |
| 20:12:21 | <female_student_5> | im trying to write this: (λv.w) ((λx.(x z y)) l) |
| 20:12:21 | <mauke> | time to count brackets, then |
| 20:12:42 | <female_student_5> | I have Im still confused |
| 20:12:55 | <mauke> | then maybe it's some outer context |
| 20:13:10 | <mauke> | does the error still occur with 'example2 = 42'? |
| 20:13:19 | × | neuroevolutus quits (~neuroevol@146.70.211.152) (Quit: Client closed) |
| 20:13:25 | <tomsmeding> | there are more ) than ( in that line of code |
| 20:13:39 | <tomsmeding> | count again ;) |
| 20:14:34 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 20:15:07 | <tomsmeding> | (also, please fix your spacing, extra or missing spaces everywhere don't make code easier to read) |
| 20:15:24 | × | AlexZenon quits (~alzenon@178.34.150.250) (Ping timeout: 246 seconds) |
| 20:15:45 | <tomsmeding> | splitting the thing over multiple lines and using some indentation also makes things easier to count: https://paste.tomsmeding.com/bVH0Zsjv |
| 20:16:03 | <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. |
| 20:16:24 | → | AlexZenon joins (~alzenon@178.34.150.250) |
| 20:16:34 | <mauke> | tomsmeding: eh, that's still lisp-style ))))) soup |
| 20:16:54 | <female_student_5> | i want to know what bracket is messing it up |
| 20:17:36 | <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 |
| 20:17:43 | <tomsmeding> | If you don't, then there is some mismatch. :) |
| 20:18:22 | <tomsmeding> | many code editors highlight the matching parenthesis if your cursor is on or beside one; this is also quite helpful |
| 20:18:39 | × | Fooo quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 20:18:45 | <mauke> | > filter (`elem` "()") "example2 = Apply(Lambda v (Variable w) ) (Apply(Lambda x(Apply (Variable x) (Variable z)(Variable y) ))(Variable l)))" |
| 20:18:46 | <lambdabot> | "(())(((()()()))()))" |
| 20:18:50 | <tomsmeding> | (if you're using a code editor that does not do this, consider switching to a more full-featured one) |
| 20:19:30 | <tomsmeding> | > let s = "(())(((()()()))()))" in (length (filter (== '(')) s, length (filter (== ')')) s) |
| 20:19:32 | <lambdabot> | error: |
| 20:19:32 | <lambdabot> | • Couldn't match expected type ‘[Char] -> a’ with actual type ‘Int’ |
| 20:19:32 | <lambdabot> | • The function ‘length’ is applied to two arguments, |
| 20:19:43 | <tomsmeding> | > let s = "(())(((()()()))()))" in (length (filter (== '(') s), length (filter (== ')') s)) |
| 20:19:44 | <lambdabot> | (9,10) |
| 20:19:55 | <tomsmeding> | (the irony, making a parenthesis-matching error here) |
| 20:20:32 | <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)))" |
| 20:20:34 | <lambdabot> | [0,1,2,1,0,1,2,3,4,3,4,3,4,3,2,1,2,1,0,-1] |
| 20:21:10 | <tomsmeding> | that, but then manually ;) |
| 20:22:24 | <female_student_5> | still makes no sense |
| 20:22:32 | <female_student_5> | literally just trying to add a simple variable into it |
| 20:22:35 | <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) |
| 20:22:46 | <tomsmeding> | female_student_5: did you try to count the '(' and ')' in your line of code? |
| 20:22:52 | <female_student_5> | yes but it doesnt help |
| 20:22:59 | <tomsmeding> | what numbers did you end up with? |
| 20:23:00 | <female_student_5> | because by the logic, im going to change the structure of the original line |
| 20:23:05 | <female_student_5> | which is not what I want to do |
| 20:23:19 | <mauke> | what did you get? |
| 20:23:30 | <female_student_5> | Apply(Lambda "v" (Variable"w")) (Apply(Lambda "x"(Apply (Variable "x") (Variable "z") ))(Variable "l")) - THIS WORKS |
| 20:23:30 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 20:23:31 | <female_student_5> | BUT |
| 20:23:34 | <female_student_5> | that is |
| 20:23:45 | <female_student_5> | (λv.w) ((λx.(x z)) l) |
| 20:23:59 | <female_student_5> | I want it to be: (λv.w) ((λx.(x z y)) l) |
| 20:24:06 | <female_student_5> | but I insert the variable y |
| 20:24:10 | <female_student_5> | and it causes problems |
| 20:24:26 | <mauke> | female_student_5: no, what numbers did you get from your count? |
| 20:24:36 | <female_student_5> | the same as you, im telling you, i dont find it helpful |
| 20:24:44 | <female_student_5> | because it doesnt help me to tell me where to put the bracket |
| 20:24:46 | → | son0p joins (~ff@186.121.18.131) |
| 20:24:49 | <female_student_5> | and ive put the brackets everywhere and nothing works |
| 20:24:54 | <mauke> | what |
| 20:25:03 | <tomsmeding> | female_student_5: https://tomsmeding.com/ss/get/tomsmeding/qIOjny |
| 20:25:12 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:25:24 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 20:25:29 | <tomsmeding> | green is what is added in your original line of code as compared to the "THIS WORKS" line you posted just now |
| 20:25:57 | <tomsmeding> | did you intend to add all three of those things? |
| 20:26:30 | <dmj`> | [exa]: MicroHs has the same MonoLocalBinds restriction that GHC has, so no let generalization :( |
| 20:27:28 | <female_student_5> | tomsmeding, yes what you posted doesnt work either |
| 20:27:31 | <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 |
| 20:27:41 | <mauke> | you need to remove it |
| 20:28:09 | <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 |
| 20:29:18 | <female_student_5> | ive put the bracket in 3 different index positions and have event ried without it |
| 20:29:20 | <female_student_5> | tried* |
| 20:29:22 | <female_student_5> | nothing works |
| 20:29:31 | <tomsmeding> | female_student_5: did you read what mauke and I wrote? |
| 20:29:36 | <mauke> | yes, but do you get a different error? |
| 20:29:43 | <female_student_5> | yes, I feel like none of you are reading what I have wrote |
| 20:29:50 | <mauke> | the code you're trying to write is a type error |
| 20:29:53 | <tomsmeding> | what error do you get if you just remove the last ) on the line? |
| 20:29:54 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:30:04 | <mauke> | the fixes we've suggested only get rid of the parse error |
| 20:30:28 | <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) |
| 20:30:32 | <female_student_5> | to be (λv.w) ((λx.(x z y)) l) |
| 20:30:42 | <tomsmeding> | right |
| 20:30:46 | <tomsmeding> | what is the error you're now getting? |
| 20:30:59 | <tomsmeding> | it's probably a different one from before |
| 20:31:05 | <female_student_5> | None |
| 20:31:08 | <female_student_5> | I am asking a question |
| 20:31:18 | <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 |
| 20:31:33 | <mauke> | so when you said "nothing works", you mean "it works, there are no errors"? |
| 20:31:37 | <mauke> | or what |
| 20:31:50 | <female_student_5> | I said it does not produce an error so that means it works |
| 20:31:58 | <tomsmeding> | yes, this one works |
| 20:32:10 | <female_student_5> | yes so how do I adjust it to make it:(λv.w) ((λx.(x z y)) l) |
| 20:32:11 | <tomsmeding> | but your modified line, with the additional Variable, doesn't work -- it gives an error |
| 20:32:14 | <tomsmeding> | what error is that? |
| 20:32:17 | <mauke> | oh, you're talking about different code again |
| 20:32:24 | <tomsmeding> | the error will point you in the right direction |
| 20:32:31 | <mauke> | female_student_5: this is super frustrating. you're not directly answering any of our questions |
| 20:32:42 | <female_student_5> | mauke ok dont help me then |
| 20:32:44 | <tomsmeding> | we're talking past each other here |
| 20:32:47 | <female_student_5> | because I find it hard to talk to you |
| 20:32:49 | <mauke> | you're always changing the topic, talking about something else, or venting frustration |
| 20:33:02 | <tomsmeding> | mauke and I were under the impression that you were still working on the parentheses, and were getting the same parse error |
| 20:33:15 | <female_student_5> | mauke, please dont accuse me of stuff, I am using" I feel " statements on purpose |
| 20:33:20 | <tomsmeding> | but I now suspect that after you fixed the parse error (by removing the final ')'), you're getting a different error |
| 20:33:23 | <female_student_5> | anyway, I am going to leave, this server is not helpful |
| 20:33:27 | <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 |
| 20:33:28 | ← | female_student_5 parts (~female_st@79.79.255.40) () |
| 20:33:39 | <tomsmeding> | (ok so much for trying to diagnose communication issues) |
| 20:33:48 | × | ars23 quits (~ars23@user/ars23) (Quit: Leaving) |
| 20:34:07 | <tomsmeding> | lesson: read your error messages and note when they change |
| 20:38:29 | <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 |
| 20:38:37 | <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 |
| 20:39:35 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 20:39:41 | <mauke> | (the original question, "why is this line of code throwing a [parse] error", was answered fully and directly) |
| 20:40:38 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:41:19 | <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 |
| 20:42:09 | <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 |
| 20:42:09 | <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 |
| 20:42:59 | <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) |
| 20:43:07 | <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`. |
| 20:43:46 | <constxd> | bro you are thinking way too hard about it |
| 20:43:51 | × | ash3en quits (~Thunderbi@2a01:c23:897f:a700:28e1:960a:9b2:3b4d) (Quit: ash3en) |
| 20:44:50 | <constxd> | they were impatient, uncooperative, and ungrateful. plain and simple. who cares that they didn't resolve the problem. good riddance |
| 20:45:06 | <mauke> | I do |
| 20:45:09 | → | gentauro joins (~gentauro@user/gentauro) |
| 20:45:15 | <dmj`> | Bowuigi: entailment in THIH is just superclass detection and instance traversal (byInst, bySuper). |
| 20:45:37 | <haskellbridge> | <Bowuigi> Oh so it is already there |
| 20:45:55 | <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 |
| 20:46:01 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 20:46:02 | <haskellbridge> | <Bowuigi> It makes sense, after all, both extensions share similar syntax and origins |
| 20:46:07 | <constxd> | you couldn't have made it any clearer than the screenshot of the color-coded diff |
| 20:46:55 | <[exa]> | mauke: helping people is hard. |
| 20:46:56 | <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) |
| 20:47:10 | <tomsmeding> | and I suspect that they just didn't notice that the error had _changed_ |
| 20:47:27 | <tomsmeding> | hence they didn't tell us that they now had a different problem, hence the miscommunication |
| 20:47:56 | → | athan joins (~athan@107.116.47.35) |
| 20:48:07 | <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 |
| 20:49:09 | <haskellbridge> | <Bowuigi> So synthesis is just a very focused constraint solver? |
| 20:49:46 | <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 |
| 20:50:31 | <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 |
| 20:50:39 | <mauke> | tomsmeding: that makes sense, unfortunately |
| 20:52:07 | <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 |
| 20:52:30 | <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 |
| 20:53:53 | × | athan quits (~athan@107.116.47.35) (Read error: Connection reset by peer) |
| 20:54:22 | → | athan joins (~athan@2600:382:2d09:ef51:9785:f8c8:8da1:7865) |
| 20:54:25 | <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) |
| 20:54:30 | <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 |
| 20:55:38 | <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 |
| 20:57:10 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 20:57:29 | <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 |
| 20:58:28 | <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) |
| 20:59:45 | <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 |
| 21:01:09 | <dmj`> | yea using prolog is attractive because you get unification for free |
| 21:01:55 | × | CrunchyFlakes quits (~CrunchyFl@ip-109-42-114-232.web.vodafone.de) (Read error: Connection reset by peer) |
| 21:01:59 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 21:02:24 | <EvanR> | constxd, bro that's why this is #haskell and not #team-public-shaming |
| 21:03:24 | <haskellbridge> | <thirdofmay18081814goya> is bartosz milewski's category theory for programmers the best resource for category theory in haskell? |
| 21:03:35 | <EvanR> | is it even in haskell |
| 21:03:44 | <EvanR> | it seems to be just basic category theory |
| 21:03:49 | <EvanR> | with art |
| 21:04:00 | <EvanR> | and not much programming at all |
| 21:04:01 | <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. |
| 21:04:10 | <haskellbridge> | <thirdofmay18081814goya> EvanR: that was my impression too |
| 21:04:46 | <EvanR> | I liked this book which is apparently on arxiv https://arxiv.org/abs/1612.09375 |
| 21:04:58 | <EvanR> | not much haskell either |
| 21:04:59 | <dmj`> | Bowuigi: I'll check out the 2004 Leijen paperr |
| 21:05:51 | <EvanR> | perhaps surprisingly for a haskeller, the book doesn't get around to monads |
| 21:06:20 | <haskellbridge> | <thirdofmay18081814goya> wish there was less: prove this, more: this is the definition, do things with it |
| 21:06:40 | <EvanR> | do things? |
| 21:06:45 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:07:04 | <haskellbridge> | <thirdofmay18081814goya> suddenly "do" |
| 21:07:49 | <EvanR> | conal elliott has a few videos of his presentation on compiling via categories |
| 21:08:06 | <EvanR> | this is ostensibly doing something |
| 21:08:34 | <dmj`> | Bowuigi: do you have a link to your compiler? |
| 21:10:14 | <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 |
| 21:10:53 | <haskellbridge> | <Bowuigi> Wdym my compiler? |
| 21:11:48 | <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) |
| 21:12:36 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:12:59 | <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 |
| 21:13:36 | <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. |
| 21:14:11 | <haskellbridge> | <Bowuigi> Wait which optimizations does it block? |
| 21:14:51 | <dmj`> | Bowuigi: monomorphization |
| 21:15:06 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:15:26 | <haskellbridge> | <Bowuigi> Oh, it may be possible to adapt Lambda Set Specialization to those without much trouble |
| 21:16:42 | <dmj`> | Bowuigi: hah, thats exactly what I'm looking into, but that's specifically for defunctionalization, an improvement on reynolds |
| 21:17:55 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 21:19:09 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 21:20:24 | → | sw4n joins (~sw4n@2605:59c0:40f0:9610:1416:5e9c:d850:b266) |
| 21:21:34 | <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. |
| 21:21:52 | <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... |
| 21:21:57 | <haskellbridge> | ... Riehl (assumes you are a mathematician, big brain stuff in there) |
| 21:22:42 | <haskellbridge> | <Bowuigi> dmj` after defunctionalization, you don't have any more higher rank functions to worry about so monomorphization can work as usual |
| 21:22:56 | <haskellbridge> | <Bowuigi> If I understood them correctly, that is |
| 21:25:17 | <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 |
| 21:25:38 | → | Ptival joins (~halloy449@64.16.51.186) |
| 21:26:00 | × | sw4n quits (~sw4n@2605:59c0:40f0:9610:1416:5e9c:d850:b266) (Remote host closed the connection) |
| 21:27:47 | <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 |
| 21:28:54 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:29:05 | <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)`? |
| 21:29:36 | <haskellbridge> | <Bowuigi> It intersects with type theory at some point, but other than that it is mostly a tool of thought |
| 21:29:49 | <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=web3x&utm_name=web3xcss&utm_term=1&utm_content=share_button |
| 21:31:07 | × | Ptival quits (~halloy449@64.16.51.186) (Changing host) |
| 21:31:07 | → | Ptival joins (~halloy449@user/Ptival) |
| 21:32:58 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:33:27 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 21:35:17 | <dmj`> | Bowuigi: existential types / higher rank polymorphism, polymorphic recursion all block specialization and therefore monomorphization |
| 21:36:17 | <haskellbridge> | <Bowuigi> Oh you mean the one in datatypes, I meant the one in functions |
| 21:36:30 | × | kimiamania2 quits (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 21:36:53 | <dmj`> | depending on the IR, closures and data types are represented identically, like in GRIN |
| 21:37:21 | → | kimiamania2 joins (~65804703@user/kimiamania) |
| 21:37:40 | <haskellbridge> | <Bowuigi> Yeah no idea how to handle datatype monomorphization other than duplicating a lot of code |
| 21:37:59 | <haskellbridge> | <Bowuigi> Oh wait row types sort of give you an entry point |
| 21:38:30 | <dmj`> | code duping is fine if you can do DCE |
| 21:39:02 | <haskellbridge> | <Bowuigi> Either Gaster and Jones or Leijen said something about compiling lacks constraints as evidence passing |
| 21:40:27 | → | Guest25 joins (~Guest25@176.106.34.161) |
| 21:41:45 | <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 |
| 21:43:14 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 21:43:16 | <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 |
| 21:43:50 | <dmj`> | is that an alternative to dictionary passing? |
| 21:44:17 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 21:47:17 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty) |
| 21:48:00 | <haskellbridge> | <Bowuigi> Technically, yes |
| 21:48:04 | × | Guest25 quits (~Guest25@176.106.34.161) (Quit: Client closed) |
| 21:48:35 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 21:49:09 | × | son0p quits (~ff@186.121.18.131) (Ping timeout: 248 seconds) |
| 21:49:15 | <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 |
| 21:52:51 | <dmj`> | yea that static monomorphization for that would be a good alternative, but it would only work with WPC, and disabling polymorphic recursion |
| 21:53:42 | <dmj`> | row types shouldn't pose any problem for monomorphization afaict |
| 21:54:03 | <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... |
| 21:54:08 | <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 |
| 21:54:45 | <haskellbridge> | <Bowuigi> I forgot some commas there (englishn't) but it should be clear enough lol |
| 21:55:09 | <dmj`> | is it too much though |
| 21:55:52 | <dmj`> | I think caching could help a lot |
| 21:55:56 | <haskellbridge> | <Bowuigi> Yup, monomorphizing records and variants is pretty much creating C-style structs and unions respectively as needed |
| 21:58:18 | <dmj`> | yea that sounds great, that's what all heap objects become |
| 21:58:44 | <dmj`> | but just fewer pointer indirections this time |
| 21:59:40 | <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) |
| 21:59:42 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 21:59:43 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:00:20 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 22:00:47 | <dmj`> | fewer indirections, less allocations, less GC, faster code |
| 22:01:02 | <haskellbridge> | <Bowuigi> Fun stuff |
| 22:02:18 | <dmj`> | could open the door to writing an OS or RTS w/ Haskell, if you can optimize well enough |
| 22:02:23 | <haskellbridge> | <Bowuigi> I want an interpreted rather than a compiled language (mostly for configs, replacing Nix, Dhall and Hugs in my workflow) but these optimizations sound really interesting |
| 22:03:29 | <dmj`> | why not both |
| 22:03:53 | <dmj`> | Bowuigi: have you looked into GRIN at all |
| 22:04:36 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 22:04:40 | <haskellbridge> | <Bowuigi> Both would be too much for a short project (maybe in the future) |
| 22:04:49 | <haskellbridge> | <Bowuigi> GRIN seems very interesting tbh |
| 22:05:32 | <dmj`> | GRIN is much nicer than STG imo |
| 22:06:21 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 22:06:26 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 22:07:27 | <haskellbridge> | <Bowuigi> Is GRIN still maintained tho? |
| 22:08:24 | <haskellbridge> | <Bowuigi> LLVM is on version 18 and they ask for 7, apparently no support for LSS + Perceus |
| 22:09:35 | <haskellbridge> | <Bowuigi> Unless I'm looking at the wrong repo, which would make sense |
| 22:14:03 | <dmj`> | yea it works, I don't know if it will be upstreamed, but there are compiler plugins that allow you to use it with GHC. LLVM should be fine. You'd have to add LSS to STG for that to work. Perceus I don't know if ref. counting would work due to cyclic data structures |
| 22:14:32 | <dmj`> | but, you can make your own implementation too |
| 22:15:28 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:19:53 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 22:22:27 | <haskellbridge> | <Bowuigi> Hmmm I will definitely try to make a GRIN backend after the main parts of the lang are done. For the interpreter, just Kiselyov's eta optimized combinator compilation algorithm paired with primitives to manipulate Vectors of boxed values should do |
| 22:26:21 | ZharMeny | is now known as house |
| 22:26:33 | house | is now known as ZharMeny |
| 22:30:53 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:31:13 | → | Guest25 joins (~Guest25@176.106.34.161) |
| 22:35:42 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 22:41:21 | × | edwtjo quits (~edwtjo@fsf/member/edwtjo) (Ping timeout: 248 seconds) |
| 22:41:31 | × | Guest25 quits (~Guest25@176.106.34.161) (Quit: Client closed) |
| 22:41:40 | → | edwtjo joins (~edwtjo@h-85-24-142-35.A213.priv.bahnhof.se) |
| 22:41:40 | × | edwtjo quits (~edwtjo@h-85-24-142-35.A213.priv.bahnhof.se) (Changing host) |
| 22:41:40 | → | edwtjo joins (~edwtjo@fsf/member/edwtjo) |
| 22:45:29 | <az181> | dose anyone konw any good beginer progects? I've just finished this course https://haskell.mooc.fi and would like to build a project but i'm not realy sure what to do. any sugestions would be appreciated. |
| 22:46:18 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 22:48:48 | <EvanR> | a computer game |
| 22:49:11 | <EvanR> | turn based, text based, if you want to make it easier |
| 22:49:22 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:50:48 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 22:58:57 | × | acidjnk_new quits (~acidjnk@p200300d6e72cfb83b0c9f42d7d842c79.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 23:00:59 | × | ZharMeny quits (~user@user/ZharMeny) (Read error: Connection reset by peer) |
| 23:01:13 | → | ZharMeny joins (~user@user/ZharMeny) |
| 23:01:45 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:06:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:07:27 | <probie> | An interpreter for a non-Haskell language you wish that you were writing in? |
| 23:09:17 | <jackdk> | http://jackkelly.name/blog/archives/2022/05/28/text-mode_games_as_first_haskell_projects/ |
| 23:09:36 | × | athan quits (~athan@2600:382:2d09:ef51:9785:f8c8:8da1:7865) (Ping timeout: 276 seconds) |
| 23:10:58 | <probie> | Have a go at implementing a backend for "RealWorld" (https://www.realworld.how/) (although that might not qualify as a beginner project, depending on your definition of beginner) |
| 23:12:26 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:13:21 | × | xff0x quits (~xff0x@2405:6580:b080:900:290e:6738:41ab:e283) (Ping timeout: 252 seconds) |
| 23:14:12 | → | xff0x joins (~xff0x@2405:6580:b080:900:8680:f8c6:1d4:83ab) |
| 23:17:06 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:17:52 | <haskellbridge> | <thirdofmay18081814goya> is there any meaningful way to compose recursion scheme? |
| 23:17:55 | <haskellbridge> | <thirdofmay18081814goya> * schemes? |
| 23:18:10 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:20:36 | <probie> | A catamorphism and an anamorphism can be composed into a hylomorphism, and natural transformations compose with each other and {cata,ana}morphisms |
| 23:22:25 | <haskellbridge> | <thirdofmay18081814goya> probie: oh didn't know about the last one, ty |
| 23:22:25 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 23:32:20 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 23:33:27 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:38:03 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 23:42:20 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 23:43:27 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:43:46 | <az181> | thanks for the sugestions |
| 23:48:53 | → | merijn joins (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 23:49:20 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 23:53:59 | <probie> | thirdofmay18081814goya: Probably not the most convincing example, but see https://play.haskell.org/saved/6UmBthxw |
| 23:54:26 | <yin> | don't forget paramorphisms and apomorphisms |
| 23:54:30 | × | merijn quits (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 23:56:43 | <haskellbridge> | <thirdofmay18081814goya> probie: nice!! thanks a lot for the example! |
All times are in UTC on 2024-08-27.