2024/05/18

Newest at the top

2024-05-18 22:00:25 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-05-18 22:00:15 +0200 <raehik> geekosaur: even with that package I need to provide a proof that n >= 1... bleh
2024-05-18 21:39:05 +0200machinedgod(~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 +0200y04nn(~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 +0200L29Ah(~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 +0200euleritian(~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 +0200y04nn(~username@2a03:1b20:8:f011::e10d)
2024-05-18 21:05:55 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)