Newest at the top
| 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) |
| 2026-04-23 19:20:22 +0000 | <dminuoso> | Since bottom does not come with stack traces... |
| 2026-04-23 19:20:17 +0000 | jmcantrell_ | jmcantrell |
| 2026-04-23 19:20:17 +0000 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-04-23 19:20:16 +0000 | <EvanR> | rather you don't have to do much more than mention them |
| 2026-04-23 19:20:15 +0000 | <dminuoso> | EvanR: An explicit pattern match allows/nudges you into conjuring up an `error`. It saves downstream users a lot of time when they can search for your error string |
| 2026-04-23 19:19:33 +0000 | <EvanR> | you also don't have to mention impossible cases, it's built in |
| 2026-04-23 19:19:19 +0000 | <EvanR> | you don't have to prove this every time since it's built in |
| 2026-04-23 19:19:10 +0000 | <EvanR> | monochrom, for simple algorithms, the termination is guaranteed by recursion on a smaller argument |
| 2026-04-23 19:18:50 +0000 | <monochrom> | For automating finding a proof, you will have to look into satisfiability modulo theories (SMT), e.g., Z3. |
| 2026-04-23 19:18:49 +0000 | <EvanR> | similar to safeFromJust |
| 2026-04-23 19:18:15 +0000 | <EvanR> | if for some reason you have a list that is definitely not empty (and we didn't / can't use NonEmpty to get there), then a pattern match leaves you with no good options |
| 2026-04-23 19:18:10 +0000 | <dminuoso> | Since you can snuff a `error "lib:foo - cannot be empty"` in there, which serves as a primitive assertion whose provenance a downstream user can easily figure out |
| 2026-04-23 19:17:44 +0000 | <EvanR> | that's not true in general no |
| 2026-04-23 19:17:29 +0000 | <EvanR> | they can both go wrong, and a novice might actually end up doing that |
| 2026-04-23 19:17:25 +0000 | <dminuoso> | Even if you make an assumption of non-emptiness, an explicit pattern match is going to be vastly better. |
| 2026-04-23 19:17:13 +0000 | <EvanR> | for the same reason that every use of general recursion is bad? |
| 2026-04-23 19:17:05 +0000 | asd | (~asd@2a02:587:4550:b400:874e:c79f:8e8f:2a67) |
| 2026-04-23 19:16:52 +0000 | <EvanR> | ... |
| 2026-04-23 19:16:47 +0000 | <dminuoso> | EvanR: Id argue that every use of head/tail is bad. *shrugs* |
| 2026-04-23 19:16:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-23 19:16:24 +0000 | <monochrom> | Oh they require you to write the proof. Then they sit back and say "no". |
| 2026-04-23 19:15:55 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |