I hold the general opinion that types enable me to program more effectively; I understand that this may not apply to everyone, though. In this post, I'd like to explore how types facilitate higher-quality programs in my workflow.

My first serious programming language was Perl (although I was pretty serious about BASIC as a kid); I learned how to program without having much in the way of types except the differentiation between scalars, arrays, and hashes. I also spent a fair amount of time writing assembly on the 6502s (where I'd make the joke "there is no type but the bit"). I could make the argument that this really enabled me to learn how to program from a conceptual standpoint. Later, picking up C, I was introduced to the concept of stronger types. Common Lisp was an interesting hybrid; for prototyping, there isn't a requirement for type annotations but they are provided for optimizing programs. I didn't use types in Erlang, but pattern matching provided some similar benefits (but with much weaker guarantees); Dialyzer handled much of the static analysis and I was interested in checking out QuickCheck for Erlang but never did.

Recently, I've also been playing with Racket. I found the idea of contracts fascinating. Essentially, a contract looks like this:

(struct node (label edges)
  #:transparent
  #:guard (λ (label edges type-name)
            (cond
              [(and (symbol? label)
                    (or (list? edges)
                        (set?  edges))
                    (if (list? edges)
                        (andmap symbol? edges)
                        (foldr (λ (x y)
                                 (and x y))
                               #t
                               (set-map edges symbol?))))
               (values label
                       (if (list? edges)
                           (list->set edges)
                           edges))]
              [else (error "Node labels must be symbols."
                           label edges)])))

This particular contract is on a data type, and says that I am defining a data type node that contains edges and a label. The edges value must be a list (or set) of symbols, and the label must be a symbol. This is a rather verbose declaration. In Go, I would specify

struct Node {
    Edges []Symbol // Go doesn't define an analogue to symbols
    Label Symbol
}

Likewise, in Haskell it would be

data Node = Node { edges :: [Symbol]
          ,label :: Symbol } deriving Show

and finally, the Common Lisp implementation:

(defstruct node
  "NODE represents a node in the graph. It has a LABEL, which should
   be a SYMBOL, and edges, which is a list of SYMBOLs."
  (label nil :type symbol) (edges nil :type list))

The Common Lisp variant only specifies that the edges be a list, though. Enforcing the symbol requirement is done in the constructor, which hides this requirement from the user. What I find useful is explicit (i.e. as part of the function or data structure documentation) is to specify the expected type of data coming in. Go, C, and Common Lisp are less strict about this; data can be cast around without much effort.

What makes the Racket approach interesting is that contracts can be applied on an as-needed basis: only those functions or types that the author deems useful warrant a contract as to their behaviour. The rest is left up to the user. I haven't spend much time verifying the behaviour of the contract system in this regard, whether it will analyse the interactions of functions without contracts with those that do have them at compile time.

In an IRC channel, Steve, Jeremy, and I were discussing Jon Blow's programming language Jai, in which Steve mentioned

12:30 [ steve] he basically invented compile time contracts
12:30 [ steve] because he got mad at type systems and wanted to check
               what he wants to
12:30 [ steve] instead of a complex type system that gets in his way

I think the optional type system is somewhat similar to the approach of the L4 exokernel, which verifies a core subset of the kernel. This still allows reasoning about the behaviour of the system while keeping the programmer's workload at a manageable level. This optional typing (often leaning on the no-typing side) seems preferred by the prototype-oriented style of programming, in which a program is slowly built out, typically in a REPL, and slowly grown into the final product. This is the style I favour when writing Common Lisp, Racket, and Clojure. Similarly, in Go I tend to build up functions with tests to verify their behaviour and from this base build out the program. The programmer spends their time as much in development as in planning.

In a strictly-typed system, such as Haskell, or a dependently-typed language like Coq or Idris, the programmer is forced into using types at all levels. This can get tedious and lead to wrestling with the type system; I've found that when using these languages, I spend more time thinking about how the program should work and what its behaviour should be than actually writing code. Particularly, I try to consider what behaviours are expected of it in both success and failure modes.

It seems natural that being a security engineer that I prefer strict typing with higher degrees of formal verification of behaviour as possible. The Coq model of proving theorems about the code as a basis for developing code was an enlightening experience earlier this year; at some point, I'd like to dive into Idris. Much of the benefit that I derive from type systems comes from static analysis: once the program is built, there is a class of errors that I can avoid entirely, which enables a more focused scrutiny on the behaviour of the program.

When I'm writing secure systems, I prefer to think in terms of collections of data types and behaviours. What inputs should function parseMetaData operate on? What types should it emit? How are errors signalled and propagated usefully through the program? How should a MetaData instance behave? Go's weak typing and interfaces provide a useful and pragmatic approach to this that I've leveraged quite often; this approach has yielded several systems that have been running continuously for long periods of time with no maintenance or attention at all. In fact, I periodically re-attach to a tmux(1) instance to find a program running that I'd forgotten about for months. Recent examples of this include a service that provides random data to stir the RNGs on my VPSes via the random number generator (including a few HWRNG sources) on a BeagleBone Black and an encrypted log transport service for several of my sites.

An alternate approach that I've been learning is the use of polymorphic types combined with type classes used to specify the shape and kind of data as well as the behaviours expected of it. This seems a promising direction to explore, particularly in light of tools such as QuickCheck.

Racket has a few other interesting ideas I'd like to explore in other languages; particularly, the idea of custodians that explicitly manages resources (i.e. threads, file descriptors, sockets, etc...)