7
$\begingroup$

I was reading this article about types, and started wondering how static type checkers could enforce other properties in programs. For example, say I wanted to create a language which would allow checking at compile time that a particular function was only called at most once every 300ms. How would I go about specifying the language to allow that to be enforced? What existing languages try to enforce similar properties?

$\endgroup$
  • $\begingroup$ 1) Why would you have the type checker do these things? 2) "milliseconds" is not a meaningful unit for a compiler; the resulting code should be valid for more than one machine and in more than one load scenario. 3) The particular property you state is likely undecidable. A reduction from the halting problem seems immediate. $\endgroup$ – Raphael Oct 8 '14 at 9:00
4
$\begingroup$

The property you mention is probably not something that sounds like an ideal fit for enforcement by type systems, so it's not the first example I would suggest looking at, if you want to learn more about how type systems can be used to enforce a variety of properties. (I'm not saying it is impossible to enforce that property using a type system, but it might not look natural or feel super-useful to an everyday programmer, and the type system might need some hand-holding or help from the programmer.)

However, there are other properties that are a better fit for type systems. For instance, you might look at dependent type systems, which can be used to enforce many properties.

In my experience, type systems tend to be more useful for enforcing safety properties. It tends to be harder to reason about time or liveness properties using a type system (I'm not saying it is impossible, but it might be harder or less natural).

You might also enjoy reading about the Curry-Howard correspondence, which shows a correspondence between theorems and types (and between a proof of a particular theorem vs a particular program that can be given a particular type). Proof-carrying code is one example of a system that relies heavily on this view of proofs-as-programs. The goal there is to prove non-trivial properties of a program. The theorem you want to prove gets encoded as a type, and the proof gets encoded as an expression in an abstract language; then checking the validity of the proof becomes as simple as checking that the expression has the claimed type. This essentially shows how you can reduce "showing that the program satisfies a particular safety property" to type-checking.


In a similar but not identical vein, you might also enjoy looking at languages like Haskell and the QuickCheck tool, which uses the rich type information available from the Haskell type system to synthesize test cases. Anecdotally, QuickCheck is effective at finding many bugs. This is not an example of using the type system to enforce absence of a particular kind of bug, so much as using the type system to make random testing more effective and thereby tend to help programmers catch many bugs earlier.

| cite | improve this answer | |
$\endgroup$
4
$\begingroup$

Many problems of this kind can be adressed by abstract interpretation of programs. It may well be that abstract interpretations can always be expressed in type systems, but I am not quite sure about it as I did not follow the field for a long time. The early work, at least, was often perceived as interpreting types differently.

A very early paper on this, very easy reading, is the following. It is mostly examples, as I recall. It was fun reading at the time.

Michel Sintzoff: Calculating properties of programs by valuations on specific models, Proceedings of ACM conference on Proving assertions about programs, 1972 doi:10.1145/800235.807086

Later work on abstract interpretation was devoted to formalization of the concept.

You will find major references on the web and in Wikipedia.

The simplest example of abstract interpretation is taught in elementary school. It is the "Casting out nines" test. It can be used to check that the value of an expression satisfies a property when the values of the unknown arguments satisfy that property. The checking is done by actually evaluating the expression in a different interpretation domain. In this case, the abstract value can also be seen as types for the variables.

| cite | improve this answer | |
$\endgroup$
3
$\begingroup$

I'm aware of at least one attempt to use unification to infer time-like facts about programs. The following papers are from David Gifford's research group at MIT, back in the late 1980s/early 1990s. They infer the "times" of functions as polymorphic expressions of the "times" of their inputs. Dornic's paper tries to infer time complexity of functions, while Reistad's paper tries to infer actual time estimates in terms of the measured cost of micro-operations (like dereferencing a pointer or returning a value from a function.)

Dornic, Vincent; Jouvelot, Pierre; Gifford, David K.: Polymorphic time systems for estimating program complexity. ACM Lett. Program. Lang. Syst. 1(1):33-45, March 1992. DOI=10.1145/130616.130620.

Reistad, Brian; Gifford, David K.: Static Dependent Costs for Estimating Program Execution Time. ACM Conference on Lisp and Functional Programming, 1994: 65-78.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.