module UniverseConstructions where open import Data.Bool open import Data.Nat open import Data.Nat.Show renaming (show to showℕ) open import Data.Product open import Data.String hiding (show) --show : {t : Set} → (v : t) → String --show {t} v = {!!} data Code : Set where BOOL NAT STRING : Code PAIR : Code → Code → Code ⟦_⟧ : Code → Set ⟦ BOOL ⟧ = Bool ⟦ NAT ⟧ = ℕ ⟦ STRING ⟧ = String ⟦ PAIR X Y ⟧ = ⟦ X ⟧ × ⟦ Y ⟧ show : {C : Code} → ⟦ C ⟧ → String show {BOOL} true = "true" show {BOOL} false = "false" show {NAT} n = showℕ n show {STRING} s = s show {PAIR A B} (a , b) = show a ++ " , " ++ show b -- Shamelessly ripped from David Christiansen's Talk @CurryOn'15 -- "Coding for Types: The Universe Pattern in Idris" data Type : Set where NAT BOOL : Type ⟪_⟫ : Type → Set ⟪ NAT ⟫ = ℕ ⟪ BOOL ⟫ = Bool data Expr : Type → Set where Cst : {t : Type} → ⟪ t ⟫ → Expr t Add : Expr NAT → Expr NAT → Expr NAT LeessEqThen : Expr NAT → Expr NAT → Expr BOOL eval : {t : Type} → Expr t → ⟪ t ⟫ eval (Cst x) = x eval (Add x y) = eval x + eval y eval (LeessEqThen x y) = {!!}