pact icon indicating copy to clipboard operation
pact copied to clipboard

possible cell / column-delta generalization

Open joelburget opened this issue 7 years ago • 0 comments

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:

  1. 0 is an integer literal. This is completely distinct from the decimal literal 0.0. So you'd have to specify integers and decimals separately.
  2. What's the type of column? Well, it's just column. But this would require the typechecker to have special info about column when 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)))))

joelburget avatar Oct 08 '18 18:10 joelburget