[Agda] Coinductive families

[Nicolas Pouillard]

On Tue, 5 Oct 2010 17:33:43 -0400, Dan Doel <dan.doel at gmail.com> wrote:
> On Tuesday 05 October 2010 3:56:17 pm Nicolas Pouillard wrote:
> 
> > I was also thinking that one could translate them away, namely using 'with'
> > on projections.
> > 
> > foo (true  , x) = e1
> > foo (false , x) = e2
> > 
> > would become
> > 
> > foo p with proj₁ p
> > ... | true   = e1[ x := proj₂ p ]
> > ... | false  = e2[ x := proj₂ p ]
> 
> This isn't quite good enough. For instance:
> 
>   Case : Set → Set → Bool → Set
>   Case T _ true  = T
>   Case _ F false = F
> 
>   foo : Σ Bool (Case Bool (Bool × Bool)) → Bool × Bool
>   foo p with proj₁ p
>   ... | true  = (proj₂ p , proj₂ p)
>   ... | false = proj₂ p
> 
> This fails, because the expression 'proj₂ p' doesn't have a type refined from 
> the match. We need to project them both at the same time:
> 
>   foo : Σ Bool (Case Bool (Bool × Bool)) → Bool × Bool
>   foo p with proj₁ p | proj₂ p
>   ... | true  | x = x , x
>   ... | false | x = x
> 
> And, in general, presumably project all the fields that will actually be used 
> in the same with clause.

OK, makes sense. So we agree that they can be translated away using 'with' on
all fields, but that would be equivalent that what we have know.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr