[Agda] Mixing = and ~

[Nils Anders Danielsson]

Hi,

Consider the following universe:

   data Kind : Set where
     μ : Kind
     ν : Kind

   data Tμ (A : Set) : Set where
     c₀ : (x : A) (y : Tμ A) -> Tμ A
     c₁ : Tμ A

   codata Tν (A : Set) : Set where
     c₀ : (x : A) (y : Tν A) -> Tν A

   T : Kind -> Set -> Set
   T μ = Tμ
   T ν = Tν

I would want to define a map function for this universe as follows:

   map : forall {k A B} -> (A -> B) -> T k A -> T k B
   map {μ} f (c₀ x y) = c₀ (f x) (map f y)
   map {μ} f c₁       = c₁
   map {ν} f (c₀ x y) ~ c₀ (f x) (map f y)

I want to mix = and ~ (recursion and corecursion) in order to make
things evaluate as much as possible. However, Agda currently does not
allow this. Would it be problematic to allow definitions like the one
above? The clauses containing = would evaluate freely, while ~ clauses
would only evaluate under a destructor. The termination checker would
also have to be tweaked: I think it is enough to restrict the use of
guardedness to those call sequences which cross a ~, at least for the
old foetus-style checker. Furthermore with clauses would be translated
into = clauses, since they are never (directly) guarded.

I believe that this question is mostly orthogonal to the long-standing
discussion about how to handle coinductive definitions; feel free to
rephrase it in terms of coalgebras.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.