CODEWITHSUNDEEP
recursiontypesagda
Cactus
Cactus

Reputation: 27636

Preserving functor positivity when going via product vs. vector

In the following code, the definition of μ₁ is accepted by Agda as a strictly positive functor, which makes sense. If I tie the knot via a product, as in μ₂, it is still accepted. However, if I try to go via a vector, as in μ₃, it is not accepted anymore.

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

The error message for μ₃ is

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

What is the fundamental difference between μ₂ and μ₃? Is there a way to get something like μ₃ working?

Upvotes: 2

Views: 51

Answers (1)

effectfully
effectfully

Reputation: 12715

I'm mostly guessing. _×_ is a record and Vec is a data. Agda rejects μ₂, when _×_ is defined as a data:

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

Results in "μ₃ is not strictly positive, because it occurs...". But if you define ⟦_⟧₃ as

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

or

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

then everything is OK (your μ₂ is a bit misleading, since there is no pattern matching on F too). In the second case Agda just normalizes the expression, since there is no pattern matching on the first argument and the second is in the WHNF, so ⟦_⟧₃ is totally eliminated. But I don't know, how Agda resolves the first case. Something ad hoc, I suppose.

Your μ₂ typechecks, because 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))

So it's just like the

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

case.

Also, ⟦_⟧₃ will typecheck, if you remove pattern matching on the first argument.

UPDATE

No, it's not about pattern matching elimination, since this definition

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

is rejected too.

Upvotes: 2

Related Questions