possible cell / column-delta generalization
cell-delta and column-delta infer the type of their column based on the available schemas. This works fine in the case where they're passed a concrete column ((column-delta table 'balance)), but we'd like to be able to do something like (defproperty (table-conserves-mass (table:table) (forall (column:(columns-of table)) (= 0 (column-delta table column)))).
We can't currently do this because column-delta is typechecked / inferred. This should work if the columns are all of the same type, but that's never going to be the case in the real world.
A possible solution is to allow column filtering, something in the spirit of: (forall (column:(columns-of table)) (=> (= (typeof column) integer) (= 0 (column-delta table column)))). This isn't bad, but has two problems that I see:
0is an integer literal. This is completely distinct from the decimal literal0.0. So you'd have to specify integers and decimals separately.- What's the type of
column? Well, it's justcolumn. But this would require the typechecker to have special info aboutcolumnwhen operating to the right of(= (typeof column) integer) =>. I don't think we want to pursue a design where the compiler has magical type info the user can't see.
Slightly further afield from the current design: (forall (column:(column-of integer)) (=> (member column table) (= 0 (column-delta table column)))). "For all integer-valued columns in table...". I like this more -- the type of column is static and specified (in a user-accessible way) up-front. This is what table-conserves-mass looks like:
(defproperty table-conserves-mass (table:table)
(forall (column:(column-of integer))
(=> (member column table) (= 0 (column-delta table column))))
(forall (column:(column-of decimal))
(=> (member column table) (= 0.0 (column-delta table column)))))