[Python-ideas] type checking using PyContracts; was: Proposal: Use mypy syntax for function annotations

[Andrea Censi]

Dear all,

(Apologies for not replying to the original thread,  I only signed up
to the mailing list today)

I wrote PyContracts[1], which implements type-checking functionality
using decorators for Python 2.7+ and annotations in Python 3.

 [1] http://andreacensi.github.com/contracts/

> def word_count(input: List[str]) -> Dict[str, int]:

Here's that example done using PyContracts and Python 3,
and note the extra constraint '>=1' that PyContract can express:

    from contracts import contract

    @contract
    def word_count(input:'list(str)') -> 'dict(str:int,>=1):
        ...

Here's that example done using PyContracts and Python 2.7, using
a decorator instead of annotations:

    from contracts import contract

    @contract(input='list(str)', returns='dict(str:int,>=1)')
    def word_count(input):
        ...

I would like to make a few points from my experience of writing
PyContracts regarding the general issues that one encounters in adding
type checking to Python.

1) Once one starts to think about it, "types" are very broad and if you
   design a system from scratch, make sure it is extensible. For example,
   you might want to have "positive integer" in addition to "integer"
   ('int', and 'int,>=0' in PyContracts). Also, let the users add
their own types.

2) Dependent types are a must and they must have a simple syntax.
   For example, this is a PyContracts annotation that says the function takes
   a list of strings and returns a list of integers of the same size N:

       @contract(x='list[N](str)', returns='list[N](int)')
       def f(x):
           return list(map(len, x))

   PyContract's convention is that and a,b,c,...,y,z bind to any variables
   and A,B,C,...,Z bind to integer variables. This makes numpy contracts
   very nice looking:

       @contract
       def gray2rgb(gray:'array[HxW](uint8)') -> 'array[HxWx3](uint8)':
         ...

3) There is an argument for using regular strings to describe annotations
   rather than Python constructs such as MyPy. One advantage
   is that the system is backwards compatible. It also makes the code
   much cleaner because you don't need to import the various symbols.

   Here's a simple example in MyPy:

        from typing typevar, Sequence

        T = typevar('T')      # Declare type variable

        def first(seq: Sequence[T]) -> T:
            return seq[0]

   Here's the same example in PyContracts (using Python 3's annotations):

        from contracts import contract

        @contract
        def first(s: 'seq(type(t))') -> 'type(t)':
            return s[0]

   Same example in Python 2.7+ (using decorators):

     from contracts import contract

        @contract(s='seq(type(t))', returns='type(t)')
        def first(s):
            return s[0]

(By the way, after a while, I actually like the decorator version
 better than Python 3's annotations, because you can see very
easily the function's name and parameters, and only if you want
you can then read the function annotations above.)

cheers,
A.

-- 
Andrea Censi | http://censi.mit.edu | "Not all those who wander are lost."
research scientist @ LIDS / Massachusetts Institute of Technology