Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Simulating "type providers" in 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
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 _>>=_ _>>_
-- 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.