Newest at the top
| 2024-05-07 21:37:23 +0200 | <ncf> | what's isx? |
| 2024-05-07 21:36:39 +0200 | <tomsmeding> | but that's incidental, you can write a list type of unboxed integers and then you can put one in there |
| 2024-05-07 21:36:28 +0200 | <tomsmeding> | I mean, I guess an unboxed value would count as "cannot put it in a list" |
| 2024-05-07 21:36:08 +0200 | <tomsmeding> | is not the whole point of polymorphism that you can instantiate a type variable with _anything_ |
| 2024-05-07 21:35:38 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-05-07 21:35:36 +0200 | <energizer> | is there a value x that trying to do anything with it other than `isx x` will fail? even identity or putting it in a list |
| 2024-05-07 21:32:44 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-05-07 21:31:14 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-05-07 21:23:35 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 21:20:30 +0200 | madeleine-sydney | (~madeleine@c-71-229-185-228.hsd1.co.comcast.net) |
| 2024-05-07 21:19:02 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 21:17:02 +0200 | sp1ff | (~user@c-24-21-45-157.hsd1.wa.comcast.net) |
| 2024-05-07 21:16:20 +0200 | disgrunt | (~disgrunt@129.176.64.49) (Quit: Boom.) |
| 2024-05-07 21:15:06 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 2024-05-07 21:13:57 +0200 | <meejah> | shapr does ;) |
| 2024-05-07 21:13:05 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 252 seconds) |
| 2024-05-07 21:10:49 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 21:09:21 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-05-07 21:08:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 21:08:40 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-05-07 21:08:33 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 21:08:05 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 21:07:16 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 21:06:41 +0200 | chele | (~chele@user/chele) (Ping timeout: 256 seconds) |
| 2024-05-07 21:06:29 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 21:06:14 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 21:05:31 +0200 | <kaol> | Anyone have more than 32GB RAM? I'd be interested to hear how much more is enough to run the 25m dataset on my little program. https://gitlab.com/kaol/recommender-als |
| 2024-05-07 21:05:22 +0200 | <int-e> | mauke: so how is life in your house of pebbles? |
| 2024-05-07 21:04:51 +0200 | <monochrom> | No, lowercase l :) |
| 2024-05-07 21:04:34 +0200 | <mauke> | also, "lambda" is just greek for L, so lambda calculus => the L pebble |
| 2024-05-07 21:02:25 +0200 | <monochrom> | Hell, s/10%/1%/ |
| 2024-05-07 21:01:52 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 21:01:52 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 21:00:32 +0200 | <glguy> | Sorry, we're not currently accepting rename requests for calculus |
| 2024-05-07 21:00:22 +0200 | <monochrom> | Pebbles of construction will brick your home router! >:) |
| 2024-05-07 20:59:41 +0200 | <mauke> | petition to rename "calculus" to "pebble" |
| 2024-05-07 20:57:02 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2024-05-07 20:56:09 +0200 | <disgrunt> | Thanks all for the input. |
| 2024-05-07 20:55:48 +0200 | <monochrom> | And they teach calculi of constructions. |
| 2024-05-07 20:55:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:55:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:54:46 +0200 | <monochrom> | But you first learn what it should look like to users (the specification) before there is anything to implement for. |
| 2024-05-07 20:53:53 +0200 | <disgrunt> | monochrom: I'm interested in implementing something like Coq or Lean and not using it. |
| 2024-05-07 20:52:35 +0200 | <monochrom> | Because every book that says "lambda calculus" in the title is heading to somewhere else right after the basic (the first 10%). |
| 2024-05-07 20:52:19 +0200 | <ncf> | maybe https://kar.kent.ac.uk/20998/1/ttfp.pdf |
| 2024-05-07 20:51:07 +0200 | <monochrom> | or the official book for Agda. |
| 2024-05-07 20:50:45 +0200 | <monochrom> | Go straight to setting yourself up for calculi of constructions: Read the official book for Coq or the official book for Lean. |
| 2024-05-07 20:49:59 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:48:27 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:47:57 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |