search

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
782 stars 31 forks source link

Information loss in the effect system #364

Open bugarela opened 1 year ago

bugarela commented 1 year ago

The effect system is much simpler than the type system. With the current representation of effects, it is impossible for tuple projections or record access to propagate effect information correctly in all cases. After the effects are combined in a constructed tuple or record, there is no way to project them according to the position/field being accessed.

This is not a big issue since records and tuples are only associated with Read effects, which doesn't restrict the user in meaningful ways (as Update does)

bugarela commented 1 year ago

Solving this will require some representation of row types in effects.