[Agda] Re: Generic Programming with Indexed Functors

[Martin Stone Davis]

I stopped work on re-implementing it when I became disheartened, finding
out that the original work was done by disabling the positivity and
termination checkers. I couldn't see a way to do it with those checkers
enabled.

--
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

On Sun, Jan 24, 2016 at 10:10 PM, Kenichi Asai <asai at is.ocha.ac.jp> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160125/e10d23df/attachment.html