[Agda] Typed DeBruijn, typed Phoas, and untyped DeBruijn

[András Kovács]

Alternatively, we can postulate parametricity <http://lpaste.net/363029>
for PHOAS terms, and then the translation works without further cheating
(that's why it's "parametric", right?).

2018-02-28 19:45 GMT+01:00 Philip Wadler <wadler at inf.ed.ac.uk>:

> That worked perfectly!!! Thank you, Ulf! Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> On 28 February 2018 at 16:10, Ulf Norell <ulf.norell at gmail.com> wrote:
>
>>
>> On Wed, Feb 28, 2018 at 2:31 PM, Roman <effectfully at gmail.com> wrote:
>>
>>> The downside is that `agda-prelude` is not compatible with the standard
>>> library.
>>
>>
>> These days agda-prelude is compatible with the standard library. The only
>> wrinkle
>> is that the deriving Eq functionality gives you an implementation of the
>> agda-prelude
>> Eq record, but converting it to the standard library equivalent should be
>> straight-forward.
>>
>> In fact here's the code:
>>
>> \begin{code}
>> -- These two imports are from agda-prelude (https://github.com/UlfNorell/
>> agda-prelude)
>> open import Tactic.Deriving.Eq using (deriveEq)
>> import Prelude
>>
>> instance
>>   unquoteDecl EqType = deriveEq EqType (quote Type)
>>   unquoteDecl EqEnv  = deriveEq EqEnv  (quote Env)
>>
>> ⊥To⊥ : Prelude.⊥ → ⊥
>> ⊥To⊥ ()
>>
>> decToDec : ∀ {a} {A : Set a} → Prelude.Dec A → Dec A
>> decToDec (Prelude.yes x) = yes x
>> decToDec (Prelude.no nx) = no (⊥To⊥ ∘ nx)
>>
>> _≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
>> A ≟T B = decToDec (A Prelude.== B)
>>
>> _≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
>> Γ ≟ Δ = decToDec (Γ Prelude.== Δ)
>> \end{code}
>>
>> / Ulf
>>
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180301/152b9a83/attachment.html>