[Agda] Dealing with HOAS

[Nils Anders Danielsson]

On 2009-09-24 20:36, Vag Vagoff wrote:
> data Exp : Typ → Set where
> val : ∀ {t} → Val t → Exp t
> lam : ∀ {t₁ t₂} → (Exp t₁ → Exp t₂) → Exp (t₁ ⟶ t₂)
> app : ∀ {t₁ t₂} → Exp (t₁ ⟶ t₂) → Exp t₂ → Exp t₁
> 
> How to hack this representation to get rid of error?

You can only define strictly positive types in Agda (unless you turn off
the positivity checker).

You may want to check out "A Universe of Binding and Computation" by Dan
Licata and Bob Harper. This paper describes a language, embedded in
Agda, which supports both functions-as-computation and
functions-as-data.

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