RntzDatabase.agda

{-# OPTIONS --without-K #-}
module RtnzDatabase where

open import HoTT

Σ' = Σ -- renaming just so we can make the following syntax decl
syntax Σ' A (λ x → B) = ∃ x ∶ A · B

FinSet = Set -- not really constraining to finite, just conveying intent

postulate
  -- some imagined example base data types
  int : Set
  double : Set
  string : Set

{- We can declare a database in 'row-major representation',
   in which there is a set ρ of row labels, each element of which
   is mapped to the appropriate data... -}
rowT : Set₁
rowT = ∃ ρ ∶ FinSet · (ρ → (int × double × string))

{- Or in 'column-major' representation, in which we have three separate
   columns -}
colT : Set₁
colT = ∃ ρ ∶ FinSet · ((ρ → int) × (ρ → double) × (ρ → string))

-- The 'parametricity' you're talking about I would phrase as:
-- The row-major type admits a -factorization- through the function

rowMajorFor : Set → Set₁
rowMajorFor dataType = ∃ ρ ∶ FinSet · (ρ → dataType)

_ : rowT == rowMajorFor (int × double × string)
_ = idp

-- whereas the column-major type does not.

-- However, although arbitrarily pattern-matching on a type is
-- undesirable, we can without any trouble take a step back and
-- classify explicitly the information required to capture a
-- schema.

Schema : Set₁
Schema = ∃ κ ∶ FinSet · (κ → Set)

-- The type κ is the type whose elements are column labels.
-- From this define row-major and column-major representations of a schema:

rowMajorForSchema : Schema → Set₁
rowMajorForSchema (κ , f) = ∃ ρ ∶ FinSet · (ρ → (col : κ) → f col)

colMajorForSchema : Schema → Set₁
colMajorForSchema (κ , f) = ∃ ρ ∶ FinSet · ((col : κ) → ρ → f col)

-- I can make the factorization I'm talking about even more explicit now.
-- Given a schema, I can coalesce into a single type, the type of a row:

coalesce : Schema → Set
coalesce (κ , f) = (col : κ) → f col

-- and then it's true that

_ : rowMajorForSchema == rowMajorFor ∘ coalesce
_ = idp