Contravariant Functors Are Weird • Hacker News Board

Re: Contravariant Functors Are Weird

#21

Post by TheAsprngHacker » Thu, Sep 17, 2020, 4:26 PM UTC

maxiepoo wrote: post #15

TheAsprngHacker wrote: post #9

One thing I've never understood is polarity. To my understanding, positive types are defined in terms of their introduction rules and negative types are defined in terms of their elimination rules. However, don't types both have introduction and elimination rules, making them positive or negative based on how you choose to define them? Also, how does polarity (emphasis on introduction versus elimination rules) relate…

The idea of polarity comes from the category theoretic notion of a universal property. Nice types have introduction and elimination rules but for negative types the introduction rule is "reversible" whereas for positive types the elimination rule is. As an example, the function type `A -> B` is negative because the function introduction rule G, x:A |- M : B ---------------- G |- lam x. M : A -> B is a bijection: the…

Thank you for the explanation of polarity, I found it helpful.

I just remembered that people use the +/- notation to denote covariance and contravariance (such as in OCaml syntax and Scala syntax). I think it's possible that the author saw this and then related the +/- notation to polarity, even though variance is unrelated.

Re: Contravariant Functors Are Weird

#22

Post by theschwa » Thu, Sep 17, 2020, 4:59 PM UTC

How would I use contravariants to improve the architecture of some code?

I geek out on articles like this, but I frequently struggle to see where I would actually apply it.

Re: Contravariant Functors Are Weird

#23

Post by magicalhippo » Fri, Sep 18, 2020, 12:01 AM UTC

joppy wrote: post #16

Any function defines a covariant function by postcomposition. Take for example the string-length function (len : string -> int). We can take any other function which outputs a string, say (f : X -> string) where X is any fixed type, and produce a new function (g : X -> int) by g(x) = len(f(x)). So the len function defines a functor from the set of functions with signature (X -> string) to the set of functions with si…

Thank you for the example, this really helped me to grasp the concept.

So given that I'm clueless when it comes to this topic, what kind of functions aren't functors? Those that take multiple parameters or something like that?

Re: Contravariant Functors Are Weird

#24

Post by brmgb » Fri, Sep 18, 2020, 12:55 PM UTC

TLDR: If you have a function from b to c and a function from a to b then if you run the second function before the first one you can see the whole thing as a function from a to c. It even works with multiple arguments of type b by converting them all before hand, no kidding.

Re: Contravariant Functors Are Weird

#25

Post by DanielMcLaury » Wed, Sep 23, 2020, 5:10 PM UTC

euiq wrote: post #8

bollu wrote: post #5

Earlier quoted context omitted.

While I know precisely what you are saying (have been learning scheme theory this summer), this is hardly an accessible example to pure math undergrads , let alone someone who's attempting to learn some functional programming, with no heavy experience with abstract algebra. First of all, why use Spec? Use ideals/varieties, it contains roughly the same data, while being way better to intuit. I'll put my money where my…

Let's just define Spec(R) = Hom(R,-) and call it a day.

This is why affine schemes as a thing never really took off until Grothendieck, despite Noether and Krull noting some of their interesting properties decades before. If you're just using affine schemes you don't get anything you don't get just by doing commutative algebra.

However, once you start gluing affine schemes together, you start getting things that represent functors you can't represent if you're working over the category of commutative rings alone.

Re: Contravariant Functors Are Weird

#26

Post by DanielMcLaury » Wed, Sep 23, 2020, 5:16 PM UTC

theschwa wrote: post #22

How would I use contravariants to improve the architecture of some code? I geek out on articles like this, but I frequently struggle to see where I would actually apply it.

I think in a lot of cases this is sort of like asking "how can I use an abstract factory to improve my COBOL code?"

Like, if your code isn't already written in terms of classes, you probably can't just jump in and use OOP design patterns to do anything.

Similarly, you may need to start from a reasonably functional codebase to apply most functional programming concepts.