Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Yet another Dhall-API-protocol proposal
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
})
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.