2024/05/18

Newest at the top

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)
2024-05-18 21:05:43 +0200destituion(~destituio@2a02:2121:607:127a:483a:846b:b497:f738)
2024-05-18 20:57:27 +0200 <ski> mauke : yea, Java messed this up
2024-05-18 20:56:43 +0200 <monochrom> The beauty is that neg times neg is pos too. For example in ((X -> Int) -> Int), X is at a positive covariant position, because it's neg of neg.
2024-05-18 20:56:39 +0200 <mauke> this is because of reasons
2024-05-18 20:56:36 +0200 <mauke> if you're familiar with C, T *ptr automatically converts to const T *, but T **ptr does not convert to const T **
2024-05-18 20:56:26 +0200 <ski> e.g. we could have `test p = p t0 && (p t1 || not (p t2))', for some `t0,t1,t2 :: T'
2024-05-18 20:56:05 +0200y04nn(~username@45.129.56.202) (Ping timeout: 240 seconds)
2024-05-18 20:55:58 +0200 <ski> and in `(a -> Bool) -> Bool', `a' is again in positive position. if you have `test :: (T -> Bool) -> Bool', then this function `test' in some sense "contains" a number of `T' values (they're "output", although only indirectly, from the function `test'. you can only "prod" at them by providing predicate callbacks)
2024-05-18 20:54:34 +0200 <ski> in `a -> Maybe b', `b' is in positive (output/result/covariant) position, while `a' is in negative (input/argument/parameter/contravariant) position
2024-05-18 20:54:14 +0200 <mauke> ArrayStoreException
2024-05-18 20:53:36 +0200 <ski> (think about rules like "positive times positive is positive", "positive times negative is negative", ..)
2024-05-18 20:53:18 +0200 <ski> oh, also "positive (position)" for covariant, and "negative (position)" for contravariant
2024-05-18 20:51:59 +0200 <ski> aryah : happy it made sense
2024-05-18 20:51:37 +0200 <ski> there are various other words that are also used. covariant : order-preserving, increasing, monotone, upper. contravariant : order-reversing, decreasing, antitone, lower
2024-05-18 20:51:06 +0200 <aryah> ski: ty, a very clear explanation, I wondered the same a few times
2024-05-18 20:50:22 +0200 <ski> for methods (and functions in general), the inputs (arguments/parameters) are contravariant, and the output (result) is covariant
2024-05-18 20:49:51 +0200 <ski> btw, if you have mutable arrays, then `U[]' is neither a subtype nor a supertype of `T[]', when `U' is a subtype of `T'. this is because we can both read (output) from arrays (which is covariant), and write (input) to arrays (which is contravariant). so saying `Bike[]' is a subtype of `Vehicle[]' is wrong, if the array is mutable
2024-05-18 20:47:35 +0200 <ski> s/some kind/same kind/
2024-05-18 20:46:58 +0200 <ski> so, this is contravariant
2024-05-18 20:46:31 +0200 <ski> a *supertype* `T', though, allowing `bar' in `D' to accept *more* types of objects than the original `bar' in `C'
2024-05-18 20:46:25 +0200 <ski> however, if we instead look at argument/parameter types, say we have `void bar(U obj);' in `C', then we could have `void bar(T obj);' in `D'. because a `D' is supposed to be a `C' (you can pass a `D' object to where a `C' object is expected), `bar' in `D' will always have to be prepared for people sending `U's to it, we can't replace `U' with a subtype of `U', in the subclass `D'. we *can* replace `U' with
2024-05-18 20:45:20 +0200 <EvanR> OOP. foo Blah blah