Newest at the top
| 2025-08-16 12:23:10 +0200 | poscat0x04 | (~poscat@user/poscat) (Ping timeout: 255 seconds) |
| 2025-08-16 12:21:50 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-08-16 12:19:39 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-08-16 12:18:41 +0200 | <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 12:14:20 +0200 | <Leary> | You can further argue that the proofs are declarative too, if you want to go Curry-Howard. |
| 2025-08-16 12:13:25 +0200 | <Leary> | Maths proceeds though rigourous deduction, yes, but in the process of doing so a great number definitions are declared. |
| 2025-08-16 12:10:24 +0200 | <jreicher> | Leary: It depends what you mean by "maths". In personal opinion maths is proof, and that's not declarative. |
| 2025-08-16 12:08:33 +0200 | <yin> | because GHC.TypeNats.Nat is just a synonym to that |
| 2025-08-16 12:08:30 +0200 | Beowulf | (florian@gabilgathol.bandrate.org) |
| 2025-08-16 12:06:03 +0200 | <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 12:05:38 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-08-16 12:05:22 +0200 | <yin> | Leary: that's not bad at all! thanks |
| 2025-08-16 12:01:33 +0200 | Beowulf | (florian@gabilgathol.bandrate.org) (Quit: = "") |
| 2025-08-16 12:00:24 +0200 | <Leary> | yin: I don't know about idiomatic, but I like `compare (void xs) (void ys)`. |
| 2025-08-16 11:59:00 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-16 11:58:30 +0200 | <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 11:51:33 +0200 | <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 11:51:15 +0200 | <davros1> | haskellbridge, thanks |
| 2025-08-16 11:50:31 +0200 | <ackthet> | yep. i also got a 2nd BS in math so I've done real analysis, proofs, modern algebra etc |
| 2025-08-16 11:48:58 +0200 | <jreicher> | I recall you mentioning a background in physics, so I'm guessing you have calculus, PDEs, vector calculus, and tensors. |
| 2025-08-16 11:48:24 +0200 | <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 11:48:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 11:47:44 +0200 | <ackthet> | jreicher: i think certain types of math do, but not the types I was exposed to |
| 2025-08-16 11:46:36 +0200 | trickard_ | trickard |
| 2025-08-16 11:45:34 +0200 | <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 11:43:32 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-16 11:41:19 +0200 | <ackthet> | *intro texts I mean |
| 2025-08-16 11:40:21 +0200 | <ackthet> | jreicher: agreed. I do have a fairly strong math background so might like more of that angle which many texts tend to ignore |
| 2025-08-16 11:33:14 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-08-16 11:30:51 +0200 | jreicher | (~user@user/jreicher) jreicher |
| 2025-08-16 11:24:18 +0200 | trickard_ | (~trickard@cpe-90-98-47-163.wireline.com.au) |
| 2025-08-16 11:24:05 +0200 | trickard_ | (~trickard@cpe-90-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-16 11:17:02 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 11:13:00 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-08-16 11:12:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-16 11:11:38 +0200 | elbear | (~lucian@109.166.131.102) (Ping timeout: 245 seconds) |
| 2025-08-16 11:06:22 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) todi |
| 2025-08-16 11:02:14 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-08-16 11:01:17 +0200 | sprotte24 | (~sprotte24@p200300d16f25fb005c76564b71b01fdc.dip0.t-ipconnect.de) |
| 2025-08-16 10:57:41 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-16 10:56:36 +0200 | jreicher | (~user@user/jreicher) (Quit: In transit) |
| 2025-08-16 10:56:05 +0200 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-08-16 10:54:05 +0200 | hyletic | (~textual@user/hyletic) (Quit: Textual IRC Client: www.textualapp.com) |
| 2025-08-16 10:53:17 +0200 | trickard_ | (~trickard@cpe-90-98-47-163.wireline.com.au) |
| 2025-08-16 10:53:05 +0200 | trickard_ | (~trickard@cpe-90-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-08-16 10:51:34 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-08-16 10:48:11 +0200 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
| 2025-08-16 10:46:45 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-08-16 10:42:17 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-08-16 10:38:17 +0200 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) (Quit: WeeChat 4.5.2) |