[Agda] Coinductive families

[Andreas Abel]

On Oct 4, 2010, at 10:45 AM, Dan Doel wrote:

> On Monday 04 October 2010 4:04:19 am Andreas Abel wrote:
>
>> It comes natural then to extend pattern matching to destructor
>> patterns, so the constructor is creating an object defined by its
>> observations.
>>
>>   cons : .{A : Set} -> A -> Stream A -> Stream A
>>   head (cons a as) = a
>>   tail (cons a as) = as
>
> Yes, I've seen that before, and it's what I expected. I hadn't fully  
> thought
> through the corecursive definition angle, though, so I elided it.
>
> I suppose another piece of the puzzle is that refinements happen in  
> certain
> cases with indexed records/coinductive families:
>
>  data Fin : Nat -> Set where
>    zero : .{n : Nat} -> Fin (suc n)
>    suc  : .{n : Nat} -> Fin n -> Fin (suc n)
>
>  codata Cofin : Nat -> Set where
>    pred  : .{n : Nat} -> Cofin (suc n) -> Maybe (Cofin n)
>    empty : Cofin 0 -> Bot
>
>  inject : .{n : Nat} -> Fin n -> Cofin n
>  -- in the first two cases, n = suc m, refined by pred
>  pred  (inject zero)    = nothing
>  pred  (inject (suc i)) = just (inject i)
>  -- in this case, n = 0, refined by empty
>  empty (inject ())
>
> or, in more generality:
>
>  ana : .{F : Nat -> Set} -> (F 0 -> Bot)
>                          -> (.{n : Nat} -> F (suc n) -> Maybe (F n))
>      -> .{n : Nat} -> F n -> Cofin n
>  -- pred (ana e p f) = mapMaybe (ana e p) (p f)?
>  -- Would that pass a syntactic productivity check? I'm not entirely  
> sure
>  -- what the criteria would be.

To get this productivity check, I am doing my research on sized  
types.  I have ideas how to adapt them to destructor patterns, and  
when I am finished, the answer is yes!

>  pred  (ana e p f) with p f
>  ... | nothing = nothing
>  ... | just f' = just (ana e p f')
>  empty (ana e _ f) = e f
>
> -- Dan
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/