[Agda] Coinductive families

[Dan Doel]

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.

-- Dan