Create a gist now

Instantly share code, notes, and snippets.

Currying using a Universe
module Currying where
open import Level
open import Data.Product as P using (_×_ ; _,_)
open import Function
data Universe (ℓ : Level) : Set (suc ℓ) where
set : (A : Set ℓ) Universe ℓ
_**_ : (u₁ u₂ : Universe ℓ) Universe ℓ
⟦_⟧ : {ℓ : Level} (u : Universe ℓ) Set ℓ
⟦ set A ⟧ = A
⟦ u₁ ** u₂ ⟧ = ⟦ u₁ ⟧ × ⟦ u₂ ⟧
⟦_⟧→_ : {ℓ : Level} (u : Universe ℓ) (R : Set ℓ) Set ℓ
⟦ set A ⟧→ R = A R
⟦ u₁ ** u₂ ⟧→ R = ⟦ u₁ ⟧→ (⟦ u₂ ⟧→ R)
curry : {ℓ : Level} (u : Universe ℓ) {R : Set ℓ} (f : ⟦ u ⟧ R) ⟦ u ⟧→ R
curry (set A) f = f
curry (u₁ ** u₂) f = curry u₁ $ λ v₁
curry u₂ $ λ v₂
f (v₁ , v₂)
uncurry : {ℓ : Level} (u : Universe ℓ) {R : Set ℓ} (f : ⟦ u ⟧→ R) ⟦ u ⟧ R
uncurry (set A) f = f
uncurry (u₁ ** u₂) f = P.uncurry $ λ v₁ v₂ uncurry u₂ (uncurry u₁ f v₁) v₂
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment