[Agda] Dealing with HOAS

[Carsten Schuermann]

or, check out Twelf ...

-- Carsten

Nils Anders Danielsson wrote:
> 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.
>