データベースの定式化

スキーマ、タプル空間、タプルインスタンス、フィールド関数、テーブル

structure Schema where
  fields : Type
  typeAssig : fields → Type

def TupleSpace (S : Schema) := ((f : S.fields) → S.typeAssig f)

inductive NameAge where
|  name : NameAge
|  age : NameAge
deriving Repr

def Person : Schema := {
  fields := NameAge
  typeAssig := (λ| .name => String | .age => (Nat:Type))
}

#check TupleSpace Person

def personTaro : (TupleSpace Person) := 
 (λ| .name => "Taro" | .age => (21 :Nat) )
#eval personTaro .age

def personAkane : (TupleSpace Person) := 
 (λ| .name => "Akane" | .age => (25 :Nat) )

structure Person' where
  name : String
  age : Nat

def personTaro' : Person' := {
  name := "Taro"
  age := 21
}
#eval personTaro'.age

def getField (S : Schema ) (t : TupleSpace S) (f: S.fields) : 
   (S.typeAssig f) :=
t f
#eval getField Person personTaro NameAge.age

def Table (S : Schema) :Type := List (TupleSpace S)

def TaroAkane : Table Person := [
  personTaro,
  personAkane
]

#eval TaroAkane.map (λ p => p NameAge.age)

文字列または番号の有限集合としての列挙型をどうする？