[Agda] Generic Programming with Indexed Functors

[Martin Stone Davis]

{-
The fixed-point definition in section 2.3 of Generic Programming with
Indexed Functors
<https://www.researchgate.net/publication/228944016_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 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160106/a41be871/attachment.html