Expressions

Here is the grammar of expressions E. As is standard in ML-family languages and Haskell, juxtaposition is used to represent function application, with application associating to the left.

1. Actions

The DomTool language is purely functional. Like Haskell, it uses a monad to inject effectful operations into its pure core. For DomTool, this is the action monad. This monad merges two potentially separate features that tend to occur together.

First, actions are used to run code that will affect the outside world and lead to changes in the configuration of real daemons. Primitive actions like domain and vhost are the building-blocks here. They are defined by plugins. The other action forms in the table above are there just to allow the proper composition and sequencing of applications of primitive actions, which do the real work. See DomTool/Implementation for how the code to run for a particular primitive action is registered with the implementation.

Second, the action monad provides the functionality of environment variables. These are similar to UNIX environment variables, but DomTool maintains its own environment where each variable has a static type. The rationale for including environment variables in the language is that, while many actions are highly configurable, you usually only want to tweak a few of their options at a time. DomTool allows an ambient environment of default variable settings, and it provides language constructs for modifying certain variables both globally and locally.

1.1. Effects of the action expressions on the environment

1.2. Nested action functions

Sometimes it is convenient to be able to write new nested actions that call primitive nested actions as subroutines. For instance, the dom helper function uses domain as a subroutine. Standard functions aren't good enough for these purposes, since they don't allow us to take into account the different environment effects that different nested action arguments might have. The nested function type P => T is the solution to this problem.

You can define a nested action function with the \\ Symbol : P -> E form. Such a function has type P => T when assuming that Symbol has type [P] implies that E has type T. Any call to this function will be typed taking into account that we play the argument action's effect before playing the effect of the function's body.

2. Extern types

Extern types (which are also used to implement "primitive types" like int and string) have something of the flavor of dependent types or refinement types. Registering appropriate handlers from a plugin can create an extern type whose values are controlled by an arbitrary predicate. Plugin implementers are supposed to maintain the invariant that the predicate controlling an extern type is never observably inconsistent in the course of a single type-checking session. That is, it never once declares a value to belong to type T and also declares it not to belong to T in the same type-checker invocation. A good example is the your_domain type, which consists of those strings naming domains that the current user is allowed to configure. Within a single type-checking, the user remains constant, and so your_domain's predicate returns consistent decisions. On the other hand, across different sessions by different users, the predicate will of course make different decisions. This approach allows extern types to be used for flexible type-level enforcement of security policies.

It would be a pain for users to have to mark exactly which extern type a certain expression is meant to belong to. Instead, the DomTool language implementation uses slightly non-compositional type-checking to make use of rich extern types more convenient. By "non-compositional", I mean that the value of an expression, not just its type, may matter in type-checking a larger expression that it is found within. This non-compositionality is only used to infer when a value was given a base type like string when it really ought to have been given some rich extern type. For instance, when a function is called that expects an argument of type your_domain, the argument is first type-checked. If its inferred type is your_domain, then all is well. If not, then we try again, passing the actual argument expression to your_domain's controlling predicate. Only if that predicate also rejects the expression do we signal a type error. No simplifications are performed on an expression before checking its form; for instance, a global variable's definition won't be unfolded to check if the value satisfies a required predicate.

• Print
• Edit
• Quit
• |
• ←
• 1
• 2
• 3
• 4
• 5
• 6
• 7
• →
• |

• 5|7