WebCheck uses a version of PureScript for specifications in testing web applications, which I'll refer to as "the language" in this document.
A specification includes a top-level definition called proposition
, which
must be a pure expression of type Boolean
. The interpreter of the language
does not allow effects (the Effect
type in PureScript, formerly known as
Eff
). But there are a few built-in constructs that are at least backed by
non-pure computations:
queryAll
: this can be seen as performing a DOM query for the current state (more in this later) of an element. For example,queryAll "p" { textContent }
would return a value of typeArray { textContent: String }
, i.e. an array of objects with the respective text contents.next
andalways
: these are temporal operators, used to alter the temporal mode of a subexpression. For instance,next expr
evaluatesexpr
in the context of the next state of execution, as opposed to the current. This means that an expression likeexpr == next expr
states thatexpr
in the current state equalsexpr
in the next state.
When WebCheck runs tests, it doesn't perform browser interactions or query the DOM at the same time as interpreting the specification. Instead, the process has three phases:
- WebCheck perform a static analysis of the specification to extract all queries.
- Then, it generates sequences of actions, performs them, and records the state at each step. The recorded state is based on the queries.
- Finally, it evaluates the
proposition
against the recorded states to validate the behavior. EachqueryAll
expression can be substituted for the corresponding recorded state, and can thus be seen as a pure expression. When a temporal operator is used, the interpreter evaluates the subexpression using the next state or all states of the behavior recorded in phase 2.
The catch is that even though queryAll
is conceptually pure in phase 3,
you cannot have queries depend on the results of other queries. For instance,
dependentQuery
in the following snippet cannot be supported by WebCheck:
selectors = map _.textContent (queryAll "p" { textContent })
dependentQuery =
concat (map (queryAll _ { textContent, attribute "enabled" }) selectors)
It's not allowed, as the query in dependentQuery
is constructed from the
results of selectors
. All queries must be known statically in phase 1
detailed above.
But knowing which queries are part of a proposition doesn't mean they are all relevant for all test runs. We might want to branch differently based on the results of a query:
branchingQuery =
if null selectors -- `selectors` from last snippet
then queryAll "button" { textContent, attribute "enabled" })
else []
It's still possible to statically extract both queries in the above example,
even if the result of selectors
is used in the conditional. The abstraction
outlined above seems to be the same as Selective Applicative
Functors. The
difference would be that in WebCheck the constraint "a query expression must
not depend on the results of a query" is checked by a static analysis pass in
the interpreter, while in the Haskell code in the paper, it's explictly
represented with a type in a correct-by-construction manner.
Now, I'm wondering:
- Do you know of other similar usages of selective applicative functors (even if they aren't identified as such) that do not use a representation like in the paper? More like what I'm using here, a static analysis approach?
- Can you think of other approaches that would fit with a pure expression language like the one in WebCheck?
I could encode this as selectives, as PureScript has all the machinery needed, but I don't want to put the burden on specification authors. I think most users will never hit this "limitation", and if they do, it might be a mistake. Forcing everyone to always use applicatives and selectives for that reason seems like overkill, especially as a proposition is treated as a pure expression.
You're absolutely right! It breaks referential transparency big time.
Yeah, I'm targeting "any web developer that is willing to learn some temporal logic", and having Applicative as another gate wouldn't be great. Using PureScript in the first place might be a problem, even. I've already heard some concerns and I might consider a TypeScript frontend further on, if this proves useful at all. So yeah, this is a trade-off between the principled and nice solution (which I personally like best!) and one that is approachable and more familiar by people outside our clique. I'm sure you see my point. 🙂
Thanks so much for the feedback!