Communities

Writing
Writing
Codidact Meta
Codidact Meta
The Great Outdoors
The Great Outdoors
Photography & Video
Photography & Video
Scientific Speculation
Scientific Speculation
Cooking
Cooking
Electrical Engineering
Electrical Engineering
Judaism
Judaism
Languages & Linguistics
Languages & Linguistics
Software Development
Software Development
Mathematics
Mathematics
Christianity
Christianity
Code Golf
Code Golf
Music
Music
Physics
Physics
Linux Systems
Linux Systems
Power Users
Power Users
Tabletop RPGs
Tabletop RPGs
Community Proposals
Community Proposals
tag:snake search within a tag
answers:0 unanswered questions
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
votes:4 posts with 4+ votes
created:<1w created < 1 week ago
post_type:xxxx type of post
Search help
Notifications
Mark all as read See all your notifications »
Q&A

Welcome to Software Development on Codidact!

Will you help us build our independent community of developers helping developers? We're small and trying to grow. We welcome questions about all aspects of software development, from design to code to QA and more. Got questions? Got answers? Got code you'd like someone to review? Please join us.

What does "parameterised type in the positive / negative position" mean in the context of invariant functors?

+2
−0

From PureScript's Data.Functor.Invariant documentation (emphasis mine):

A type of functor that can be used to adapt the type of a wrapped function where the parameterised type occurs in both the positive and negative position, for example, F (a -> a).

What do the terms "positive" and "negative position" refer to above?
.. and also wondering why F (a -> a) requires an entirely new type of functor, but that should be another question probably..

I tried to figure this out both by learning more about invariant functors and looking up the terms "positive", "negative" in connection with functional programming, but wasn't able to connect the dots yet. Is there a basic resource that I've missed? Or, at least, where should one start to understand these concepts? (Not even sure what the right topic is; see my research attempts below.)


From the search results for "invariant functor positive negative" , "positively invariant vs negatively invariant polarity" , "type theory positive negative polarity invariant" , and "what are invariant functors":

History
Why does this post require moderator attention?
You might want to add some details to your flag.
Why should this post be closed?

0 comment threads

1 answer

+3
−0

"Invariant" isn't really the right word to search, though that's clearly not obvious. The idea is that we have covariant functors where if we have a -> b we can make f a -> f b, and contravariant functors where if we have a -> b we can make f b -> f a. You can see that the "functor" f a = a -> a is neither covariant nor contravariant. The term "invariant" (which isn't really used this way by the math community) is meant to indicate that it's "not co- or contra-variant". (This notion of "invariant functors" also doesn't really come up that often in my experience. Mathematicians would be more likely to talk about functors out of the core of the category which would give you something like imap but only when the two provided functions are mutually inverse.) Another term, not widely used by the math community, is free variant for a functor that is both covariant and contravariant. The name comes from the fact a functor is usually free variant because it doesn't use the parameter at all. Chapter 2 of Hagino's A Categorical Programming Language gives a technical run-down of formulating these ideas in more generally and systematically.

So one way of defining "positive/negative position" is if we consider the functor that maps its argument to that position, is it covariant/contravariant? So, for example, for a -> b, as a functor of a (with b fixed) it's contravariant and as a functor of b (with a fixed). In practice, negative positions almost always directly or indirectly arise from being the domain of a function type.

One of the reasons for the "positive"/"negative" terminology is that a "negative of a negative is positive". Which is just to say that if you compose two contravariant functors the result is covariant, while if you compose two covariant functors the result is covariant. Of course, composing a covariant functor with a contravariant functor is contravariant. This is even clearer if you eliminate the notion of a contravariant functor, and instead replace them with (covariant) functors from the opposite category. In symbols, a contravariant functor from A to B is a covariant functor AopB, and we have (Aop)op = A. We also have for a functor F : AB that it can also be viewed as a functor Fop : AopBop.

One intuition is "positive" positions are positions where a value of the type "provides" a value, where "negative" positions are positions where a value of the type "accepts" or "receives" a value. This is especially clear for the function type. A function of type A -> B accepts a value of type A and provides a value of type B. Less obvious is a type like (A -> B) -> B, where if the function wants to use its (function) argument it needs to provide a value of type A. The negative of a negative is positive makes sense in this context because if I accept something that accepts a type A, then I need to provide a type A if I want to use it.

Just for completeness, there's also the notion of a strictly positive type. This is usually applied to recursive types and here the idea is that we can define a recursive type R as a fixed point of a type constructor as R = μ x. F x (where μ is the traditional binding form for computing the least fixed point). R is strictly positive if not only is F a covariant functor, but the expression defining F doesn't have positive occurrences of the argument due to being a negative of a negative.

Polarity is something else entirely.

History
Why does this post require moderator attention?
You might want to add some details to your flag.

0 comment threads

Sign up to answer this question »