[Agda] mutual strangeness

[Nils Anders Danielsson]

On 2009-01-31 21:44, Thorsten Altenkirch wrote:
>
> it seems that constructors are not visible in the types of mutually
> defined functions.

Right. Let us say that we have n mutually recursive definitions (types
or functions)

  D₁ : T₁ = d₁, …, D_n : T_n = d_n.

Then D_i is in scope in T_(i+1), …, T_n and all the d_j. Any
constructors defined in d_i are in scope in the type signatures of
later constructors in d_i plus in d_(i+1), …, d_n. I believe these
restrictions are intended to rule out any definition with a type which
depends (too strongly) on the definition itself. Furthermore, in order
to avoid evaluating something which has not been type checked yet, the
name D_i is treated as a neutral term when all the T_j and d₁, …, d_i
are type checked.

These restrictions can perhaps be relaxed or modified, though.

> [...] one can just define an auxilliary function to overcome this
> restriction.

Not quite. You cannot pattern match on the constructor until it is in
scope. Consider the following example:

  mutual

    data A : Set where
      a₁ : A
      a₂ : C a₁ → A

    a₁′ : A
    a₁′ = a₁

    data B : A → Set where
      b : {x : A} → C x → B x

    f : (x : A) → B x
    f a₁     = b c₁′
    f (a₂ x) = b ?       -- Impossible to split x,
                         -- because c₁ is not in scope.

    data C : A → Set where
      c₁ : C a₁
      c₂ : C (a₂ c₁)

    c₁′ : C a₁′
    c₁′ = c₁

Note also that the auxiliary functions corresponding to a₂ and b above
can not be defined until after the definition of C, because their type
signatures mention C.

One could perhaps let a constructor name stand for the corresponding
auxiliary function from the first point in which the function can be
defined until the constructor has come into scope. However, this rule is
quite complicated. A better alternative might be to try to come up with
new rules for mutually recursive definitions, preferably both flexible
and easy to understand.

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