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 +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 |
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 +0200 | y04nn | (~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 |