stefan-hoeck / idris2-sqlite3

Idris2 bindings to the sqlite3 C-API
BSD 3-Clause "New" or "Revised" License
3 stars 1 forks source link

[ new, refactor ] flattening marshallers #28

Closed stefan-hoeck closed 9 months ago

stefan-hoeck commented 9 months ago

With this change, interfaces FromRow and ToRow get much more versatile, as they allow us now to not only convert record types to rows if all fields have a ToCell and FromCell interface, but also when all fields have a ToRow and FromRow implementation.

This allows us to store record fields in marshallable record fields, so that everything is flattened out when going to the database. It also allows us to use parameterized types with placeholders such as unit to mark values to be auto-generated when inserting, and correctly read them when collecting data.

I'll do some more experiments and will then add another part to the tutorial to show the advantages in more detail.

Implementing this was satisfyingly simple: Dependent types helped a lot here.