[Agda] Generic Programming with Indexed Functors

[Andrea Vezzosi]

As far as I understand the problem is the last line:

    ⟦ Iso C D e ⟧ r o = D r o

Semantically we know from 'e' that 'D' must be isomorphic to a
container but to the positivity checker it's just an arbitrary
function '(I -> Set) -> (O -> Set)' so it is unknown whether it is
strictly positive or not.

As long as positivity is something only an external oracle can certify
we will have problems like this.

By the way, If you look at the code bundle linked from the paper

http://dreixel.net/research/code/gpif.tar.gz

the module IxFun where this universe is defined starts by disabling
the positivity and termination checkers, so the version of Agda
doesn't seem to matter.

Best,
Andrea

On Thu, Jan 7, 2016 at 5:03 AM, Martin Stone Davis
<martin.stone.davis at gmail.com> wrote:
> {-
> The fixed-point definition in section 2.3 of Generic Programming with
> Indexed Functors no longer type-checks in the latest version of Agda, which
> complains that μ is not strictly positive:
>
>   data μ {I O : Set} (F : (I ⊎ O) ▶ O) (r : Indexed I) (o : O) : Set where
>     ⟨_⟩ : ⟦ F ⟧ (r ∣ μ F r) o → μ F r o
>
> I haven't had any luck finding a workaround. The code below is ripped from
> the article and reproduces the problem I'm having. Thanks in advance for any
> help solving this.
> -}
>
> module IndexedFunctor where
>   open import Function using (_∘_)
>   open import Relation.Binary.Core using (_≡_)
>
>   open import Data.Empty using (⊥)
>   open import Data.Unit using (⊤ ; tt)
>
>   open import Data.Product using (_×_ ; ∃)
>   open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
>
>   Indexed : Set → Set₁
>   Indexed I = I → Set
>
>   _▷_ : Set → Set → Set₁
>   I ▷ O = Indexed I → Indexed O
>
>   record _≃_ (A B : Set) : Set where
>     field
>       from : A → B
>       to   : B → A
>       iso₁ : ∀ {x} → to (from x) ≡ x
>       iso₂ : ∀ {x} → from (to x) ≡ x
>
>   _∣_ : ∀ {A B} → Indexed A → Indexed B → Indexed (A ⊎ B)
>   _∣_ ia _ (inj₁ x) = ia x
>   _∣_ _ ib (inj₂ x) = ib x
>
>   mutual
>     data _▶_ : Set → Set → Set₁ where
>       Z      : ∀ {I O} → I ▶ O
>       U      : ∀ {I O} → I ▶ O
>       I      : ∀ {I O} → I → I ▶ O
>       !      : ∀ {I O} → O → I ▶ O
>       _⊕_    : ∀ {I O}   → I ▶ O → I ▶ O → I ▶ O
>       _⊗_    : ∀ {I O}   → I ▶ O → I ▶ O → I ▶ O
>       _⊚_    : ∀ {I M O} → M ▶ O → I ▶ M → I ▶ O
>       _↗_↘_  : ∀ {I I' O O'} → I' ▶ O' → (I' → I) → (O → O') → I ▶ O
>       Fix    : ∀ {I O} → (I ⊎ O) ▶ O → I ▶ O
>       ∑      : ∀ {I O} → {C : ⊥ ▶ ⊤} → (⟦ C ⟧ (λ _ → ⊤) tt → I ▶ O) → I ▶ O
>       Iso    : ∀ {I O} → (C : I ▶ O) → (D : I ▷ O) → ((r : Indexed I) → (o :
> O) → D r o ≃ ⟦ C ⟧ r o) → I ▶ O
>
>     data μ {I O : Set} (F : (I ⊎ O) ▶ O) (r : Indexed I) (o : O) : Set where
>       ⟨_⟩ : ⟦ F ⟧ (r ∣ μ F r) o → μ F r o
>
>     ⟦_⟧ : ∀ {I O} → I ▶ O → I ▷ O
>     ⟦ Z         ⟧ r o = ⊥
>     ⟦ U         ⟧ r o = ⊤
>     ⟦ I i       ⟧ r o = r i
>     ⟦ F ↗ f ↘ g ⟧ r o = ⟦ F ⟧ (r ∘ f) (g o)
>     ⟦ F ⊕ G     ⟧ r o = ⟦ F ⟧ r o ⊎ ⟦ G ⟧ r o
>     ⟦ F ⊗ G     ⟧ r o = ⟦ F ⟧ r o × ⟦ G ⟧ r o
>     ⟦ F ⊚ G     ⟧ r o = ⟦ F ⟧ (⟦ G ⟧ r) o
>     ⟦ Fix F     ⟧ r o = μ F r o
>     ⟦ ! o'      ⟧ r o = o ≡ o'
>     ⟦ ∑ f       ⟧ r o = ∃ (λ i → ⟦ f i ⟧ r o)
>     ⟦ Iso C D e ⟧ r o = D r o
>
> --
> Martin Stone Davis
>
> Postal/Residential:
> 1223 Ferry St
> Apt 5
> Eugene, OR 97401
> Talk / Text / Voicemail: (310) 699-3578
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>