[Agda] An exercise in typing

[Jason Hu]

Hi Roman,

Interesting challenge. I give my shot for the first part, which encodes the type of functions in this pattern. The idea is to use cps to avoid use of any data structure other than natural numbers:


naryP : ℕ → Set₁
naryP zero    = Set
naryP (suc n) = Set → naryP n

naryf-go : Set → (Set → Set) → ∀ n → naryP n
naryf-go Q f zero    = f Q
naryf-go Q f (suc n) = λ A → naryf-go Q (λ x → f (A → x)) n

naryf : Set → ∀ n → naryP n
naryf Q n = naryf-go Q (λ x → x) n

RecN-go : ∀ n → (Set → naryP n) → Set₁
RecN-go zero f    = {R : Set} → ({Q : Set} → f Q → Q) → f R → R
RecN-go (suc n) f = {A : Set} → RecN-go n λ R → f R A

RecN : ℕ → Set₁
RecN n = RecN-go n λ Q → naryf Q n

I believe the body can be implemented in a similar manner.


From: Roman<mailto:effectfully at gmail.com>
Sent: Sunday, June 12, 2022 12:12 PM
To: Agda<mailto:Agda at lists.chalmers.se>
Subject: [Agda] An exercise in typing

Hi,

I stumbled upon a funny challenge some time ago and wanna share the
essential part of it.

Can you define `recN` that computes like this:

    recN 0 ~>* λ k f -> f
    recN 1 ~>* λ k f -> f (k λ x -> x)
    recN 2 ~>* λ k f -> f (k λ x y -> x) (k λ x y -> y)
    recN 3 ~>* λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)
    ...

where `x`, `y` and `z` all have different implicitly bound types.

If that doesn't sound hard enough, here's an additional condition:
don't use any `data` or `record` types (tuples included) apart from
the type of natural numbers.

If you're curious where the functions that `recN` computes to arise
from, they're a part of the "Unraveling recursion: compiling an IR
with recursion to System F" paper [1].

The challenge template with full details can be found here:
https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda

Copy the file and replace

    postulate
      kitRecN : KitRecN

with an actual definition of `kitRecN`.

Hope I'm not alone thinking it's a funny challenge.

--------------------

[1] https://files.zotero.net/eyJleHBpcmVzIjoxNjU1MDQzNzQ3LCJoYXNoIjoiNTUwYjc1ZjVkNGYyNzVlMjQ2OWNhMWIxYjUxODkyZTAiLCJjb250ZW50VHlwZSI6ImFwcGxpY2F0aW9uXC9wZGYiLCJjaGFyc2V0IjoiIiwiZmlsZW5hbWUiOiJLaXJlZXYgZXQgYWwuIC0gMjAxOSAtIFVucmF2ZWxpbmcgcmVjdXJzaW9uIGNvbXBpbGluZyBhbiBJUiB3aXRoIHJlY3Vyc2kucGRmIn0%3D/355301e3f049d523f8705af363927604bca986aed61c7c350fddc70a5e70f109/Kireev%20et%20al.%20-%202019%20-%20Unraveling%20recursion%20compiling%20an%20IR%20with%20recursi.pdf
_______________________________________________
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/20220612/de7daa10/attachment.html>