Simulating "type providers" in Agda

RuntimeTypes.agda

module RuntimeTypes where

open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Product.Pointwise using (_×-≟_)
open import Relation.Binary.List.Pointwise using (decidable-≡)

DecEq : ∀ {a} → Set a → Set a
DecEq A = Decidable {A = A} _≡_

-- A simple universe of database types. Flesh out if you care
data DbType : Set where
  integer string : DbType
  nullable : DbType → DbType

-- Note that we could make this a lot fancier and express database constraints that result in proofs of membership in another table!
⟦_⟧T : DbType → Set
⟦ integer ⟧T = ℤ
⟦ string ⟧T = String
⟦ nullable x ⟧T = Maybe ⟦ x ⟧T -- a real example might prevent this from being nested

-- Someday we'll get that reflection thing working, but for now I have to write this crap
eqT? : DecEq DbType
eqT? integer integer = yes refl
eqT? integer string = no (λ ())
eqT? integer (nullable y) = no (λ ())
eqT? string integer = no (λ ())
eqT? string string = yes refl
eqT? string (nullable y) = no (λ ())
eqT? (nullable x) integer = no (λ ())
eqT? (nullable x) string = no (λ ())
eqT? (nullable x) (nullable y) with eqT? x y
eqT? (nullable x) (nullable .x) | yes refl = yes refl
eqT? (nullable x) (nullable y) | no ¬p = no (λ x → ¬p (cong (λ { integer → integer; string → string; (nullable x) → x }) x))

-- A schema is a list of columns, each of which has a name and a type
record Schema : Set where
  constructor schema
  field
    fields : List (String × DbType)

-- Now let's get a real type representing our table. In a real setting, this wouldn't be reified in memory
-- but you'd be able to perform queries against it. But this should give you an idea
⟦_⟧S : Schema → Set
⟦ schema ts ⟧S = List (All (⟦_⟧T ∘ proj₂) ts) -- `All f` is roughly `HList . map f`

-- Are two schemas equal?
eqS? : DecEq Schema
eqS? (schema xs) (schema ys) with decidable-≡ (String._≟_ ×-≟ eqT?) xs ys
eqS? (schema xs) (schema .xs) | yes refl = yes refl
eqS? (schema xs) (schema  ys) | no ¬p = no (¬p ∘ cong Schema.fields)



employee : Schema
employee = schema (("id" , integer) ∷ ("name" , string) ∷ ("age" , integer) ∷ ("manager" , nullable integer) ∷ [])

-- You get the idea
sampleEmployees : ⟦ employee ⟧S
sampleEmployees = 
  (+ 0 ∷ "Nancy Drew"  ∷ + 16 ∷ nothing ∷ []) ∷
  (+ 1 ∷ "Frank Hardy" ∷ + 18 ∷ just (+ 0) ∷ []) ∷ []

-- ⟦ employee ⟧S basically expands to an HList containing:
-- "id" : ℤ , "name" ∶ String , "age" ∶ ℤ, "manager" ∶ Maybe ℤ

infixl 1 _>>=_ _>>_

postulate
  -- Not going to actually implement these
  IO : Set → Set
  putStrLn : String → IO ⊤ -- In paulp's honor
  exit : ∀ {A} → ℤ → IO A -- Doesn't return, so might as well be accurate
  getSchema : String → IO (Σ Schema ⟦_⟧S)

  _>>_  : ∀ {A B} → IO A → IO B → IO B
  _>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B


-- This function is super typesafe, and can assume a particular schema.
-- (we might have "nice" error cases in real life if the schema changes at runtime; can't escape concurrency)
myFancyEmployeeProcessingProgram : ⟦ employee ⟧S → IO ⊤ -- 
myFancyEmployeeProcessingProgram table =
  putStrLn "I'm really safe" >>
  putStrLn "or am I?" >>
  exit (+ 1)

-- This is Agda, so no do notation :(
main : IO ⊤
main = 
  putStrLn "hello!" >>
  getSchema "employee" >>= λ employeeSchema →
  case eqS? (proj₁ employeeSchema) employee of λ
    { (yes eq) → myFancyEmployeeProcessingProgram (subst ⟦_⟧S eq (proj₂ employeeSchema))
    ; (no ¬eq) → putStrLn "Sorry, the schema didn't match and I don't know what to do!" >> 
                 exit (- (+ 1)) -- Number syntax isn't one of Agda's strong points
    }

-- Note how this design forced us to deal with potential schema mismatches outside the actual processing code!
-- Concerns are separated, validation happens outside, then the hard actual work doesn't need to worry about
-- failed assertions and data validation.