Atelier Evan
Atelier Evan
ContactAbout
Strict Positiveness

Strict Positiveness

Tags
math/PL
Last Updated
Revised963 Sep 25, 2025
Published
Sep 8, 2025
Author
Evan Gao
Text
🎶NOW LISTENING🎶
music
奇縁ロマンス・ナナヲアカリ

前言

最近在搞很早期的一个屎山玩具语言项目，叫 Tigris，致敬 Appel 的 Modern Compiler Implementation in ML 和 Compiling with Continuation.
GitHub - notch1p/tigris: a language of the ML family with user-defined operator.
a language of the ML family with user-defined operator. - notch1p/tigris
GitHub - notch1p/tigris: a language of the ML family with user-defined operator.
https://github.com/notch1p/tigris
GitHub - notch1p/tigris: a language of the ML family with user-defined operator.
这个项目的起点是好几年前第一次接触 Lean 时候写的一个迷你 ML 系语言（但真的只有前端而已， 手写的 Parser + Hindley-Milner Type System）后边 Lean 的库陆陆续续完善了，我又捡起来这个项目，做了把手写的 Parser 的换成 Parser Combinator + Pratt 等各种 feature 上的工作。具体见上面的项目主页。
和一众 Theorem Prover 的 Typechecker 不同，我这个语言显然是没有做 Strict Positivity Checking 的。我的 testcases 里面同样对这个进行了测试。那么我们首先来看什么是 Strict Positivity/ Positiveness (Agda jargon)
💡
以下用我这个 Tigris 语言的语法，有必要时换 Lean. Tigris 可以看作是 Lean/OCaml/Haskell 的缝合怪。

What is SP?

Strict Positivity 指出，对于一个/多个递归类型的定义，这个类型在其 value constructor 的类型签名中必须出现在 strict positive 的位置上。这是什么意思？考虑 List
type List a = Nil | Cons a (List a)
                         ^^^^^^^^^^ ctor signature
我们就要求 List a 应当出现在划线部分的 strict positive 位置上。
那么什么位置算作 strict positive ?
A position is strictly positive if it is not in a function's argument type (no matter how many function types are nested around it) and it is not an argument of any expression other than type constructors of inductive types. —— The Lean Language Reference: 4.4.3.2.2. Strict Positivity
这听起来有点绕，而且是从反面说的。意思就是：一个位置是 strict positive 的当且仅当其
  1. 不在箭头 ( Arrow Type) 的左侧 / 类型 ( dependent product) 的下标/第一个参数上，或
  1. 不作为任何表达式（不包括 type constructor）的参数。
可能听着仍然较为抽象，需要两个反例，这里我直接抄 Lean 给的：
inductive Bad where
  | bad : (Bad -> Bad) -> Bad
情况 1
可以看到 Bad 出现在了箭头的左侧，因而不满足条件 1.
inductive Fix (f : Type u -> Type u) where
  | fix : f (Fix f) -> Fix f
情况 2
可以看到， Fix 作为 f 的参数，且 f 不是任意一个已知的 type constructor，则不满足条件 2.
在这里的例子，情况 2 其实就是 typelevel 的 fixpoint，因而我们用 arrow type constructor instantiate f, 就有 where
这样就违反条件 1 了，所以说可以从情况 2 的反例推出情况 1 的反例。现在我们只需要研究情况 1 即可。

Why Bad bad?

Insight from fixpoint

为何不允许上面两种情况？什么想法？有时候从逻辑的角度想会轻松很多，因为 type theory 的 inconsistencies 直接能推出 runtime 的 inconsistencies. 考虑
读作：若有 ，则有 . 显然这是个重言式，它也指出关系 满足 reflexivity. 现在考虑类型
这个类型是典型的 fixpoint 的签名（关于这个话题几年前我也讲过了，见
Fixpoint is all you need）。读作：若有「若有 则有 」，则有 . 这个类型颇有点循环论证的意味在。
出现这个类型的 inhabitant 是很危险的，因为 没有约束。现在可以构造 —— 这就相当于我们能证明任意命题。那么，难道能说具有上面那个形状的类型都全是有问题的吗？显然不是的。
where denotes the constant function; denotes the default inhabitant of . 只要我们加上一个约束：对任意的 s.t. , 有 . 但这个构造并没有用到箭头左侧，相当于被我们舍弃了。
但这和我们上面说的 Bad 有什么联系呢（teaser: 一个很直觉的想法是把 instantiate 成 Bad 就得到 bad 的签名）？

From fixpoint to Bad

我们现在知道，出现上述类型的 inhabitant 并非完全错误。但是在 inductive 的 Bad 这里，其出现的位置在 value constructor 的签名上 —— value constructor 就是 introduction rule. 直觉上给人的感觉就有一点循环论证。
有人说，那么多递归类型， List Nat Int ，照你这说的，都会有一种循环论证感，但是人家不会，因为人家有 base case. 如果没有base case，即譬如 List 只有一条 introduction rule Cons ，那等价于 Empty .
当然，这不是一个很好的例子，因为一个Bad 的平凡的实例就是 Bad id . 所以这和有没有 Base Case / 是不是 inhabited 关系不大。这里拿出来讲主要是提示一种想法上的启发。
重点是，这个类型允许独立构造出 Bad （无中生有式地, closed term）. 首先给出其在我的 Tigris 中的定义（写法和 Haskell 一样）：
type Bad = Bad (Bad -> Bad)

Construct #1

有一种构造是
let rec collapse : Bad -> Bad
	| Bad k => collapse $ k $ Bad k

let omega : Bad = collapse (Bad collapse)
collapse 可以看作一个 driver, 用于把某个 Bad 里边的 k 取出来，再 apply 到自己身上。而这个 collapse 本身又可以用来 intro 一个 Bad，最终的结果是 omega ，collapse 将自己 apply 到自己身上，达成循环论证 (). 但我认为这并非真正使得各 theorem prover 都要 enforce strict positivity 的驱动力，原因很简单：
  • Theorem prover 一般都做 termination check，上面这种构造首先就过不了停机检查（实际上也当然不可能停机）。
  • 所以这种情况已经被 termination check 给排除了，因而不足以成为 strict positivity 要求的动机。
但上面描述的计算过程是我们构造 Bad 的关键 insight, 现在目的就是尝试一种可以过 termination analysis 的 construct.

Construct #2

其实很简单，上面的 collapse 可以看作不停的将 k apply 到自身 Bad k 上，我们先将其改成 1-step applySelf:
let applySelf b =
	let (Bad k) = b in
	k b
let omega = applySelf $ Bad applySelf
如上所示，发现已经消灭了 letrec . 同时又构造出一个新的 omega. 不妨 term-rewriting 一下：
omega 
==>
	let (Bad k) = Bad applySelf in
	k (Bad applySelf)
==>
  applySelf (Bad applySelf)
==> 
  omega
我们发现，完全不必 letrec ，我们直接就能实现一个循环论证：这就是允许 nonpositive position 的最致命的地方：我们能够逃过 termination check 的法眼，用非递归的写法直接构造出一个 looping computation. 这点，可以通过 Tigris 的 IR (ANF, before lambda lifting) 直接看出：
letι lam3 =
  fun b ↦
    case b of
      «Bad/1» →
        let p1 = b[0]
        p1(b)ᵀ
let con4 = Bad⟦lam3⟧
lam3(con4)ᵀ
不妨脑内 reduce 一下，可以发现， p1 就是 lam3 ；将前者全部换成后者，可知 lam3 是尾递归的；递归调用的参数 b 并不满足严格降链 (strict-decreasing chain) 要求，且实际上它根本没有下降。所以这个函数计算起来一定是 diverge 的。因而其结果应当被推定为 Empty type. 当然，我们的类型系统并不知道这一点，所以右侧类型仍然是 Bad .
现在来想： applySelf 的 result type 是谁决定的？我们发现，就是被 Bad 包住的 k .
不妨改写一下 Bad 的定义：
type Bad = Bad (Bad -> Empty)
上面的程序仍然有效：将这样得到的 applySelf 和 Empty 的 elimination rule 复合一下就有
这样，这个系统就真正的 unsound 了。

Formalizing

有人会说，既然是改写的 Bad 导致的 inconsistency，那我们只禁止这类情况不就好了 —— 实际上是第一种定义能推第二种定义。不妨来写一下 Bad (第一种定义) 的 intro/(dependent-)elim/fold rule (katex 和 mathjax 写 proof tree 还是差了点，直接导出 svg 了)，应该很直观:
  • From we introduce:
  • Eliminate into a family (motive) :
notion image
  • The non-dependent variant:
notion image
  • computation rule of the above:
notion image
豁然开朗了。
注意 elimination rule 中的
我们发现，这两个式子都在箭头的左侧，符合 nonpositive 位置的特征：我们本来就是要用两个 recursor 证明上述类型，结果我们在 recursor 的定义（证明）中直接用到了上述类型 —— 这不就是循环论证吗。
上述循环论证导致这两个 eliminator 过强，使得系统 unsound. 这就是要加强 strict positiveness 的根本动机：
  • 有没有 termination checking 和递不递归都不重要，因为 eliminator 本身就是有问题的：因而这本质上仍是逻辑上的问题，而不是 operational 的。
而前面的定义一推定义二的问题就迎刃而解了，而且定义二不过是一种 monomorphic motive 的特例。我们把 的 result type instantiate 成 Empty 即可。当然，这都是多此一举的操作：我们直接把 Bad eliminate 到任意一个类型：
noncomputable unsafe example {C} (b : Bad) : C :=
  b.recOn (motive := fun _ => C)
    fun f step => step (.bad f)
其中 step 又包含对 recOn 的非降 recursive call
也可以脱裤子放屁：
noncomputable unsafe def explode (b : Bad) : False :=
  -- motive is Bad → False
  b.recOn (motive := fun _ => Bad → False)
    (fun f h b' => h (f b') b') b
noncomputable 是因为 Lean 不支持 eliminator 的 codegen, 这也符合预期：computation rule 是在 kernel 做的，termination checker 检查不到这里。
这个构造，和下面这个程序的构造是等同的：
let rec collapse : Bad -> C
	| Bad k => collapse (Bad k)
一眼就可以看出来是错误的循环论证 —— 但是正常情况下由于 termination checker 的存在写不出 let rec bot () = bot () 错误的玩意，
  • 现在却由于没有 enforce strict positiveness 而可以通过 eliminator 写出了；
  • 此外，我们还可以构造 Lean 看不出来的 divergence (Construction #2), 虽然这个情况造成的问题有限，
  • 但由于 eliminator 的关键问题，所以需要这个限制。
有人会说：那对于这样的类型，我们告诉 kernel 不要去产生对应的 recursor 不就好了么，重点是区别对待 —— well 这就是 unsafe 干的事（当然 unsafe 其实也会产生 unsafe recursor）。最重要的是，由于上述原因， unsafe 就需要是传染性的，一个类型是 unsafe ，所有用到这个类型的东西都需要 unsafe ，最终结果就是整个库都 unsafe，太难看了。
one could argue: 这种难看只是一种心理作用，如果能有一种折中的方案给大家心理上的安慰（譬如一个 compiler flag）区分编程和证明，使得大家编程就随便用 nonpositive 的类型不就好了嘛（因为确实这个限制会带来表达力上的限制）
—— 答：那这个就是权衡证明和编程的问题了，Lean 作为一个 theorem prover，其重心肯定还是在 soundness 上的。

Practical Issues

注意，我们这里所谓 practical，指的仍然是 theorem prover 中的实际问题，而不是传统编程语言的（那些语言，比如 Haskell，ML 系，本来也没有这样的限制。）

NBE divergence

一个很实际的问题是：在做 definitional equality checking/需要 unfold definition 的时候，绝大部分 theorem prover 都做 NBE (normalization-by-evaluation) 。
譬如 Coq 就会将部分代码直接编译到 OCaml bytecode 再经 ocamlopt 处理（我记得是这样），Lean 也会主动 unfold reducible definition 和按需 unfold semireducible 的，如果有上面那样 Construction #2 的 term 出现，虽然现在绝大部分编译器都建 dependency graph 然后通过 SCCs (strongly connected components) 的大小 (size > 1, size = 1 w/ self-edge) 来判断是否有递归，不单纯靠 syntax directed parsing （当然我的 Tigris 还是很单纯的），但是那些方法是无法检查 Construction #2 是否存在递归的：
  • 既然没有递归，自然也没有 termination checking 的说法，
  • kernel 里面针对递归定义设置的一些 guard 也不起作用，那么若遇上这类 Omega term 则
  • 最终结果是 runtime instability, 导致 kernel 和 LSP 的崩溃.
而这个最终结果带来的问题可不小，特别是遇上一些有小问题的编辑器插件的时候：Thoughts 25' - June - 4
有人会说，Lean 也不是不让你定义这种类型，加 unsafe 不就好了么，那么不还是会有这种问题 —— unsafe 对于 kernel 来说也是一个 marker，有这个 marker 的定义都是 irreducible 的。就跟 funext （因为用的 Quotient Construction，包含 propext）会 block reduction 是一个道理。

Expressive Power

这里和普通编程语言的界限就比较模糊了。没有这个限制肯定是更自由的。事实上，本文使用的语言 Tigris，我在编写其 Parser 时就有遇到这个问题（亦见项目的 Readme）。
Tigris 是支持 user-defined operators 的。语法如下：
<op-decl> ::= ("infixl" | "infixr") <prec> <strlit> "=>" <expr>
<prec> ::= <intlit>
因为我们用 parser combinator 这种 monadic parsing 的设计模式，很自然的一点就是去做 higher-order parsing：
  • 将所有的运算符（算符本身，precedence，表达式）按优先级序其次字典序的顺序存储于一张表（TreeMap）中，
  • （这张表显然是 cached，存在一个 State Monad （实际上是 ST -backed StateRefT）中）
  • 利用 chainl chainr 将之 fold 一遍，产生一个新的 parser,
  • 我们每 parse 一个 <op-decl> ，就向表中插一个条目。
可说是一个很简单易懂的方法。
那么，最重要的部分就是什么时候去产生这个新的 parser：按当时的想法是在每一个到 parseExpr （term parser）的 call 处 fold 一遍。那么这实际上效率是很低下的，相当于每 parse 一个 term 我们就需要重新构建一遍 parser，在运算符很多的情况下是很糟糕的：实际上每次对表格的更新只在 <op-decl> 处发生，我们只需在该处构建 parser 然后缓存即可。
很自然地会去想，如果把 parser 缓存在上述的 Parser Monad 的 StateRefT 中就好了：这时候，我们发现，存在一个 cyclic dependency：构建的 parser 本来就在 parser monad 中，现在却要向其 State 部分的定义再添加上自身 —— 产生了一对 mutual recursive 的类型 —— 这时候 strict positiveness 就展现了其负面的效果：
  • parser monad 的 transformer ParserT 是 State-like 的，也就是说其实际上是一个函数类型，
  • 这会导致某个类型 (PEnv) 出现在箭头的左侧：
structure PEnv σ α : Type where
  ops : OpTable
  tys : TyArity
  undTy : List Symbol
  parser : Option (TParser σ α)

inductive TParser σ α where
  | mk (_ : SimpleParserT Substring Char (StateRefT (PEnv σ α) (ST σ)) α)
σ 作为 ST 的形式参数用于封装具体的状态：此处其是 rank-2 bounded，更是 existentially quantified，因而绝对不会泄露出 scope. （题外话）
(kernel) arg #3 of 'TParser'.mk' has a non positive occurrence of the datatypes being declared
这种定义是不被 Lean 接受的。
而且还有一个问题是
  • Lean 只允许 inductive type 的 mutual recursion, 普通 def/abbrev 是没办法 pass termination checker 的（因为它们不靠某个/某些参数来递归），
  • 所以即便允许，用起来也不方便、不符合 monad 的 design pattern：因为这时的 TParser 也不是一个 monad，它没有被 bound 到一个 (type) term 上，
  • 而是作为一个 inductive type 在其中（payload）装了一个 parser monad.
（所以最后我选择用 good ol’ pratt parsing）
这是一个比较 elaborate 的例子，但是也确实说明了这一限制在表达力上带来的问题，当然我也会说，这主要是体现了 termination checking 之于表达力的限制，而不是 strict positiveness.

From Bad to fixpoint

我们前面有 fixpoint to Bad ，现在反过来了（所谓 bidirectional）
而事实上，这主要是行文上的考虑：前面主要是从 insight 和想法的角度叙述两者之间的一种似然的联系，而当我们对 strict positiveness 的问题有足够的了解之时，才能更全面地阐述两者的关系。
前文已经说过，两者的签名在形状上一致： bad 就是 fix 在 α = Bad 的一个 monomorphic variant.
那么 operational 的意义上呢？
细心的读者可以注意到，我用了 omega 这个 id 作为 Construction #2 的变量名：是不是和 term 有点联系呢？ Recall,
再来看这里的 omega ,
omega 
==>
	let (Bad k) = Bad applySelf in
	k (Bad applySelf)
==>
  applySelf (Bad applySelf)
==> 
  omega
我们发现：它们在 operational/behavioral 的意义上是镜像的，都是通过 self-application 实现一个 closed 且 non-normalizing 的 term. 当然 在任何一个不具备 equirecursive/infinite type (solving ) 的系统中都不存在（比如 ocaml 不开 -rectypes 的情况下)，因为没有办法 type — 甚至在 Tigris 的 REPL 中尝试 type 这样的项也会直接报错：
> fun x -> x x
(* Unbounded fixpoint constructor does not exist in a strongly normalized system.
   unifying ?m0 and ?m0 → ?m1 results in μ?m0. ?m0 → ?m1, which isn't allowed.
   recursion is supported primitively via letrec or unsafely via fixpoint combinator `rec` *)
这时候， bad : (Bad -> Bad) -> Bad 就很可注意了：在类型上，可以将其看作一个 wrapper, 将 Bad -> Bad 打包成一个 Bad ，接着通过一个特殊化的 apply (applySelf ) 将其内部的函数取出来，apply 到自身。通过 recursor 去 inteperet 这个计算过程也是一样的，上文亦已阐述过。
  • 若把 fixpoint combinator 想成一个能够给定任意一个 endofunction 则计算出其 fixpoint 的函数，
  • bad 就是其 monomorphic 的一个 variant.
当然，我们需要清晰地区分在这个意义上的两者：在 extensional 的角度看来，它们的行为一致；在 intensional 的角度看来，它们所表达的计算意义完全不同：
  • fixpoint combinator 是实打实的产生一个不动点
  • bad 只是通过一个 constructor 封装一层。其 self-application 的 driver code 要归功于那个特化的 applySelf .
九，二六