[Agda] Re: Generic Programming with Indexed Functors

[Kenichi Asai]

Dear Martin,

It appears you are re-implementing the Indexed Functors using the Agda
standard library.  Do you make the code available somewhere?

-- 
Kenichi Asai


On Wed, Jan 06, 2016 at 08:03:35PM -0800,
 Martin Stone Davis 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