<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><div><span>If you try to write fold for CN, and then try to define _+_ as a fold in the usual way, you'll fail right away. If you try to patch it up, you either get the same error, or you get a Set-omega error. Probably nothing you can do about this, tho.</span></div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; "><div style="background-color: transparent; ">fold : {A : Set} → A → (A → A) → Cℕ → A</div><div style="background-color: transparent; ">fold z s n = n z s</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">suc : Cℕ → Cℕ</div><div style="background-color: transparent; ">suc n z s = s (n z s)</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">_+′_ :
Cℕ → Cℕ → Cℕ</div><div style="background-color: transparent; ">m +′ n = fold n suc m</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">yields a type error because suc is obviously the wrong type. I'm not sure there's any way to translate it naturally into this form. Certainly it would be lovely if you could: you could implement a language without having to deal with inductive types ever. But levels and such.</div></div><div></div><div> </div><div>- darryl</div></div> <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <hr size="1"> <font size="2" face="Arial"> <b><span style="font-weight:bold;">From:</span></b> Nils Anders Danielsson <nad@cse.gu.se><br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams <psygnisfive@yahoo.com>
<br><b><span style="font-weight: bold;">Cc:</span></b> agda list <agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Friday, June 28, 2013 5:28 AM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re: [Agda] More universe polymorphism<br> </font> </div> <div class="y_msg_container"><br>On 2013-06-28 01:09, Darryl McAdams wrote:<br>> I've certainly run into issues with levels. A good example is an<br>> implementation of Scott/Church encodings. You can define the encoding,<br>> but trying to define simple things like addition becomes difficult if<br>> not impossible, from what I can tell.<br><br>Are you referring to some kind of universe-polymorphic Church numerals?<br>The basic encoding works fine (for addition, at least):<br><br>module Church where<br><br>open import Data.Nat using (ℕ; zero; suc)<br>open import Relation.Binary.PropositionalEquality<br><br>Cℕ : Set₁<br>Cℕ = {A : Set} →
A → (A → A) → A<br><br>toℕ : Cℕ → ℕ<br>toℕ n = n zero suc<br><br>fromℕ : ℕ → Cℕ<br>fromℕ zero = λ z s → z<br>fromℕ (suc n) = λ z s → s (fromℕ n z s)<br><br>toℕ-fromℕ : ∀ n → toℕ (fromℕ n) ≡ n<br>toℕ-fromℕ zero = refl<br>toℕ-fromℕ (suc n) = cong suc (toℕ-fromℕ n)<br><br>_+_ : Cℕ → Cℕ → Cℕ<br>m + n = λ z s → m (n z s) s<br><br>+-correct : ∀ m n → toℕ (fromℕ m + fromℕ n) ≡ m Data.Nat.+ n<br>+-correct zero n = toℕ-fromℕ n<br>+-correct (suc m) n = cong suc (+-correct m n)<br><br>-- <br>/NAD<br><br><br></div> </div> </div> </div></body></html>