Fin Closure

FinClosure.agda

module FinClosureEx where
open import Agda.Primitive
open import Data.Bool
open import Data.Fin
open import Data.List
open import Data.Nat
open import Data.Product
open import Function.Base

private
  variable
    U : Set₀

{-
    Mutually dependent definitions FinClosure and El
        FinClosure represent the high level type formers that are allowed in our language
            here just 
                types, sigma types, and pi types
        El stands for Element, it lets us construct elements of a type (under some interpretation P)
-}
data FinClosure {U : Set₀} (P : U → Set₀) : Set₁

El : {P : U → Set₀} → FinClosure P → Set₀

data FinClosure {U = U} P where
  Ty : (u : U) → FinClosure P
  ΣF : (A : FinClosure P) → (El A → FinClosure P) → FinClosure P
  ΠF : (A : FinClosure P) → (El A → FinClosure P) → FinClosure P
  _⊗_ : FinClosure P → FinClosure P → FinClosure P
  _⇒_ : FinClosure P → FinClosure P → FinClosure P
  list : FinClosure P → FinClosure P

El {P = P} (Ty u) = P u
El (ΣF A B)       = Σ (El A) (El ∘ B)
El (ΠF A B)       = (a : El A) → El (B a)
El {P = P}(A ⊗ B) =  El A × El B  
El {P = P}(A ⇒ B) =  El A → El B 
El {P = P}(list A) =  List (El A)


-- We can enumerate our Base types here
data BaseTypes : Set₀ where  -- Should remove parameterized types from here and put then in the Fin Closure
    nat : BaseTypes
    bool : BaseTypes


-- interp maps our base types into actual types in Set
⦅_⦆ : BaseTypes → Set₀
⦅ nat ⦆ = ℕ 
⦅ bool ⦆ = Bool 

-- We call our "universe" of types Type, and give it the interpretation `interp`
Type : Set₁
Type = FinClosure ⦅_⦆

⟦_⟧ : Type → Set
⟦_⟧ = El 

prod : Type -- sigma product type
prod = ΣF (Ty nat) (λ _ → Ty bool)

prod₁ : Type -- regular product type
prod₁ = (Ty nat) ⊗ (Ty bool)


_ : ⟦ prod ⟧ 
_ = 4 , true

-- some examples
tynat : Type
tynat = Ty nat

n : ⟦ tynat ⟧ 
n = 3

tylist : Type
tylist = list (Ty bool)

bs : ⟦ tylist ⟧
bs = true ∷ false ∷ true ∷ []

-- pattern matching on types
natToBool : Type → Type 
natToBool (Ty nat) = Ty bool  
natToBool x = x

_ : ⟦ natToBool tynat ⟧
_ = true

_ : ⟦ Ty nat ⇒ Ty bool ⟧
_ = λ n → true

https://agda.readthedocs.io/en/v2.6.2.1/language/mutual-recursion.html

Not quite phoas