<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Hi Roman,</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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:</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryP : </span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""> → Set</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New""><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryP zero = Set<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryP (suc n) = Set → naryP n<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryf-go : Set → (Set → Set) →
</span><span style="font-family:"Cambria Math",serif">∀</span><span style="font-family:"Courier New""> n → naryP n<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryf-go Q f zero = f Q<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryf-go Q f (suc n) = λ A → naryf-go Q (λ x → f (A → x)) n<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryf : Set → </span>
<span style="font-family:"Cambria Math",serif">∀</span><span style="font-family:"Courier New""> n → naryP n<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">naryf Q n = naryf-go Q (λ x → x) n<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">RecN-go : </span><span style="font-family:"Cambria Math",serif">∀</span><span style="font-family:"Courier New""> n → (Set → naryP n) → Set</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New""><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">RecN-go zero f = {R : Set} → ({Q : Set} → f Q → Q) → f R → R<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">RecN-go (suc n) f = {A : Set} → RecN-go n λ R → f R A<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">RecN : </span><span style="font-family:"Cambria Math",serif">ℕ</span><span style="font-family:"Courier New""> → Set</span><span style="font-family:"Cambria Math",serif">₁</span><span style="font-family:"Courier New""><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">RecN n = RecN-go n λ Q → naryf Q n<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">I believe the body can be implemented in a similar manner. </p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:effectfully@gmail.com">Roman</a><br>
<b>Sent: </b>Sunday, June 12, 2022 12:12 PM<br>
<b>To: </b><a href="mailto:Agda@lists.chalmers.se">Agda</a><br>
<b>Subject: </b>[Agda] An exercise in typing</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Hi,<br>
<br>
I stumbled upon a funny challenge some time ago and wanna share the<br>
essential part of it.<br>
<br>
Can you define `recN` that computes like this:<br>
<br>
recN 0 ~>* λ k f -> f<br>
recN 1 ~>* λ k f -> f (k λ x -> x)<br>
recN 2 ~>* λ k f -> f (k λ x y -> x) (k λ x y -> y)<br>
recN 3 ~>* λ k f -> f (k λ x y z -> x) (k λ x y z -> y) (k λ x y z -> z)<br>
...<br>
<br>
where `x`, `y` and `z` all have different implicitly bound types.<br>
<br>
If that doesn't sound hard enough, here's an additional condition:<br>
don't use any `data` or `record` types (tuples included) apart from<br>
the type of natural numbers.<br>
<br>
If you're curious where the functions that `recN` computes to arise<br>
from, they're a part of the "Unraveling recursion: compiling an IR<br>
with recursion to System F" paper [1].<br>
<br>
The challenge template with full details can be found here:<br>
<a href="https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda">https://github.com/effectfully/random-stuff/blob/master/RecN-challenge.agda</a><br>
<br>
Copy the file and replace<br>
<br>
postulate<br>
kitRecN : KitRecN<br>
<br>
with an actual definition of `kitRecN`.<br>
<br>
Hope I'm not alone thinking it's a funny challenge.<br>
<br>
--------------------<br>
<br>
[1] <a href="https://files.zotero.net/eyJleHBpcmVzIjoxNjU1MDQzNzQ3LCJoYXNoIjoiNTUwYjc1ZjVkNGYyNzVlMjQ2OWNhMWIxYjUxODkyZTAiLCJjb250ZW50VHlwZSI6ImFwcGxpY2F0aW9uXC9wZGYiLCJjaGFyc2V0IjoiIiwiZmlsZW5hbWUiOiJLaXJlZXYgZXQgYWwuIC0gMjAxOSAtIFVucmF2ZWxpbmcgcmVjdXJzaW9uIGNvbXBpbGluZyBhbiBJUiB3aXRoIHJlY3Vyc2kucGRmIn0%3D/355301e3f049d523f8705af363927604bca986aed61c7c350fddc70a5e70f109/Kireev%20et%20al.%20-%202019%20-%20Unraveling%20recursion%20compiling%20an%20IR%20with%20recursi.pdf">
https://files.zotero.net/eyJleHBpcmVzIjoxNjU1MDQzNzQ3LCJoYXNoIjoiNTUwYjc1ZjVkNGYyNzVlMjQ2OWNhMWIxYjUxODkyZTAiLCJjb250ZW50VHlwZSI6ImFwcGxpY2F0aW9uXC9wZGYiLCJjaGFyc2V0IjoiIiwiZmlsZW5hbWUiOiJLaXJlZXYgZXQgYWwuIC0gMjAxOSAtIFVucmF2ZWxpbmcgcmVjdXJzaW9uIGNvbXBpbGluZyBhbiBJUiB3aXRoIHJlY3Vyc2kucGRmIn0%3D/355301e3f049d523f8705af363927604bca986aed61c7c350fddc70a5e70f109/Kireev%20et%20al.%20-%202019%20-%20Unraveling%20recursion%20compiling%20an%20IR%20with%20recursi.pdf</a><br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>