Newest at the top
2024-05-18 21:39:05 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
2024-05-18 21:37:46 +0200 | <Rembane> | I think 0 is the roundest of the hot take primes |
2024-05-18 21:37:12 +0200 | <ncf> | not to be confused with 2, the least-odd prime |
2024-05-18 21:36:48 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 260 seconds) |
2024-05-18 21:34:58 +0200 | <monochrom> | hahaha |
2024-05-18 21:34:51 +0200 | <ncf> | 3 is actually the least odd prime |
2024-05-18 21:34:14 +0200 | <monochrom> | Hot take: 3 is the oddest of odd primes. |
2024-05-18 21:34:08 +0200 | <geekosaur> | the decision was made at some point that, rather than teach the typechecker things like that, it should be done with plugins (iirc) |
2024-05-18 21:33:24 +0200 | <geekosaur> | afaik it just adds constraints for obvious things like that |
2024-05-18 21:33:11 +0200 | <geekosaur> | that might be it |
2024-05-18 21:33:07 +0200 | <raehik> | if possible I'd like to know how to do it manually too |
2024-05-18 21:32:52 +0200 | <raehik> | geekosaur: I know of ghc-typelits-knownnat |
2024-05-18 21:29:59 +0200 | <geekosaur> | or its cousin that I can't recall ottomh |
2024-05-18 21:29:25 +0200 | <geekosaur> | yes. try the natnormalise plugin, I think? |
2024-05-18 21:29:00 +0200 | <ncf> | hmm... is this just GHC being bad |
2024-05-18 21:28:55 +0200 | <ncf> | could not deduce KnownNat (n - 1) from KnownNat n |
2024-05-18 21:26:36 +0200 | <raehik> | ncf: yeah I'm thinking withKnownNat and some unsafeCoerce ing...? |
2024-05-18 21:26:36 +0200 | <ncf> | hmm, i guess it's not clear how to proceed from there |
2024-05-18 21:25:19 +0200 | <lambdabot> | Data.Singletons.TypeLits withKnownNat :: Sing n -> (KnownNat n => r) -> r |
2024-05-18 21:25:18 +0200 | <ski> | @hoogle withKnownNat |
2024-05-18 21:24:30 +0200 | <ncf> | raehik: withKnownNat? |
2024-05-18 21:24:27 +0200 | <ski> | (like there's results where all odd primes are treated the same way, but you have to treat two differently. commonly this is, on some level, because there's only one (unique !) congruence class modulo two which doesn't contain zero) |
2024-05-18 21:24:13 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
2024-05-18 21:23:05 +0200 | <ncf> | that's true |
2024-05-18 21:22:37 +0200 | <ski> | ncf : perhaps it would be nicer with commutative monoids .. but the indices had an order given by `Ix' in this case |
2024-05-18 21:21:52 +0200 | <Rembane> | That's a good quote |
2024-05-18 21:21:26 +0200 | <ski> | i recall some mathematician saying that two is the oddest of the primes |
2024-05-18 21:21:16 +0200 | <raehik> | I need a `decSNat :: SNat n -> SNat (n-1)` (ignore n=0 case) but I can't incur KnownNat constraints. How do I write this? |
2024-05-18 21:18:32 +0200 | <mauke> | there's 10 kinds of people: binary and non-binary |
2024-05-18 21:18:01 +0200 | <EvanR> | even and odd |
2024-05-18 21:17:53 +0200 | <EvanR> | there's 10 kinds of prime numbers |
2024-05-18 21:17:44 +0200 | <ncf> | it's not actually an "extension" proper because the composition doesn't recover f |
2024-05-18 21:17:30 +0200 | <int-e> | mauke: I guess you can try that defense. (That 2 is *the* odd prime.) |
2024-05-18 21:17:27 +0200 | <ncf> | i wonder if this construction has a name |
2024-05-18 21:17:23 +0200 | <ncf> | and ximap is just the restriction of that to maps with finite contiguous domains (arrays) |
2024-05-18 21:17:06 +0200 | <ncf> | so i guess any map f : A → M into a monoid can be extended along g : A → B as b ↦ sum(f(g⁻¹(b))) : B → M |
2024-05-18 21:16:51 +0200 | <mauke> | how odd |
2024-05-18 21:16:35 +0200 | <int-e> | (I'd like to say that I have two reasons speaking against that but it's really just one.) |
2024-05-18 21:16:15 +0200 | <EvanR> | all proper prime numbers |
2024-05-18 21:16:01 +0200 | <EvanR> | all prime numbers worth their salt |
2024-05-18 21:15:49 +0200 | <ncf> | lol |
2024-05-18 21:15:44 +0200 | <int-e> | mauke: ahem |
2024-05-18 21:14:34 +0200 | <mauke> | for example, it is very hard to prove "all naturals numbers are odd". but if you strengthen the precondition, like "all prime numbers are odd", it gets much easier to prove. |
2024-05-18 21:12:03 +0200 | euleritian | (~euleritia@p200300d40f4af8006c29977101d489e2.dip0.t-ipconnect.de) |
2024-05-18 21:11:49 +0200 | <ski> | only considering fewer situations, so it's easier, not harder, to implement this overall weakened contract) |
2024-05-18 21:11:43 +0200 | <ski> | (oh, and this about contra- and co- variance of inputs/arguments and outputs/results also relates to preconditions and postconditions. if you strengthen the postcondition (make it more demanding), you strengthen the whole contract. but if you strengthen the precondition (make it more demanding), you *weaken* the whole contract, because now you're allowing fewer things to be passed to the operation, you're |
2024-05-18 21:09:03 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
2024-05-18 21:05:55 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
2024-05-18 21:05:43 +0200 | destituion | (~destituio@2a02:2121:607:127a:483a:846b:b497:f738) |
2024-05-18 20:57:27 +0200 | <ski> | mauke : yea, Java messed this up |