Newest at the top
| 2026-04-23 19:54:29 +0000 | bgtdsword | (b968c1779f@user/titibandit) (Ping timeout: 244 seconds) |
| 2026-04-23 19:54:29 +0000 | rselim | (ce261f06ff@user/milesrout) (Ping timeout: 244 seconds) |
| 2026-04-23 19:54:29 +0000 | b0o | (0e4a0bf4c9@2a03:6000:1812:100::1bf) (Ping timeout: 244 seconds) |
| 2026-04-23 19:54:04 +0000 | whereiseveryone | (206ba86c98@2a03:6000:1812:100::2e4) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:42 +0000 | jakzale | (6291399afa@user/jakzale) jakzale |
| 2026-04-23 19:53:42 +0000 | probie | (cc0b34050a@user/probie) probie |
| 2026-04-23 19:53:35 +0000 | pmk | (6afe4476a1@2a03:6000:1812:100::26d) pmk |
| 2026-04-23 19:53:29 +0000 | bheesham | (3aa22d8375@2a03:6000:1812:100::e40) bheesham |
| 2026-04-23 19:53:27 +0000 | ggb | (a62ffbaf4f@2a03:6000:1812:100::3ac) ggb |
| 2026-04-23 19:53:27 +0000 | samhh__ | (7569f027cf@2a03:6000:1812:100::e4) (Ping timeout: 244 seconds) |
| 2026-04-23 19:53:17 +0000 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) aniketd |
| 2026-04-23 19:53:05 +0000 | jakzale | (6291399afa@user/jakzale) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 +0000 | ggb | (a62ffbaf4f@2a03:6000:1812:100::3ac) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 +0000 | probie | (cc0b34050a@user/probie) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 +0000 | pmk | (6afe4476a1@2a03:6000:1812:100::26d) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 +0000 | caz | (866183745f@2a03:6000:1812:100::15d4) (Ping timeout: 245 seconds) |
| 2026-04-23 19:53:05 +0000 | smiesner | (b0cf5acf8c@user/smiesner) (Ping timeout: 245 seconds) |
| 2026-04-23 19:52:56 +0000 | jkoshy | (99b9359beb@user/jkoshy) (Ping timeout: 244 seconds) |
| 2026-04-23 19:52:56 +0000 | alethkit | (23bd17ddc6@sourcehut/user/alethkit) (Ping timeout: 244 seconds) |
| 2026-04-23 19:52:40 +0000 | bheesham | (3aa22d8375@2a03:6000:1812:100::e40) (Ping timeout: 245 seconds) |
| 2026-04-23 19:52:40 +0000 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 245 seconds) |
| 2026-04-23 19:48:19 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-23 19:43:04 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-23 19:40:27 +0000 | <Comstar> | no magmas? |
| 2026-04-23 19:38:19 +0000 | <monochrom> | One hour later I realized "oh so you're going to define N as the free monoid on the singleton set". |
| 2026-04-23 19:37:38 +0000 | <monochrom> | A math prof was teaching an intro number theory course. I heard from students that he began with monoids. I asked him why, he said "because I don't like the Peano axioms". |
| 2026-04-23 19:37:37 +0000 | <haskellbridge> | <ijouw> generalizing peano numbers: instance (Monoid a) => Num [a] |
| 2026-04-23 19:37:34 +0000 | layline_ | (~layline@149.154.26.56) (Textual IRC Client: www.textualapp.com) |
| 2026-04-23 19:36:35 +0000 | <monochrom> | which brings me to... |
| 2026-04-23 19:36:10 +0000 | <monochrom> | More precisely, for each type T, [T]'s foldr is catamorphisms for [T]. Now let T=() for Peano naturals. :) |
| 2026-04-23 19:35:42 +0000 | <Comstar> | folds/foldable and stuff |
| 2026-04-23 19:35:11 +0000 | <Comstar> | oh that's where I heard it before then |
| 2026-04-23 19:34:54 +0000 | <monochrom> | List's foldr is catamorphisms for cons lists. |
| 2026-04-23 19:33:39 +0000 | <Comstar> | yeah I could see that |
| 2026-04-23 19:32:25 +0000 | <monochrom> | Look for "catamorphism". What you have in mind may be catamorphisms for "data N = Z | S N". |
| 2026-04-23 19:31:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-23 19:31:40 +0000 | <Comstar> | where n \in \mathbb{N} |
| 2026-04-23 19:31:23 +0000 | <Comstar> | is there a generalized proof on peano-like recursion? like you have your base case essentially f_0 and some recursive step that takes you from an f_n to an f_{n-1} |
| 2026-04-23 19:31:10 +0000 | <monochrom> | Data.List.group is my last excuse for using head for non-toys (e.g., map head . group). I'm actually happy that Data.List.NonEmpty has a modernized group that produces [NonEmpty a] so I don't have to use head. |
| 2026-04-23 19:27:17 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-23 19:27:08 +0000 | accountant | (~accountan@2600:1702:5b61:8b40:955:b655:442f:e301) |
| 2026-04-23 19:25:15 +0000 | <monochrom> | Did you see the ">:)"? >:) |
| 2026-04-23 19:24:49 +0000 | <haskellbridge> | <ijouw> Maybe don't put it in the first homework? |
| 2026-04-23 19:23:59 +0000 | <haskellbridge> | <ijouw> I had to for theorem proof (and make a valid termination argument). |
| 2026-04-23 19:22:53 +0000 | <monochrom> | Speaking of which, and crossovering the Dhall/System-F conversation yesterday or two days ago: If I teach Dhall, it will be "fun" to put Ackermann on homework. >:) |
| 2026-04-23 19:21:58 +0000 | <EvanR> | the world ended because we didn't do the ideology and make sure all functions are total |
| 2026-04-23 19:21:25 +0000 | <EvanR> | you crashed |
| 2026-04-23 19:21:19 +0000 | <EvanR> | that *is* bottom |
| 2026-04-23 19:21:17 +0000 | <dminuoso> | And personally I think it improves awareness of where your code is brittle |
| 2026-04-23 19:20:48 +0000 | Square3 | (~Square@user/square) (Ping timeout: 244 seconds) |