[Agda] More universe polymorphism
Darryl McAdams
psygnisfive at yahoo.com
Sat Jun 29 12:40:14 CEST 2013
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.
fold : {A : Set} → A → (A → A) → Cℕ → A
fold z s n = n z s
suc : Cℕ → Cℕ
suc n z s = s (n z s)
_+′_ : Cℕ → Cℕ → Cℕ
m +′ n = fold n suc m
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.
- darryl
________________________________
From: Nils Anders Danielsson <nad at cse.gu.se>
To: Darryl McAdams <psygnisfive at yahoo.com>
Cc: agda list <agda at lists.chalmers.se>
Sent: Friday, June 28, 2013 5:28 AM
Subject: Re: [Agda] More universe polymorphism
On 2013-06-28 01:09, Darryl McAdams wrote:
> I've certainly run into issues with levels. A good example is an
> implementation of Scott/Church encodings. You can define the encoding,
> but trying to define simple things like addition becomes difficult if
> not impossible, from what I can tell.
Are you referring to some kind of universe-polymorphic Church numerals?
The basic encoding works fine (for addition, at least):
module Church where
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.PropositionalEquality
Cℕ : Set₁
Cℕ = {A : Set} → A → (A → A) → A
toℕ : Cℕ → ℕ
toℕ n = n zero suc
fromℕ : ℕ → Cℕ
fromℕ zero = λ z s → z
fromℕ (suc n) = λ z s → s (fromℕ n z s)
toℕ-fromℕ : ∀ n → toℕ (fromℕ n) ≡ n
toℕ-fromℕ zero = refl
toℕ-fromℕ (suc n) = cong suc (toℕ-fromℕ n)
_+_ : Cℕ → Cℕ → Cℕ
m + n = λ z s → m (n z s) s
+-correct : ∀ m n → toℕ (fromℕ m + fromℕ n) ≡ m Data.Nat.+ n
+-correct zero n = toℕ-fromℕ n
+-correct (suc m) n = cong suc (+-correct m n)
--
/NAD
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130629/95ad594c/attachment.html
More information about the Agda
mailing list