Towards a EDSL for defining concise models

[stevana]

PR #171 introduces a small language, inspired by Z/Event-B and TLA+, for specifying concise and showable models.

The, perhaps naive, idea that I have is that it will allows us to more easily port examples from Event-B and TLA+ to our setting. I say naive because the settings are obviously very different. They use classical meta-theory where as we have to be more constructive (unless we want to implement a theorem prover), and it shows in that many operations in the PR are partial.

I'd be curious to hear what other people think about this topic!

[stevana]

For N-ary relations/relational algebra it could be helpful to do something like:

• http://www.timphilipwilliams.com/posts/2017-04-12-nested-datacubes.html
• http://www.haskellforall.com/2014/12/a-very-general-api-for-relational-joins.html
• https://github.com/Gabriel439/Haskell-Bears-Library

[stevana]

Or use ideas from Datafun: https://github.com/rntz/datafun ?

[stevana]

Another idea is to have pre- and post-conditions use a new datatype instead of Bool, which gives better indication of what went wrong. For example:

precondition :: Model -> Action -> Logic
precondition _ (Apa x) = Boolean "x < 5" (x < 5) .&. Boolean "x > 10" (x > 10)

data Logic = Boolean String Bool | Logic .&. Logic

test :: Logic -> Either String ()
test (Boolean str b) | b              = Right ()
                               | otherwise = Left str
test (p .&. q)           = do
  Right () <- test p
  test q

We can then instead of just printing "precondition failed for Apa" show why it failed.

We can also be more fancy and have test accumulate error strings. Or make Boolean take a data Predicate = forall a. (Ord a, Show a) => LessThan a a | ... instead of a String and a Bool, the advantage of this approach apart from not having to provide the string is that we can also negate the predicate, which is helpful when adding disjunction to Logic.

[stevana]

Ideas from the above comment were added in PR #192.

[stevana]

The above ideas are as of #209 part of the counterexample output.