[Agda] mutual strangeness

[Nils Anders Danielsson]

On 2009-02-02 14:42, Lennart Augustsson wrote:
> When it comes to ordering things, I prefer the computer to do menial
> tasks rather than imposing them on me.
> That's true for the whole mutual construct as well as what goes inside it.
> 
> I don't think reading is an issue.  I (with the help of Emacs) am
> capable of scanning the text in both directions for a definition.

There are several issues here:

* Scope: It would be nice if Agda performed the topological sort for us.
  When I describe code in a paper I do not always present definitions in
  dependency order, so it seems reasonable that I should not have to do
  so in Agda either (especially considering literate Agda). Perhaps it
  would aid readability if mutually recursive constructs were explicitly
  marked as such. The presence of meta-variables may complicate things,
  but does not seem like a show-stopper.

* Evaluation: When type checking mutually recursive definitions a
  function clause should not be evaluated before it has been type
  checked. James suggested that the order of the function clauses should
  be optimised automatically by the type checker, independently of the
  order imposed by the scope checker (unless I misunderstood something).
  I expressed a concern that this procedure could make it hard to
  understand why a particular piece of code is type correct. However,
  come to think of it, this does not seem much worse than the current
  situation with the termination checker, so maybe it would not be that
  bad (if we can implement it efficiently).

On a related note Ulf and I once played with the idea of lazy
type-checking: only type-check a term when you need to evaluate it, and
only as much of it as you need. Ulf even implemented a prototype. The
goal was to make it possible to handle "insanely dependent types":

  -- Reusable dependent contexts.
  data Ctxt (Ty : Ctxt Ty → Set) : Set where
    ∅   : Ctxt Ty
    _▻_ : (Γ : Ctxt Ty) → Ty Γ → Ctxt Ty

  -- An example of their use.
  data Ty : Ctxt Ty → Set where
    ℕ : ∀ {Γ} → Ty Γ
    Π : ∀ {Γ} (σ : Ty Γ) → Ty (Γ ▻ σ) → Ty Γ

I have no reason to believe that the resulting system is sound, but it
was fun to play with. :)

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