The relationship between a language and its type system is one of the most crucial aspects of engineering the language; this is as true for rule languages as any other formal language intended to be processed automatically.
The purpose of this series of questions is to try to ascertain what kind of support there is for types in the rule language. The range of possible type systems is huge, so it is a little difficult to ensure that one questionnaire covers all the possibilities.
We are attempting to answer the following core questions about types:
A.The range of possible types, for example whether types are simple or have structure (i.e., polymorphic types, object types, collection types), whether recursive types are permitted, whether type definitions and/or type renaming are permitted.
B.What relationships between types, such as subtyping, are supported.
C.What the relationship is between types and values in the language.
D.What form of type processing is supported/required by the language: whether types are processed statically (before runtime) or dynamically (at runtime), or both, whether types are inferred or verified only, and so on.
In the following questions, we will use the abbreviation RL to denote the rule language, type-free if appropriate; and TL will refer to the type language. (It is quite possible for TL=RL, in some systems. In general they are distinct.)
Is the language typed?
1.Does the RL support any form of types on terms, predicates and other program elements?
Note: If no, please read following questions, you might decide to re-answer this question.
2.Does the language support any form of explicit type language (=TL) ?
3.Does the language require type safety checks on the arity and/or input arguments of built-ins? (E.g., does the arithmetic addition operator verify that the arguments are numbers?)
4.Can a type violation cause a different kind of result from a normal failure/negative response?
Note: if yes, then the language supports dynamic types on terms.
About the type language
5.Do types have names? I.e., is type equivalence defined as type name equivalence or structural equivalence (a.k.a. type unification)?
6.Are TL terms simple names, or may a TL term be a function term (i.e., may a type term contain other type terms as arguments)?
Note: if yes, then the type language support parametric polymorphism.
7.Does the TL support standard complex type terms?
8.Are collection types supported?
9.Are array types supported?
10.Are set/bag types supported?
11.Are index types supported? (I.e., can the index of an array or collection be typed separately?)
12.Are list types supported?
13.Are tuple types/type tuples supported?
14.Are numeric interval types supported?
15.Are class types supported?
16.Are higher-order elements of the RL given specific TL terms? E.g., can function types be used as arguments of other types?
17.Is there any distinction between primitive types (e.g., numbers) and other types? (I.e., does the term “boxable” apply to the TL?)
18.Does the language support any form of reference type?
Note: Reference types are a kind of pointer type often used in conjunction with re-assignable variables.
19.For parametric polymorphic type systems, are there any distinctions between the types permitted on reference types as compared to non-reference types?
Note: Many functional programming languages have complex rules associated with the type targets of reference types; such as not permitting polymorphism in such cases.
20.Is it possible to define new types?
21.Is it possible to define type aliases?
22.Can a type be defined extensionally? (a.k.a. algebraic types)
23.Can a type be defined intensionally?
24.Does the TL permit definition of recursive types?
25.Is it possible to define arbitrary predicates over type terms?
Note: if yes, then the language is likely not type decidable.
26.Does the language support any predefined predicates over type terms?
27.Does the language support any form of sub-type relation over type terms?
Note: if yes, then the language supports sub-type polymorphism
28.Does the TL support existential types? E.g., is it possible to write rules that can 'recover' a type of an argument whose type is obscured?
29.Does the language support type reflection? I.e., can the type of an expression be reified, and can the type of an expression be determined to be consistent with a reified type expression?
Note: if yes, then the language must also support type casting.
30.Does the language support type interfaces?
31.Can a type interface include assertions as well as pure type descriptions?
32.Can a type interface capture preconditions/postconditions/invariants?
a.Preconditions only
b.Preconditions and postconditions
c.Preconditions, postconditions and invariants
33.Are types of large scale entities such as classes, modules, packages etc. part of the TL.?
34.Does the type system support the assembly of rule systems from multiple sources? (I.e., are features such as loading of modules also type safe?)
Relationship between the TL and the RL
35.Are TL terms syntactically distinct from RL terms that denote values?
36.Are TL terms semantically distinct from RL terms that denote values?
37.Are TL terms permitted as value terms in rules?
Note: if yes, then language supports explicit dynamic typing
38.Which statement is more accurate for the relationship between type terms and other elements of the language:
a.The type system induces an abstract interpretation over the sets of rules.
b.The type system partitions the universe of elements into disjoint categories.
c.The type system represents a system of monadic predicates with a distinguished interpretation.
d.All of the above.
e.None of the above.
Note: this is an attempt to gain a rough characterization of the semantics of types vs the semantics of rules themselves.
39.Does the language system perform type consistency verification independently of any queries?
Note: if yes, then the language supports static type checking
40.Does the language permit more than one type interpretation of any terms/rules/functions/predicates etc.?
Note: if yes, then the language is weakly typed, if no, then the language is strongly typed.
41.Does the language permit more than one type for any function/predicate/action symbol?
Note: if yes, then the language supports overloading.
Note: this is different to previous question, it is possible to be strongly type checked and to support overloading.
42.Are type assignments to RL terms inferred automatically by the type systems?
43.Can type inference infer recursive types for RL expressions?
44.Are all elements of the RL associated with unique elements from TL?
45.Can a type of an element of the RL be left as a type variable?
Note: this, together with type terms being structured, means that the language supports parametric polymorphism. On its own, permitting free variables to denote types is a marker for support for generics.
46.Does the language permit annotations on expressions that further constrain the type of the expression?
47.Does the RL language permit type casting?
48.Does the language permit runtime evaluation if one or more type inconsistencies are detected?
49.Does the language permit individual rules to select on the type of the arguments (as opposed to the values of the arguments)?
Note: if yes, the language supports type restrictions.
50.If the TL and RL support classes, what is the correspondence between a class type and a class implementation:
a.Each class type has exactly one implementation
b.An interface can be implemented by any number of implementations
c.A class type can be implemented by any number of class implementations
51.Which statement is more accurate?
a.Predicates are typed, tuples are not.
b.Each tuple in a relation carries an independent type assignment.