Structs

Structs is an Agda library that lets you use anonymous, ML-style records with convenient syntax. Mostly, it’s useful as a way to model records in formalisations of other languages which have records, as Agda records are nominally typed and dependent, so they’re not useful for this purpose.

You can construct records like so:

-- type can be stated as Struct _, for brevity.
test : Struct ( ("foo" , ℕ) ∷ ("bar" , Bool) ∷ ("baz" , Struct [ "msg" , String ] ) ∷ []) 
test = ⟨ "foo" ∶ 32 
       ∷ "bar" ∶ True 
       ∷ "baz" ∶ ⟨ "msg" ∶ "Hello, Structs!" ∷ [] ⟩
       ∷ [] 
       ⟩

Assign to them like so:

test′ : Struct _
test′ = test ∙ "bar" ≔ False

And read from them like so:

test″ : String
test″ = test′ ∙ "baz" ∙ "msg"

The three lemmas spurious-update, read-after-update and frame-inertia give you the ability to prove things about these record operations reasonably easily.

There’s also some advanced stuff that you probably don’t need, but if you want to concatenate records, we have append and its inverse drop-append, and the TypeChangingAssignment module has just that.

Have fun!

liamoc/structs

Structs