[Agda] Dealing with HOAS

[Jean-Philippe Bernardy]

On Fri, Sep 25, 2009 at 12:05 AM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> 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.

There is also PHOAS, which is a bit more lightweight. (Adam Chlipala,
Parameterized Higher Order Abstract Syntax for Mechanized Semantics).

I have started a translation of the paper in Agda:

http://github.com/jyp/topics/tree/73270760a7cf54ed25800219879d1f13bb993dd0/PHOAS

Cheers,
JP.