Types and Programming Languages Chapter 1 Introduction

1.1 Types in Computer Science

Page 2

research on typed lambda-calculi is usually concerned with systems in which every well-typed computation is guaranteed to terminate, whereas most programming languages sacrifice this property for the sake of features like recursive function definitions.

• @mrageh: Why don't programming languages drop recursive function definitions so their type systems can guarantee that every well typed computation will eventually terminate?

  • @tuzz: Some programming languages do, but in general, recursion is a useful tool that lends itself well to certain kinds of problems. For example, we did a meeting once on the Towers of Hanoi problem which can be solved in just a few lines with recursion.

  • @jcoglan: if you can guarantee that a program will terminate, then it is not Turing-complete. it turns out you can still do many useful things with systems less powerful than Turing machines, but for general-purpose programming you’re going to need them

  • @tomstuart: They can. These are called “total programming languages”, e.g. the Charity programming language. The downside is that they aren’t as powerful as languages that don’t provide this guarantee.

A type system can be regarded as calculating a kind of static approximation to the run-time behaviors of the terms in a program.

• @mrageh: Does this mean a type system tries to determine how a program would behave during runtime?

  • @jcinnamond: I think a type system* tries to give some guarantees about runtime behaviour. For example you might run a function that returns the number 3. The runtime behaviour will be producing this value. The type system might be able to guarantee that the function produces a number, or that it produces a number greater than zero, or that it produces the value without modifying global state, or whatever. That is, the type system gives some approximation of the runtime behaviour without including all of the detail. In general, the more accurately the type system is able to describe runtime behaviour, the more complex the types involved.

    (*) for some definition "type system". Not all type systems are about guarantees. Ruby, for example, uses types to control runtime behaviour, not predict it.

  • @tomstuart: Yes, that’s the entire game we’re playing: what can you decide about a program’s runtime behaviour without actually running it?

Being static, type systems are necessarily also conservative: they can categorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time.

• @mrageh: Why can static type systems only prove the absence of bad program behaviour and not the presence?

  • @jcinnamond: The key word here is 'some'. Types are less specific than runtime values, so sometimes there is not enough information to decide whether or not the value that you will encounter at runtime will cause a problem.

    Consider a function in a statically typed language called findUser. This takes a numeric id and returns the corresponding user if the ID exists, or nil if it doesn't. Thus we can say that the return type of that function is (User OR null). Now imagine your code looks like this:

    return if user.nil?
    
    print user.name

    The typechecker will look at the call to user.name, and then look at the type of user (User OR null) and be unable to guarantee that the call will succeed. So it will reject it because it doesn't know that the bad behaviour (calling name on null) is impossible in this code. (edited)

    If, however, findUser was guaranteed to return a User object, or at least to return an object that responded to name, then the type checker could guarantee that the call to user.name will work. So in this case it will accept the program. (edited)

    I think that the wording absence of bad program behaviour is awkward here. I think it's clearer to say something like there are situations where code will be fine at runtime, but the type checker can't guarantee that so it might incorrectly reject valid programs

    • @jcoglan: I like @jcinnamond’s findUser example because some type systems will accept that and some will reject it

      e.g. Java’s type system allows calls to null, haskell’s does not

      in Java, user would just have type User, the fact it can be null is not captured

      in Haskell it would be a Maybe User and you’d have to explicitly handle that

  • @tomstuart: Because of undecidability. If you write a program that says “if this complicated expression returns true then do something bad, else do something good”, it may not be possible to decide whether the complicated expression returns true without running it. In that case the type system will assume that it is possible for the bad behaviour to happen, even if it actually never happens when the program is run.

    (The statement should really be “type systems cannot prove the presence of bad behaviour IN GENERAL” — for some programs it’s easy to decide that they have bad behaviour.)

1.2 What Type Systems Are Good For

Page 4

In practice, static typechecking exposes a surprisingly broad range of errors. Programmers working in richly typed languages often remark that their programs tend to “just work” once they pass the typechecker, much more often than they feel they have a right to expect. One possible explanation for this is that not only trivial mental slips (e.g., forgetting to convert a string to a number before taking its square root), but also deeper conceptual errors (e.g., neglecting a boundary condition in a complex case analysis, or confusing units in a scientific calculation), will often manifest as inconsistencies at the level of types.

• @mrageh: Do Ruby programmers use TDD to mimic static typechecking? If I'm refactoring some code I rely on my test suite to tell me all places that need changing after I change a method or class. Do programmers working in such languages not rely on TDD as heavily as we do?

  • @jcinnamond: Both tests and types can be used to solve the same problem: providing reassurance that a program operates correctly. Tests do this by running the code and checking that the resulting value is correct, given some specific setup. Types do this by evaluating (but not executing) the code and checking that any resulting value will have some interesting property.

    Types are better than tests for providing guarantees insofar as you can accurately express the runtime behaviour that you are interested in, and be confident that your type is correct. As the behaviour gets harder to express with a type (e.g., "when running this on a Tuesday that is also a leap day and the customer signed up within the last 12 months then do this weird thing...") then tests become better than types.

    You're correct that developers using languages with rich type systems tend to rely on tests less than those with less expressive types. Languages like Ruby that have no static type checking rely exclusively on tests.

    Note also that both tests and types can be used for more than just correctness. In fact both Test Driven Development and Type Driven Development proponents would argue that correctness is the least interesting aspect - that in fact it's all about driving better structure in your code.

  • @tomstuart: Yes. You can think of a type system as a set of tests that must pass for every program you write in that language. TDD is a bit less popular in statically typed languages because the type system rules out certain errors automatically.

Page 5

Types show up in the interfaces of modules (and related structures such as classes)

• @mrageh: For the above example should we think of modules and classes as ruby modules and classes?

  module Rubby
    def interface
      puts "am I the interface the above passage is talking about?"
    end
  end

  • @tomstuart: Yes. The “interface” of a module/class is the list of method names along with the argument/return types of each method (e.g. “#foo takes a boolean and a string and returns an integer”).

Page 7

Run-time safety is not normally achievable by static typing alone. For example, all of the languages listed as safe in the table above actually perform array-bounds checking dynamically.

• @mrageh: Why can't static type systems check for out of bound errors on arrays?

  • @jcinnamond: Not all type systems!

    The problem is that the size of an array, or the index used to access an element, are often unknown at a static analysis phase. So the type system can't express a concept like "this index is within the array bounds" because it doesn't know what the index is, or what the array bounds are.

    Dependently typed languages such as Agda and Idris solve this by having a richer type than an array, typically a Vector that consists of both the array elements and the size of the array. But that is well outside of the scope of TAPL. (I think it comes up in ATITAPL but I haven't read that yet.)

  • @jcoglan: some can, it depends what structures the lang provides and what distinctions they have. e.g. Haskell has both “lists” which can be any size but all elements must be the same type, and “tuples” which are fixed-size but each element can be a different type. e.g. a list of ints has the type [Int], and a tuple containing an int, string, bool, and a list of any type is (Int, String, Bool, [a])

    the type of tuples means their size is fixed at compile time: you can’t make a tuple with the wrong number of elements, or where some elements are the wrong type

    this is a bit like database tables vs rows: you know at boot time, from the schema, how many fields each record has and what their types are: that’s like a tuple. but, you don’t know how many records there will be because that changes at runtime, but you do know each record will conform to the schema

    so a database table list like a list of tuples of a certain type

    e.g. if your table has three columns of type int, datetime, and string, you can model the table as having type [(Int, Datetime, String)] in haskell — then haskell will let that list be any size, but every element will have 3 items of fixed types

  • @tomstuart: Advanced type systems can check this, but they are complicated and restrictive, so most languages don’t try to do it.

Overall chapter

• @mrageh: Static and dynamic checks are mentioned a few times in the first chapter.

  Static checks happen before a program is run. Do dynamic checks happen during runtime only and is that why dynamic languages are sometimes slower or less efficient?

  • @jcinnamond: Spot on. It's also why dynamic languages are considered less reliable, but there is a lack of documentation to support this assumption.

    Interestingly, JITs work by using this runtime analysis to rewrite code into more efficient forms (e.g., by removing unnecessary runtime checks) which is how to achieve better performance after some startup time.

  • @tomstuart: Yes, static means “before runtime” and dynamic means “during runtime”. And yes, that is one of the reasons why dynamic languages can be slower.

• @mrageh: C has a compiler like GCC and when we write a C program, we use GCC to produce a binary that we can execute.

  Whereas Ruby is an interpreted language and it has an interpreter that we use to execute programs.

  Do virtual machines like the JVM use a compiler or an interpreter to execute their programs?

  As far as I understand the JVM is a program that can be installed on most OSes and it converts a Java program to instructions that a particular machine can understand. But what on earth is a JVM

  it seems like it’s an interpreter to me ¯\_(ツ)_/¯

  • @mudge: when you compile a Java program, it gets translated from the Java source code you’ve written (System.out.println, etc.) into another format called Java bytecode which is a sort of machine language but for the JVM, not for your CPU directly

    the Java Virtual Machine is then, as you say, a runtime for that bytecode which translates that into instructions your particular platform understands

    so yeah, it seems very like an interpreter in that sense

    so you can think of there being an extra layer

    Ruby: lovely ruby code -> ruby interpreter -> instructions for your computer
    Java: lovely Java code -> javac -> Java bytecode -> JVM -> instructions for your computer

    so you get the benefits of a compiled language but it’s a bit more portable

    i can compile some bytecode on my Mac and you can run it on your Windows computer without recompiling it with javac

    • @mrageh: that’s a great way of putting it, I’ve noticed one difference between an interpreter and a JVM is that the JVM is used by other languages like Clojure

      is that because of the extra layer, the bytecode

      • @mudge: yeah so that’s a great point: other things can produce bytecode, not just Java

        such as Clojure, Scala, JRuby

        because it turns out the JVM is pretty amazing as a platform for your software

        e.g. it has a really interesting garbage collector for memory management and can do some impressive optimisations as your program runs

  • @tuzz: My understanding is it’s an abstraction layer that sits between the computer hardware and one or more programming languages. It’s handy because:

    1. If you’re building a new programming language, you gain all the benefits/tooling/performance of a mature VM implementation if you choose to target that. For example, Scala targets the JVM and gets loads of stuff for free like garbage collection and runtime optimisations.

    2. If you’re building a new type of computer architecture, you can run a huge number of programs on that architecture by implementing the VM according to its specification. So if you invented a computer made of Spaghetti, you could run all your Clojure, Scala, JRuby on it by implementing the JVM.

  • @jcinnamond: Ruby has a VM as well

    So in principle the VM of YARV is the same kind of thing as the VM of the JVM - they're both virtual machines targeted by compilers/interpreters.

    You can have interpreters that source code, parse it, and then try to run that code immediately using some implementation in another language. Ruby 1.8 is like this (I think...)

    You can also have interpreters that take source code, parse it, convert it into another format, and then execute that new format

    This is how Ruby 1.9 works

    So the ruby interpreter is also a compiler at some point - maybe just a lazy one.

    It's also a runtime for the ruby bytecode

    This is really two separate concepts. There is the interpreter vs compiler idea, and then the VM verses native bytecode idea. They are orthogonal.

    A compiler refers to a program that takes the full definition of a program in some source language and converts it into a corresponding executable format for some target, where the target can be a VM or an OS/architecture. It typically performs some kind of static analysis/optimisation up front because it has access to the full program.

    An interpreter is a program that takes a possibly incomplete program and runs it straight away, without explicitly emitting some executable format. There are a couple of approaches to running the input code - it can take each statement and execute it immediately (Ruby 1.8), or it can convert the input into a new format (typically more efficient to execute) and then run that new format. This latter approach is usually done for efficiency*

    Because interpreters don't usually have access to the whole program they typically can't do static analysis or up-front optimisations.

    (*) except haskell and gchi, which produces a denotational form of the source code just to fuck with your understand of what 'interpreter' means 😉

    When gcc compiles a program it spits out a sequence of instructions for a specific CPU, where the instructions are things like 'load this sequence of bytes into this register' or 'run this opcode'.

    When javac compiles a program it spits out a sequence of instructions for the JVM, where the instructions are things like 'load this value into this register' or 'run this instruction'. They're very similar ideas, but the JVM is like an idealised CPU for running java code.

    When you run a compiled java file there is some code that takes these JVM instructions and converts them into one or more underlying CPU instructions. It also does some helpful things such as scheduling threads and garbage collection.

    Something like the erlang or Go runtimes confuse this picture by compiling to native CPU instructions, but also providing a runtime (packaged into the executable) that do helpful things such as scheduling and garbage collection.

    After a while you start to question where the code stops and the physical machine starts, and then you start to question the nature of reality, and then you just curl up in a ball in the corner and shout 'microcode' at anyone who gets too close

  • @tomstuart: A virtual machine works the same as an interpreter (more or less), but it runs something like bytecode instead of the source program directly. As others have said, this gets more complicated with something like the "Ruby interpreter", which is actually made from 2 pieces: a Ruby to bytecode compiler, and a bytecode virtual machine. But from outside the box, it looks and works like an interpreter, so that's really an implementation detail.