不变函子语境下参数化类型正负位置含义解析

核心疑问 #

• PureScript的Data.Functor.Invariant文档指出，不变函子可用于适配包装函数的类型（例如F (a -> a)），其中参数化类型a同时出现在positive position（正位置）和negative position（负位置）。请问这两个术语具体指什么？
• 次要疑问：为何F (a -> a)需要使用全新的不变函子类型，而非普通的协变/逆变函子？

已尝试的学习与搜索路径 #

• nLab上的“type theory polarity”相关内容：直觉判断是正确方向，但因缺乏足够的数学/逻辑背景，无法理解大部分内容及与当前问题的关联。
• 主题为“Polarity in Type Theory”的博客文章：同样因背景不足难以理解。
• Stack Overflow问题《Example of Invariant Functor?》：答案提及了“positive”和“negative”术语，但未做解释，还提到了HOAS，但未找到相关关联资源。
• 搜索“higher order abstract syntax HOAS”：内容与当前疑问无关。
• Hackage的layers包文档中关于不变函子的部分：无法理解其与当前问题的关联。
• ploeh博客的《Invariant functors》及《Functors as invariant functors》文章：未提及“positive”或“negative”术语，但引导找到Mark Seemann的系列文章，仍未找到相关内容。
• nLab的“invariant”条目：难度过高，无法理解。

内容的提问来源于stack exchange，提问作者toraritte