Newest at the top
| 2024-06-26 01:35:44 +0200 | <joeyadams> | This means if I generate bindings for a database with 100 tables, I end up with an absurdly large binary. Not the end of the world, just slightly disappointing. |
| 2024-06-26 01:34:18 +0200 | <joeyadams> | Records compile into somewhat large binaries, is this a known issue? For example, I have a module with 16 records (205 fields), and it produces a 490K .o file (versus 99K if I remove the records). If I derive generic Aeson instances, it becomes 2.3M, and takes several seconds to compile. |
| 2024-06-26 01:11:36 +0200 | <safinaskar> | for example, "f :: forall (a :: Type -> Type). Int" can be written in C++ so: "template <template <typename> typename T> int f()" |
| 2024-06-26 01:10:22 +0200 | <safinaskar> | i'm not sure about Rust, but in C++ this seems to be totally possible |
| 2024-06-26 01:09:54 +0200 | <safinaskar> | how i will try to prove the same thing using C++ and Rust :) |
| 2024-06-26 01:04:25 +0200 | <EvanR> | and see that it is much more powerful than stuff like coq which cripples itself into only proving true stuff |
| 2024-06-26 01:04:13 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-06-26 01:04:09 +0200 | <safinaskar> | EvanR: unfortunately, this is easy, too. "false :: forall a. a" "false = undefined" |
| 2024-06-26 01:03:21 +0200 | <EvanR> | for your next trick, use haskell to prove FALSE |
| 2024-06-26 01:01:52 +0200 | <safinaskar> | so, yes, it is possible to fake type-level lambdas! |
| 2024-06-26 01:01:13 +0200 | <safinaskar> | so yes, i was able to cope with all problems! |
| 2024-06-26 01:00:57 +0200 | <safinaskar> | this means that induction actually works! |
| 2024-06-26 01:00:46 +0200 | <safinaskar> | in haskell |
| 2024-06-26 01:00:39 +0200 | <safinaskar> | ha! i proved (0 + x = x) using (x + 0 = x) and induction! https://godbolt.org/z/YMYrWW6Ee |
| 2024-06-26 01:00:20 +0200 | ft | (~ft@p4fc2ab80.dip0.t-ipconnect.de) |
| 2024-06-26 00:51:57 +0200 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) |
| 2024-06-26 00:49:55 +0200 | causal | (~eric@50.35.88.207) (Quit: WeeChat 4.3.1) |
| 2024-06-26 00:46:23 +0200 | <EvanR> | call it ring theory |
| 2024-06-26 00:46:08 +0200 | <EvanR> | just make an axiom for that |
| 2024-06-26 00:46:07 +0200 | joeyadams | (~joeyadams@2607:fb91:1617:1400:929b:26f0:654:cc5a) |
| 2024-06-26 00:46:05 +0200 | <EvanR> | easy |
| 2024-06-26 00:44:36 +0200 | cheater | (~Username@user/cheater) |
| 2024-06-26 00:44:31 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc90fd0a56c96235233a.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2024-06-26 00:44:29 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 256 seconds) |
| 2024-06-26 00:44:02 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-06-26 00:43:30 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 255 seconds) |
| 2024-06-26 00:42:11 +0200 | <safinaskar> | now i'm trying to prove (x + y = y + x) (or something similar) using all this machinery |
| 2024-06-26 00:33:33 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-06-26 00:31:40 +0200 | Foxxer | (~Foxxer@152.250.71.122) (Remote host closed the connection) |
| 2024-06-26 00:30:13 +0200 | Foxxer | (~Foxxer@152.250.71.122) |
| 2024-06-26 00:29:56 +0200 | michalz | (~michalz@185.246.207.193) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2024-06-26 00:29:47 +0200 | Foxxer | (~Foxxer@152.250.71.122) (Remote host closed the connection) |
| 2024-06-26 00:29:46 +0200 | Foxxer | (~Foxxer@152.250.71.122) |
| 2024-06-26 00:25:44 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-26 00:24:05 +0200 | sp1ff | (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 2024-06-26 00:22:06 +0200 | <safinaskar> | ncf: but i did my way, because that is whole point |
| 2024-06-26 00:21:56 +0200 | <safinaskar> | ncf: you are very helpful |
| 2024-06-26 00:21:51 +0200 | <safinaskar> | ncf: thanks |
| 2024-06-26 00:20:40 +0200 | <ncf> | note https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-Type-Equality.html |
| 2024-06-26 00:16:13 +0200 | <safinaskar> | i was able to express that lambda! |
| 2024-06-26 00:16:05 +0200 | <safinaskar> | i fixed my code and now it works! |
| 2024-06-26 00:15:57 +0200 | <safinaskar> | ha! it works! https://godbolt.org/z/Pxxjvq3oe |
| 2024-06-26 00:13:16 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-26 00:12:10 +0200 | <ncf> | you'd need a newtype probably |
| 2024-06-26 00:10:54 +0200 | <ncf> | can't** |
| 2024-06-26 00:10:54 +0200 | <safinaskar> | ncf: this is exactly i'm trying to express |
| 2024-06-26 00:10:46 +0200 | <safinaskar> | ncf: thanks |
| 2024-06-26 00:09:35 +0200 | <ncf> | the problem is that there are no type-level abstractions, so you can express p = λ b. Equal (c a) (c b) |
| 2024-06-26 00:09:34 +0200 | Guest89 | (~Guest89@bras-base-mtrlpq4706w-grc-02-174-89-234-134.dsl.bell.ca) (Client Quit) |
| 2024-06-26 00:09:10 +0200 | <ncf> | that's included in ghc2021 |