[Agda] Agda's coinduction incompatible with initial algebras

[Dan Doel]

On Thu, Oct 6, 2011 at 3:07 AM, Thorsten Altenkirch <txa at cs.nott.ac.uk> wrote:
>> I don't think this is true if you want a (typical) set theoretic
>> semantics. Fixed points of functors like:
>>
>>    K R A = (A -> R) -> R
>>
>> only exist in categories of domains and the like as I recall (and my
>> skimming of Matthes' paper didn't suggest any different). Assuming
>> anyone cares about that.
>
> We should stick to things we understand intuitively.

I frequently don't find the set theoretic models of type theoretic
features particularly intuitive. Should we get rid of
induction-recursion? I don't have any intuition for Mahlo cardinals.

> Anyway, who needs non-strict positive definitions?

I can't think of any particularly good uses, but this is cute:

{-# OPTIONS --no-positivity-check #-}

module NSP where

open import Data.Empty

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List A

foldr : ∀{A R : Set} → (A → R → R) → R → List A → R
foldr f z []        = z
foldr f z (x :: xs) = f x (foldr f z xs)

module Zip (A B C : Set) where

  data X : Set where
    roll : ((A → X → List C) → List C) → X

  Y : Set
  Y = A → X → List C

  unroll : X → Y → List C
  unroll (roll f) y = f y

  zipWith : (A → B → C) → List A → List B → List C
  zipWith f xs ys = unroll (foldr consA nilA xs) (foldr consB nilB ys)
   where
   nilA : X
   nilA = roll (λ _ → [])

   consA : A → X → X
   consA x xs = roll (λ k → k x xs)

   nilB : Y
   nilB = λ _ _ → []

   consB : B → Y → Y
   consB y ys = λ x xs → f x y :: unroll xs ys

It's asymptotically faster than the other method I know for writing
zipWith using foldr.

I think I have encountered other situations in which I wanted general
positive types. I don't have them on the top of my head, though.

-- Dan