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

[Nils Anders Danielsson]

On 2009-03-30 08:52, Carsten SchŸuermann wrote:

> tps : eval E V -> of E T -> of  V T -> type.
> 
> or
> 
> tps : {E:exp}eval E V -> of E T -> of  V T -> type.
> 
> or
> 
> tps : {E:exp}{V:exp}{T:exp}eval E V -> of E T -> of  V T -> type.
>
> Whichever option you choose, Twelf requires you to stick with your 
> choice.

Assuming that we have the definitions

  Ctxt : Set
  Ty   : Ctxt → Set
  Tm   : Ty Γ → Set  (meaning ∀ {Γ} → Ty Γ → Set)
  ⋆    : Ty Γ        (meaning ∀ {Γ} → Ty Γ),

does this mean that there is no direct way to write

  El : ∀ {Γ} → Tm (⋆ {Γ}) → Ty Γ  ?

The type

  Tm ⋆ → Ty Γ

ought to be generalised to

  ∀ {Δ Γ} → Tm (⋆ {Δ}) → Ty Γ

or

  ∀ {Γ Δ} → Tm (⋆ {Δ}) → Ty Γ,

neither of which is the intended type.

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