Yet another Dhall-API-protocol proposal

sketch.dhall

let fold = https://prelude.dhall-lang.org/List/fold
let filter = https://prelude.dhall-lang.org/List/filter
let equal = https://prelude.dhall-lang.org/Natural/equal

let Obj = <User | Pet | List>
let Key = <Id | Type | Name | Pets | Head | Tail>
let Entry = <Int_: Integer | Bool_: Bool | Double_: Double | Text_: Text | Id_: Natural | Type_: Obj | Nil>
let Row = { ptr: Natural, key: Key, val: Entry }
let Db = List Row

let Reader: Type = forall (Projection: Type)
  -> forall (ProjectionF: Db -> Projection)
  -> Projection

let ReaderImpl: Reader = \(Projection: Type)
  -> \(ProjectionF: Db -> Projection)
  -> ProjectionF [
    {ptr=0, key=Key.Id, val=Entry.Id_ 0},
    {ptr=0, key=Key.Type, val=Entry.Type_ Obj.User},
    {ptr=0, key=Key.Name, val=Entry.Text_ "Mike"},
    {ptr=0, key=Key.Pets, val=Entry.Id_ 1},
    {ptr=1, key=Key.Type, val=Entry.Type_ Obj.List},
    {ptr=1, key=Key.Head, val=Entry.Id_ 10},
    {ptr=1, key=Key.Tail, val=Entry.Nil},
    {ptr=10, key=Key.Id, val=Entry.Id_ 10},
    {ptr=10, key=Key.Type, val=Entry.Type_ Obj.Pet},
    {ptr=10, key=Key.Name, val=Entry.Text_ "Fluffy"}
  ]

let getName: (Db -> Natural -> Text) = \(db: Db)
  -> \(ptr: Natural)
  -> fold
     Row
     (filter
       Row
       (\(a: Row) -> equal a.ptr ptr)
       db)
      Text
      (\(a: Row) -> \(t: Text) -> 
        merge {
          Id=t,
          Type=t,
          Name=merge {
            Int_=\(v: Integer) -> t,
            Bool_=\(v: Bool) -> t,
            Double_=\(v: Double) -> t,
            Text_=\(v: Text) -> v,
            Id_=\(v: Natural) -> t,
            Type_=\(v: Obj) -> t,
            Nil=t
          } a.val,
          Pets=t,
          Head=t,
          Tail=t
      } a.key) ""

let View = { name: Text }
in ReaderImpl
   View
   (\(db: Db) -> {
     name = getName db 0
   })