[Agda] Re: Mixing = and ~

[Nils Anders Danielsson]

On 2008-11-20 15:26, Nils Anders Danielsson wrote:

> 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)

Andreas Abel implemented this extension during AIM 9, so now the code
above is accepted.

The definition of map above is a bit strange, since it uses both =
and ~. Mutual recursion/corecursion is perhaps easier to understand, and
the meaning of map (and other functions mixing = and ~) is defined by
translation into mutual recursion/corecursion:

   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) = rhs
     where rhs ~ c₀ (f x) (map f y)

-- 
/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.