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

[Philip Wadler]

Andras,  Thank you very much for your note [1]. Your proof appears related
to the wf relation of Chlipala [2,3]. One difference is that yours is unary
whereas his is binary, so I would expect his is more powerful, or do you
think they have equal power? Yours, -- P

[1] http://lpaste.net/363029
[2] http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html#HigherOrder.Wf
[3] http://adam.chlipala.net/cpdt/html/Intensional.html

.   \ 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 1 March 2018 at 23:54, András Kovács <kovacsahun at hotmail.com> wrote:

> 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/20180304/9533eb62/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180304/9533eb62/attachment.ksh>