通过乘积与矢量时保持函子正性

Question

在下面的代码中，μ₁ 的定义被 Agda 接受为严格正函子，这是有道理的。如果我通过产品打结，如 μ₂，它仍然被接受。但是，如果我尝试通过矢量，如 μ₃，它不再被接受。

data F : Set where
  X : F

⟦_⟧₁ : F → Set → Set
⟦ X ⟧₁ A = A

data μ₁ (f : F) : Set where
  Fix₁ : ⟦ f ⟧₁ (μ₁ f) → μ₁ f

open import Data.Product

⟦_⟧₂ : F → (Set × Set) → Set
⟦ X₁ ⟧₂ (A , _) = A

open import Data.Unit

data μ₂ (f : F) : Set where
  Fix₂ : ⟦ f ⟧₂ (μ₂ f , ⊤) → μ₂ f

open import Data.Nat
open import Data.Vec

⟦_⟧₃ : ∀ {n} → F → Vec Set (suc n) → Set
⟦ X ⟧₃ (A ∷ _) = A

data μ₃ (f : F) : Set where
  Fix₃ : ⟦ f ⟧₃ [ μ₃ f ] → μ₃ f

μ₃ 的错误消息是

μ₃ is not strictly positive, because it occurs
in the third argument to ⟦_⟧₃
in the type of the constructor Fix₃
in the definition of μ₃.

μ₂ 和 μ₃ 之间的根本区别是什么？有没有办法让像 μ₃ 这样的东西工作？

Answer 1

我主要是在猜测。 _×_ 是 record，Vec 是 data。当 _×_ 定义为 data:

时，Agda 拒绝 μ₂

data Pair (A B : Set₁) : Set₁
  where pair : A -> B -> Pair A B

⟦_⟧₃ : F → Pair Set Set → Set
⟦ X ⟧₃ (pair A _) = A

data μ₃ (f : F) : Set where     
  Fix₃ : ⟦ f ⟧₃ (pair (μ₃ f) ⊤) → μ₃ f

结果“μ₃ 不是严格正的，因为它发生了...”。但是如果你定义 ⟦_⟧₃ 为

⟦_⟧₃ : F → Pair Set Set → Set
⟦ X ⟧₃ _ = ⊤

或

⟦_⟧₃ : F → Pair Set Set → Set
⟦ _ ⟧₃ (pair A _) = A

然后一切正常（您的 μ₂ 有点误导，因为 F 上也没有模式匹配）。在第二种情况下，Agda 只是规范化表达式，因为第一个参数没有模式匹配，而第二个参数在 WHNF 中，所以 ⟦_⟧₃ 被完全消除。但我不知道，Agda 是如何解决第一个案例的。我想是临时的。

你的 μ₂ 类型检查，因为 Agda eliminates pattern matching on records:

map : {A B : Set} {P : A → Set} {Q : B → Set}
      (f : A → B) → (∀ {x} → P x → Q (f x)) →
      Σ A P → Σ B Q
map f g (x , y) = (f x , g y)

The clause above is internally translated into the following one:

map f g p = (f (Σ.proj₁ p) , g (Σ.proj₂ p))

所以就像

⟦_⟧₃ : F → Pair Set Set → Set
⟦ X ⟧₃ _ = ⊤

个案。

此外，如果您删除第一个参数的模式匹配，⟦_⟧₃ 将进行类型检查。

更新

不，这不是关于模式匹配消除，因为这个定义

data Pair (A B : Set₁) : Set₁
  where pair : A -> B -> Pair A B

fst : ∀ {A B} -> Pair A B -> A
fst (pair x y) = x

⟦_⟧₃ : F → Pair Set Set → Set
⟦ X ⟧₃ p = fst p

data μ₃ (f : F) : Set where     
  Fix₃ : ⟦ f ⟧₃ (pair (μ₃ f) ⊤) → μ₃ f

也被拒了

通过乘积与矢量时保持函子正性

Preserving functor positivity when going via product vs. vector

recursion

types

agda