[Agda] Why aren't free vars in types automatically generalized

[Nils Anders Danielsson]

On 2009-03-28 03:42, Stefan Monnier wrote:
> Coming from Twelf and ML, I keep wondering why I have to write:
> 
>    data Ω : ℕ → Set where
>      tNat  : ∀{l} → Ω l
>      tArw  : ∀{l} → Ω l → Ω l → Ω l
>      tPoly : ∀{l} → Ω (suc l) → Ω l
>      tVar  : ∀{l} → Fin l → Ω l
> 
> rather than
> 
>    data Ω : ℕ → Set where
>      tNat  : Ω l
>      tArw  : Ω l → Ω l → Ω l
>      tPoly : Ω (suc l) → Ω l
>      tVar  : Fin l → Ω l

I agree that it is often annoying to write out all the implicit
arguments in a type signature. There are several reasons not to
introduce the short-hand notation you suggest, though:

⑴ If something called l were to come into scope, then your program would
  be broken. Hopefully you would get a type error, but not in all cases.

⑵ What should the inferred implicit arguments be called? In your case it
  is obvious, but what if l depended on something else? Note that you
  can give implicit arguments by name when applying a function, so the
  names matter:

    f {A = …} x

⑶ Similarly, if several independent arguments are added, in which order
  should they appear in the type signature?

When implementing this I suppose the general idea is to 

  • take all variables which are not in scope in a type signature,
  • collect all their constraints (probably just locally inside the type
    signature), and then
  • "close the context" by introducing as few new variables as possible
    ◦ without introducing any new constraints (so if x and y both have
      type T whatever, there should be two new variables for whatever),
      and
    ◦ without introducing unnecessary generality (so that ∀ x → T x → …
      is preferred to (∀ x → T x) → …).

This description is very vague, and I would not be surprised if I had
missed some design choice or potential problem. Has anyone worked out
the details? Would the algorithm be obvious to users of the language?

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