Logs: liberachat/#haskell
| 2025-08-16 09:45:34 | <jreicher> | ackthet: I'm not sure whether a math background helps, but emphasis on "not sure". A logic background certainly helps, as a type system is logistic, and a math background might help in the relationship between recurrence relations and recursion, but functional programming is declarative, and I'm not sure if even maths gives you a background in that. |
| 2025-08-16 09:46:36 | trickard_ | is now known as trickard |
| 2025-08-16 09:47:44 | <ackthet> | jreicher: i think certain types of math do, but not the types I was exposed to |
| 2025-08-16 09:48:02 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 09:48:24 | <ackthet> | i'm the least worried about the type system. that make a lot of sense on pervious attempts, and it was my favorite thing about the lang |
| 2025-08-16 09:48:58 | <jreicher> | I recall you mentioning a background in physics, so I'm guessing you have calculus, PDEs, vector calculus, and tensors. |
| 2025-08-16 09:50:31 | <ackthet> | yep. i also got a 2nd BS in math so I've done real analysis, proofs, modern algebra etc |
| 2025-08-16 09:51:15 | <davros1> | haskellbridge, thanks |
| 2025-08-16 09:51:33 | <yin> | what's the most idiomatic way of having something like `on compare length [0..9] [0..]` return LT instead of hanging? |
| 2025-08-16 09:58:30 | <Leary> | Maths is very declarative, in very much the same way as Haskell. Typical mathematical function definitions (perhaps using induction) translate very directly to Haskell implementation (perhaps with recursion). |
| 2025-08-16 09:59:00 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 10:00:24 | <Leary> | yin: I don't know about idiomatic, but I like `compare (void xs) (void ys)`. |
| 2025-08-16 10:01:33 | × | Beowulf quits (florian@gabilgathol.bandrate.org) (Quit: = "") |
| 2025-08-16 10:05:22 | <yin> | Leary: that's not bad at all! thanks |
| 2025-08-16 10:05:38 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-16 10:06:03 | <yin> | am I misunderstanding or is https://hackage-content.haskell.org/package/ghc-bignum-1.3/docs/src/GHC.Num.Natural.html#Natural not a type-level nat at all? |
| 2025-08-16 10:08:30 | → | Beowulf joins (florian@gabilgathol.bandrate.org) |
| 2025-08-16 10:08:33 | <yin> | because GHC.TypeNats.Nat is just a synonym to that |
| 2025-08-16 10:10:24 | <jreicher> | Leary: It depends what you mean by "maths". In personal opinion maths is proof, and that's not declarative. |
| 2025-08-16 10:13:25 | <Leary> | Maths proceeds though rigourous deduction, yes, but in the process of doing so a great number definitions are declared. |
| 2025-08-16 10:14:20 | <Leary> | You can further argue that the proofs are declarative too, if you want to go Curry-Howard. |
| 2025-08-16 10:18:41 | <Leary> | yin: DataKinds is in effect, lifting the `Natural` type of value-level nats to the `Natural` kind of type-level nats. |
| 2025-08-16 10:19:39 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2025-08-16 10:21:50 | → | poscat joins (~poscat@user/poscat) |
| 2025-08-16 10:23:10 | × | poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 255 seconds) |
| 2025-08-16 10:29:08 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 10:29:35 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-08-16 10:33:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-16 10:34:29 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2025-08-16 10:36:58 | <yin> | Leary: i was under the impression there was a Peano Nats module somewhere. that's what i was searching for |
| 2025-08-16 10:40:05 | <Leary> | Not that I'm aware of. In fact, even outside of 'base', I only see people roll their own. |
| 2025-08-16 10:43:20 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 2025-08-16 10:44:31 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 10:49:19 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-16 10:54:27 | → | elbear joins (~lucian@109.166.131.102) |
| 2025-08-16 10:54:31 | × | Vq quits (~vq@81-226-147-244-no600.tbcn.telia.com) (Server closed connection) |
| 2025-08-16 10:54:46 | → | Vq joins (~vq@81-226-147-244-no600.tbcn.telia.com) |
| 2025-08-16 10:57:52 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2025-08-16 10:58:43 | × | elbear quits (~lucian@109.166.131.102) (Ping timeout: 245 seconds) |
| 2025-08-16 11:00:04 | × | caconym747 quits (~caconym@user/caconym) (Quit: bye) |
| 2025-08-16 11:00:05 | × | tromp quits (~textual@2001:1c00:3487:1b00:b18c:352c:ad0a:c01) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-16 11:00:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 11:02:21 | → | caconym747 joins (~caconym@user/caconym) |
| 2025-08-16 11:04:33 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-08-16 11:14:46 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 11:16:13 | <yin> | fair enough |
| 2025-08-16 11:16:44 | → | tremon joins (~tremon@83.80.159.219) |
| 2025-08-16 11:18:58 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 11:23:44 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2025-08-16 11:23:45 | × | trickard quits (~trickard@cpe-90-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-16 11:24:21 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2025-08-16 11:25:03 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2025-08-16 11:26:29 | → | trickard_ joins (~trickard@cpe-90-98-47-163.wireline.com.au) |
| 2025-08-16 11:29:54 | → | elbear joins (~lucian@109.166.131.102) |
| 2025-08-16 11:30:08 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 11:36:56 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-16 11:39:33 | × | gawen quits (~gawen@user/gawen) (Server closed connection) |
| 2025-08-16 11:40:46 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 2025-08-16 11:40:52 | → | gawen joins (~gawen@user/gawen) |
| 2025-08-16 11:41:53 | → | califax joins (~califax@user/califx) |
| 2025-08-16 11:43:46 | × | elbear quits (~lucian@109.166.131.102) (Ping timeout: 244 seconds) |
| 2025-08-16 11:47:51 | × | acro quits (~acro@user/acro) (Server closed connection) |
| 2025-08-16 11:48:11 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 11:49:38 | → | elbear joins (~lucian@109.166.131.102) |
| 2025-08-16 11:51:12 | → | acro joins (~acro@user/acro) |
| 2025-08-16 11:51:26 | trickard_ | is now known as trickard |
| 2025-08-16 11:52:53 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-16 12:08:30 | × | gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Server closed connection) |
| 2025-08-16 12:08:56 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 2025-08-16 12:15:49 | × | elbear quits (~lucian@109.166.131.102) (Ping timeout: 248 seconds) |
| 2025-08-16 12:20:34 | × | trickard quits (~trickard@cpe-90-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-16 12:20:47 | → | trickard_ joins (~trickard@cpe-90-98-47-163.wireline.com.au) |
| 2025-08-16 12:25:37 | × | trickard_ quits (~trickard@cpe-90-98-47-163.wireline.com.au) (Ping timeout: 244 seconds) |
| 2025-08-16 12:28:01 | × | puke quits (~puke@user/puke) (Ping timeout: 248 seconds) |
| 2025-08-16 12:29:17 | → | puke joins (~puke@user/puke) |
| 2025-08-16 12:31:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 12:31:21 | → | trickard_ joins (~trickard@cpe-90-98-47-163.wireline.com.au) |
| 2025-08-16 12:34:54 | trickard_ | is now known as trickard |
| 2025-08-16 12:35:57 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 12:46:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 12:49:01 | → | haritz joins (~hrtz@209.35.65.79) |
| 2025-08-16 12:49:01 | × | haritz quits (~hrtz@209.35.65.79) (Changing host) |
| 2025-08-16 12:49:01 | → | haritz joins (~hrtz@user/haritz) |
| 2025-08-16 12:51:22 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-16 12:51:40 | → | tromp joins (~textual@2001:1c00:3487:1b00:b18c:352c:ad0a:c01) |
| 2025-08-16 12:59:31 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 2025-08-16 13:17:29 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 13:24:00 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 13:28:37 | → | athan joins (~athan@syn-047-132-161-157.res.spectrum.com) |
| 2025-08-16 13:33:16 | × | tromp quits (~textual@2001:1c00:3487:1b00:b18c:352c:ad0a:c01) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-16 13:35:33 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 13:37:09 | → | tromp joins (~textual@2001:1c00:3487:1b00:b18c:352c:ad0a:c01) |
| 2025-08-16 13:40:01 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 13:42:53 | × | trickard quits (~trickard@cpe-90-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-16 13:43:05 | → | trickard joins (~trickard@cpe-90-98-47-163.wireline.com.au) |
| 2025-08-16 13:50:55 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 2025-08-16 13:55:24 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-08-16 13:55:48 | × | tromp quits (~textual@2001:1c00:3487:1b00:b18c:352c:ad0a:c01) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-08-16 14:00:15 | → | tromp joins (~textual@2001:1c00:3487:1b00:b18c:352c:ad0a:c01) |
| 2025-08-16 14:00:31 | → | hyletic joins (~textual@208.67.108.99) |
All times are in UTC.