typelanguage 0.3

The Types

This type language is built from the following concepts:

• Named types: int, long, float, complex, str, unicode, file, YourClassNameHere, …

• List types: [int], [[long]], …

• Tuple types: (int, long), (float, (int, Regex)), …

• Dictionary types: {string: float}, { (str, str) : [complex] }, …

• Union types int|long|float, str|file, …

• The “any” type, ??, for when a value is too complex to describe in this language. May be an indication that a piece of code is metaprogramming or should be treated with gradual typing.

• Function types:

  • str -> int

  • (int) -> int

  • (int, int) -> int

  • ( (int, int) ) -> int

  • ( str|file ) -> SomeClass

  • (int, *[str]) -> [(str, int)]

  • (int, *[int], **{int: str}) -> str

• Object types: object(self_type, field1: int, field2: str, ...)

• Polymorphic types (where ~a, ~b, ~c range over any other type)

  • ~a -> ~a

  • [~a] -> [~a]

  • ( (~a, ~b) ) -> ~a

Types as Contracts

The module typelanguage.enforce contains functions for using these types as run-time monitors.

Applied directly:

>>> check('{string: int}', {"hello" : "there"})

More interestingly, automatically protecting a function from bad input, for example, putting better error checking on Python’s unicode/str interactions.

>>> '\xa3'.encode('utf-8')
...
UnicodeDecodeError: 'ascii' codec can't decode byte 0xa3 in position 0: ordinal not in range(128)

>>> @guard('unicode -> str')
... def safe_encode(s):
...    return s.encode('utf-8')

>>> safe_encode(u'hello')
'hello'
>>> safe_encode('\xa3')
TypeError: Type check failed: ? does not have type unicode

Eventually, the notion of blame may be usefully incorporated, for pointing out which piece of code or agent in a distributed setting is responsible for the undesirable value.

Type Inference

In the spirit of Python and dynamic languages, type inference is best-effort. It works like so:

1. By traversing the code, we can discover a bunch of constraints between types in different bits.

2. Some of these constraints are going to be very easy to solve, so we can just propagate the results.

3. Some of these constraints are not going to be practical to try to solve, so we can just drop them or insert some enforcement code if we like.

More to explore

There are many other projects that check contracts or types for Python in some way or another, but none makes communication their primary goal, with the possible exception of pySonar. As such, they make different design choices. Some are research projects or prototypes – this is not. This is a library meant for use.

• PEP 316 (deferred)

• RPython and PyPy (compilation-oriented)

• pySonar and mini-pysonar (way cool)

• Pyntch

• typechecker

• pycontract

• python-dbc and one pyDBC and another pydbc and yet another pyDBC

• python-type-inference (no code, but has a great list of papers and even more tools)

And since dynamic languages are much of a muchness, it is worthwhile seeing what is happening elsewhere, though again very few projects emphasize the types themselves as fun, interesting and useful, only that the code has them.

• Contracts in Racket and Typed Racket

• Typescript aka a slightly gradually-typed Javascript and Javascript++ (sort of gradually-typed Javascript) and javascript-contracts and cerny

• Este (statically-typed coffeescript) and Uberscript (gradually-typed coffeescript) and contracts.coffee

• Contracts.ruby

I’m omitting the billion typed languages that compile to Javascript because those are just typed languages compiler to the assembly language of the web.

Finally, if you want to actually grok types, then contracts, then types and contracts together, then types and dynamic types together, then polymorphic type as contracts and dynamic types together, then type inference for such systems, try this chronological series of reading.

• *Types and Programming Languages* by Benjamin Pierce.

• Contracts for higher-order functions by Robert Bruce Findler & Matthias Felleisen. ICFP 2002.

• Hybrid type checking by Kenneth Knowles & Cormac Flanagan. TOPLAS 2010. (expanded and corrected from POPL 2006)

• Gradual typing for functional languages by Jeremy Siek & Walid Taha. Scheme workshop 2006.

• Gradual Typing for Objects by Jeremy Siek and Walid Taha. ECOOP 2007.

• Type reconstruction for general refinement types by Kenneth Knowles & Cormac Flanagan. ESOP 2007.

• Relationally-parametric polymorphic contracts by Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. DLS 2007.

• Gradual typing with unification based inference by Jeremy Siek and Manish Vachharajani. DLS 2008.

• Blame for all by Amal Ahmed, Robert Bruce Findler, Jacob Matthews, and Philip Wadler. STOP 2009.

• Always available static and dynamic feedback by Michael Bayne, Richard Cook, and Michael D. Ernst. ICSE 2011.

• The ins and outs of of gradual type inference by Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. POPL 2012.

Contributors

• Kenn Knowles (@kennknowles)

Copyright and License

Copyright 2012- Kenneth Knowles

Licensed under the Apache License, Version 2.0 (the “License”); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an “AS IS” BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.