Multiverse.agda

module Multiverse where 


module types where 
    open import Data.Nat 
    open import Data.String 
    open import Data.Bool 
    open import Data.Product

    data Type₁ : Set where 
        𝕓 𝕟 𝕤 : Type₁

    El₁ : Type₁ → Set 
    El₁ 𝕓 = Bool
    El₁ 𝕟 = ℕ
    El₁ 𝕤 = String

    data Type₂ : Set where
        𝕓 𝕟 𝕤 : Type₂ 
        _&_ _⇒_ : Type₂ → Type₂ →  Type₂

    El₂ : Type₂ → Set 
    El₂ 𝕓 = Bool
    El₂ 𝕟 = ℕ
    El₂ 𝕤 = String
    El₂ (x & y) = El₂ x × El₂ y
    El₂ (x ⇒ y) = El₂ x → El₂ y

module univ where 
    -- note this is equivalent to Poly
    -- Poly can be seen as a datatype and a universe..
    record Univ : Set₁ where
        field
            U : Set
            El : U → Set
    open Univ

    -- fixes a universe, vs the multiverse definition
    -- this is an element of Poly
    record UniverseElement (𝒰 : Univ) : Set where 
        constructor _∋_
        field
            ty : 𝒰 .U 
            elem : (𝒰 .El) ty
    open UniverseElement

    ⟦_⟧ : Univ → Set 
    ⟦_⟧ = UniverseElement
    open import Data.Product
    open import Relation.Binary.PropositionalEquality
    open types

 


    𝒰₁ : Univ 
    𝒰₁ .U = Type₁
    𝒰₁ .El = El₁

    𝒰₂ : Univ
    𝒰₂ .U = Type₂
    𝒰₂ .El = El₂


       -- set of universe elements with a particual type
    pick : {𝒰 : Univ} → (type : 𝒰 .U ) → Set
    pick {𝒰} type = Σ ⟦ 𝒰 ⟧ (λ e → ty e ≡ type)

    _ : pick {𝒰₂} (𝕓 ⇒ 𝕓)
    _ = ((𝕓 ⇒ 𝕓) ∋ λ b → b) , refl

    open import Data.Nat

    _ : ⟦ 𝒰₂ ⟧
    _ = ((𝕟 & 𝕟) ⇒ 𝕟) ∋ λ{(n , m) → n + m}
    
    data ⊥ : Set where
    data ⊤ : Set where tt : ⊤

    {-
    nary' : ℕ → Univ → Set 
    nary' zero 𝒰 =  𝒰 .U --⟦ 𝒰 ⟧
    nary' (suc n) 𝒰 = 𝒰 .U × nary' n 𝒰 --⟦ u ⟧ × nary' n u

    nary : ℕ → Univ → Set 
    nary zero 𝒰 = ⊤
    nary (suc n) 𝒰 = nary' n 𝒰

    _ : nary 3 𝒰₁ 
    _ = 𝕓 , (𝕓 , 𝕟)
    -}
    open import Data.Product
    open import Data.Bool
    nary' : ℕ → Univ → Set 
    nary' zero 𝒰 = ⟦ 𝒰 ⟧
    nary' (suc x) 𝒰 = ⟦ 𝒰 ⟧ × nary' x 𝒰

    nary : ℕ → Univ → Set 
    nary zero 𝒰 = ⊤
    nary (suc n) 𝒰 = nary' n 𝒰

    record DSL (𝒰 : Univ) : Set where 
        field 
            ℱ : ∀(n : ℕ) → nary n 𝒰 → ⟦ 𝒰  ⟧

    open DSL
    
    hmm : DSL 𝒰₂ 
    hmm .ℱ zero x = {!   !}
    hmm .ℱ (suc n) x = {! x  !}





module multi where 
    record Univ : Set₁ where
        field
            U : Set
            El : U → Set
    open Univ

    record MultiverseElement : Set₁ where
        constructor _∋_∋_
        field
            𝒰 : Univ
            ty : 𝒰 .U
            elem : (𝒰 .El) ty


    open import Data.Nat
    open import Data.String
    open import Data.Bool
    open import Function hiding (_∋_)

    data Types₁ : Set where 𝕓 𝕟 : Types₁
    data Types₂ : Set where
        𝕤 : Types₂
        _⇒_ : Types₂ → Types₂ → Types₂

    U₁ : Univ
    U₁ .U = Types₁
    U₁ .El 𝕓 = Bool
    U₁ .El 𝕟 = ℕ

    U₂ : Univ
    U₂ .U = Types₂
    U₂ .El = El'
        where 
            El' : Types₂ → Set
            El' 𝕤 = String
            El' (x ⇒ y) = El' x → El' y


    ex : MultiverseElement
    ex = U₂ ∋ (𝕤 ⇒ 𝕤) ∋ (λ s → s ++ "foo")


    ex2 : MultiverseElement
    ex2 = U₁ ∋ 𝕓 ∋ false