Newest at the top
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 |
2024-05-18 20:44:05 +0200 | <ski> | type `U' also has type `T'. this means that method return types are covariant |
2024-05-18 20:43:59 +0200 | <ski> | justsomeguy : some kind of thing comes up in Object-orientation, with subtyping. you can have a method (in a subclass) that possibly returns an object that's a subtype of the return type of the object in the superclass. so in superclass `C' you can have `T foo(Blah blah);', and in subclass `D', you can, if you want, instead have `U foo(Blah blah);' as long as `U' is a subtype of `T'. because every object of |
2024-05-18 20:40:54 +0200 | <ski> | justsomeguy : but for `ixmap', you provide `j -> i', getting back `Array i e -> Array j e', so here we're *reversing* direction ! hence, *contra*variant, in this case |
2024-05-18 20:40:09 +0200 | <ski> | justsomeguy : ditto for my `ximap', you provide `i -> j' and get back `Array i e -> Array j e', so both are going in the same direction, still |
2024-05-18 20:39:48 +0200 | <ncf> | in this case the functor under consideration is (`Array` e) |
2024-05-18 20:39:24 +0200 | <ski> | justsomeguy : for `fmap :: (a -> b) -> (Array i a -> Array i b)', we provide a function from `a' elements to `b' elements, and gets back a function from `a' arrays to `b' arrays .. so both functions, the element function, and the array function, go in the same direction |
2024-05-18 20:39:07 +0200 | <ncf> | as with functors: covariant is fmap :: (a -> b) -> f a -> f b, contravariant is contramap :: (a -> b) -> f b -> f a |
2024-05-18 20:38:27 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |