Mailman 3 Optional static typing -- late to the party - Python-ideas

newer
Proposal : allowing grouping by...

Optional static typing -- late to the party

older
Allow getting all the items out of...

Tennessee Leeuwenburg

20 Aug 2014 20 Aug '14

5:08 a.m.

Hi all, I apologise in advance for being across only that proportion of the previous correspondence that I could read in about half an hour. Too much has been said to fully integrate it all. I have some responses to what was written, and one of those I feel has been largely missed. Please accept this as "just some stuff I think" and not any kind of strident criticism or positioning. The primary goal should be a syntax which enhances human readability. While I agree that having good static code analysis tools is very useful for the write --> test --> fix cycle, actually the more bugs you can catch during the human read/understand/write cycle, the better. The earlier you can communicate useful information about variable types, the better, and the earliest stage of that is code comprehension at the human level. I mostly agree with those who are preferring docstring embedding over signature decoration, particularly for complex cases, due to the desire to separate the complexity into structured sections. The signature is like the heading, and the annotation is like additional detail. I was led to a conclusion: what is wrong with allowing both? Indeed, clearly both are actually already supported by various tools. So perhaps there is actually a higher-level common concept -- what are the actual assertion which are going to be supported? Can I declare a variable only to be a list, or can it be a list-of-ints? Further, is it possible to standardise between some of the syntax/terminology, and some of the assertion types, such that they are consistent between function annotation syntaxes and docstring embedding syntaxes? Could I use function annotation for simple cases, but seamlessly move to a docstring-embedded approach for a more complex example? e.g. def frobnicate(x: int, y: int) -> float ''' Applies some kind of standard function ''' return x**2 / y is great. But def handle_complex_case(name, context, objective, datacube): ''' @param name: str, contains a "Firstname Lastname" string @param context: dict, contains a data record @param objective: int, contains a coded directive @param datacube: numpy.array, contains a field of continuous spatial data @return: instructionset: list(callable), a list of callable instructions ''' allows me to describe what's going on in that function in a way which supports both typing and static analysis. Apologies for inventing the docstring syntax rather than correctly using an existing syntax. However, my point is that in the first example, an annotation approach is *more* readable. In the second example, you really want to spend more time describing and annotating the function. If there could be some agreement about the details and consistency, I see no reason that a dual style could not be preferable, and no more complex to understand and use. Regards, -Tennessee Leeuwenburg -- -------------------------------------------------- Tennessee Leeuwenburg http://myownhat.blogspot.com/ "Don't believe everything you think"

Attachments:

attachment.htm (text/html — 3.7 KB)

Show replies by date

Steven D'Aprano

20 Aug 20 Aug

5:35 a.m.

On Wed, Aug 20, 2014 at 10:08:48PM +1000, Tennessee Leeuwenburg wrote: [...]

...

I was led to a conclusion: what is wrong with allowing both?

"Both" being function annotations and docstring annotations. Docstring annotations will not suddenly go away if (when) Guido's proposal is accepted. But remember that any annotations in docstrings may not be available at runtime, whereas function annotations will be unless you deliberately delete them. Also, docstring annotations have the disadvantage of being text only, instead of expressions which evaluate to arbitrarily powerful or useful objects.

...

Indeed, clearly both are actually already supported by various tools. So perhaps there is actually a higher-level common concept -- what are the actual assertion which are going to be supported? Can I declare a variable only to be a list, or can it be a list-of-ints?

Yes. Using Guido's suggestion of mypy's syntax: from typing import List def spam(x:List)->List[int]: ... declares that spam accepts as argument a list of anything, and returns a list of ints. But of course you're more likely to want to accept anything which quacks like a list: from typing import Sequence def spam(x:Sequence)->List[int]: ... The precise details of the syntax aren't yet finalised, but this is suggestive of what it will likely be (I hope).

...

Further, is it possible to standardise between some of the syntax/terminology, and some of the assertion types, such that they are consistent between function annotation syntaxes and docstring embedding syntaxes? Could I use function annotation for simple cases, but seamlessly move to a docstring-embedded approach for a more complex example?

That entirely depends on the tool you are using for static type analysis and/or linting. -- Steven

Ben Finney

5:53 a.m.

Steven D'Aprano writes:

...

But remember that any annotations in docstrings may not be available at runtime

How so? What conformant Python implementation is discarding docstrings from code objects?

...

Also, docstring annotations have the disadvantage of being text only, instead of expressions which evaluate to arbitrarily powerful or useful objects.

True. This is why I'm a fan of reStructuredText for docstrings, and the conventions that have arisen for using reST field lists for code annotations URL:http://sphinx-doc.org/domains.html#info-field-lists. The structure in a docstring isn't available without parsing the reST, but that seems no worse than requiring new syntax and new tools to process function annotations. I'm not arguing against function annotations, merely addressing these claims about docstrings. -- \ “The cost of a thing is the amount of what I call life which is | `\ required to be exchanged for it, immediately or in the long | _o__) run.” —Henry David Thoreau | Ben Finney

Chris Angelico

5:56 a.m.

On Wed, Aug 20, 2014 at 10:53 PM, Ben Finney wrote:

...

Steven D'Aprano writes:

...
But remember that any annotations in docstrings may not be available at runtime

How so? What conformant Python implementation is discarding docstrings from code objects?

CPython with the -OO flag. Or is that non-conformant? ChrisA

Ben Finney

1:29 p.m.

Chris Angelico writes:

...

On Wed, Aug 20, 2014 at 10:53 PM, Ben Finney wrote:

...
Steven D'Aprano writes:

...
But remember that any annotations in docstrings may not be available at runtime

How so? What conformant Python implementation is discarding docstrings from code objects?

CPython with the -OO flag. Or is that non-conformant?

Okay, one can deliberately remove docstrings with an option to the interpreter (the “-OO” option explicitly has that purpose). So a user wanting to check annotations in docstrings wouldn't use that option. So this case doesn't seem relevant to the discussion. Remember that we're talking about type annotations that are for *static code checkers* to inspect. Docstrings will certainly be available there. -- \ “… no testimony can be admitted which is contrary to reason; | `\ reason is founded on the evidence of our senses.” —Percy Bysshe | _o__) Shelley, _The Necessity of Atheism_, 1811 | Ben Finney

Steven D'Aprano

5:09 p.m.

On Thu, Aug 21, 2014 at 06:29:16AM +1000, Ben Finney wrote:

...

Chris Angelico writes:

...
On Wed, Aug 20, 2014 at 10:53 PM, Ben Finney wrote:

...
Steven D'Aprano writes:

...
But remember that any annotations in docstrings may not be available at runtime

How so? What conformant Python implementation is discarding docstrings from code objects?

CPython with the -OO flag. Or is that non-conformant?

Okay, one can deliberately remove docstrings with an option to the interpreter (the “-OO” option explicitly has that purpose). So a user wanting to check annotations in docstrings wouldn't use that option. So this case doesn't seem relevant to the discussion.

But "the user" can be two different people: the writer of the code using the annotations, and the person running the code that wants to use annotations. It's the *second* user, not the first, who decides whether or not to use -OO. If you're the original developer, you might insist that your code is not compatible with -OO, but (in my opinion) that's a mean thing to do if it can be avoided. Better to not rely on docstrings for anything other than documentation.

...

Remember that we're talking about type annotations that are for *static code checkers* to inspect. Docstrings will certainly be available there.

True, but runtime checks may (or may not) be a part of the code checker. At least, we should not rule that out. -- Steven

Ethan Furman

5:22 p.m.

On 08/20/2014 05:09 PM, Steven D'Aprano wrote:

...

On Thu, Aug 21, 2014 at 06:29:16AM +1000, Ben Finney wrote:

...
Remember that we're talking about type annotations that are for *static code checkers* to inspect. Docstrings will certainly be available there.

True, but runtime checks may (or may not) be a part of the code checker. At least, we should not rule that out.

This proposal is not about "a code checker" but about *static* typing. Seems to be a lot of people forgetting that *static* (at least in this case), means not actually running the program -- hence, no loss of docstrings. -- ~Ethan~

Steven D'Aprano

22 Aug 22 Aug

9:15 a.m.

On Wed, Aug 20, 2014 at 05:22:45PM -0700, Ethan Furman wrote:

...

On 08/20/2014 05:09 PM, Steven D'Aprano wrote:

...
On Thu, Aug 21, 2014 at 06:29:16AM +1000, Ben Finney wrote:

...
Remember that we're talking about type annotations that are for *static code checkers* to inspect. Docstrings will certainly be available there.

True, but runtime checks may (or may not) be a part of the code checker. At least, we should not rule that out.

This proposal is not about "a code checker" but about *static* typing.

Seems to be a lot of people forgetting that *static* (at least in this case), means not actually running the program -- hence, no loss of docstrings.

I'm aware of that, but I'm just saying that we shouldn't rule out the possibility of tools which operate at runtime using those same annotations. If the annotations are in the docstring, then they cannot be used at runtime with -OO. Function annotations can be used both statically and dynamically, while docstring annotations cannot be relied on to be present at runtime. -- Steven

Andrea Censi

20 Aug 20 Aug

5:56 a.m.

On Wed, Aug 20, 2014 at 5:08 AM, Tennessee Leeuwenburg wrote:

...

I was led to a conclusion: what is wrong with allowing both? Indeed, clearly both are actually already supported by various tools. So perhaps there is actually a higher-level common concept -- what are the actual assertion which are going to be supported? Can I declare a variable only to be a list, or can it be a list-of-ints?

Yes - why not both? or all three ways? Here's the "nonempty list of positive int" example done using PyContracts [1] in 3 ways: 1) Using decorators; 2) Using annotations (Python 3 only); 3) Using docstrings. The type "list[length-type](entry-type)" means a list where the length satisfies length-type and the entries satisfy entry-type. So "list[>=1](int,>0)" means a list of length at least 1 whose entries are positive integers. 1) Using decorators: @contract(l='list[>=1](int,>0)', returns='int,>0') def mysum(l): ... 2) Using annotations: @contract def mysum(l: 'list[>=1](int,>0)') -> 'int,>0': ... 3) Using docstrings, with the :type: and :rtype: tags: @contract def mysum(l): """ :type l: list[>=1](int,>0) :rtype: int,>0 """ ... If using (1) and (2), a docstring like in (3) is automatically generated. [1]: https://pypi.python.org/pypi/PyContracts Steven D'Aprano says:

...

docstring annotations have the disadvantage of being text only, instead of expressions which evaluate to arbitrarily powerful or useful objects.

I disagree, it's actually the other way around: Python's general purpose syntax is actually cumbersome with respect to a custom language for types. Once you have the freedom of using a custom language (e.g. using PyParsing) then you can create very compact and at the same time powerful contracts. For example, expressing a type such as "list[>=1](int,>0)" using a valid Python expression will take much more space. And you have the ability of creating special syntax where it makes sense, for example in Numpy --- look at this definition of matrix multiplication with compatible dimensions: @contract def matrix_multiply(a, b): ''' Multiplies two matrices together. :param a: The first matrix. Must be a 2D array. :type a: array[MxN],M>0,N>0 :param b: The second matrix. Must be of compatible dimensions. :type b: array[NxP],P>0 :rtype: array[MxP] ''' return numpy.dot(a, b) If the contract is violated, there will be a nice message saying exactly what's wrong Example: a = numpy.zeros((2,2)) b = numpy.zeros((3,2)) matrix_multiply(a,b) Exception: Breach for argument 'b' to matrix_multiply(). Expected value for 'N' was: Instance of int: 2 instead I received: Instance of int: 3 checking: N for value: Instance of int: 3 checking: NxP for value: Instance of tuple: (3, 2) checking: array[NxP] for value: array['3x2'](float64) array([[ 0., 0.], [ 0., 0.], ... [clip] checking: array[NxP],P>0 for value: array['3x2'](float64) array([[ 0., 0.], [ 0., 0.], ... [clip] best, A. -- Andrea Censi | http://censi.mit.edu | "Not all those who wander are lost." research scientist @ LIDS / Massachusetts Institute of Technology

David Mertz

10:23 a.m.

I have to say that I find the capabilities in PyContracts--which are absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile. I do not see in any of the discussion a way that mypy/typing.py could express a concept like "A list/sequence of at least N elements, each of which has some property (as well as a basic data type)." In fact, I have trouble imagining how a native syntax could do this, rather than using a custom DSL like PyContracts uses. Well, we could do it by sticking lambdas in for properties, but that would get very ugly quickly. 2) Using annotations:

...

@contract def mysum(l: 'list[>=1](int,>0)') -> 'int,>0': ...

3) Using docstrings, with the :type: and :rtype: tags:

@contract def mysum(l): """ :type l: list[>=1](int,>0) :rtype: int,>0 """

I don't really care about the annotations vs. docstring issue much. But incorporating pre/post-conditions as part of typing makes a whole lot of sense to me.

...

@contract def matrix_multiply(a, b): ''' Multiplies two matrices together.

:param a: The first matrix. Must be a 2D array. :type a: array[MxN],M>0,N>0

:param b: The second matrix. Must be of compatible dimensions. :type b: array[NxP],P>0

:rtype: array[MxP] ''' return numpy.dot(a, b)

This is also quite lovely and powerful (and not doable in mypy), as is the error report produced.

...

Example:

a = numpy.zeros((2,2)) b = numpy.zeros((3,2)) matrix_multiply(a,b)

Exception:

Breach for argument 'b' to matrix_multiply(). Expected value for 'N' was: Instance of int: 2 instead I received: Instance of int: 3 checking: N for value: Instance of int: 3 checking: NxP for value: Instance of tuple: (3, 2) checking: array[NxP] for value: array['3x2'](float64) array([[ 0., 0.], [ 0., 0.], ... [clip] checking: array[NxP],P>0 for value: array['3x2'](float64) array([[ 0., 0.], [ 0., 0.], ... [clip]

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

Bob Ippolito

10:42 a.m.

On Wed, Aug 20, 2014 at 10:23 AM, David Mertz wrote:

...

I have to say that I find the capabilities in PyContracts--which are absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile.

It's easy to check any expressible condition at runtime, but this is not the case ahead of time as with a static analysis tool or linter. It'd be great to have this sort of capability in mypy, but what you're asking for is at the fringes of current research and will not be practical to add to Python any time soon. -bob

David Mertz

10:50 a.m.

Hi Bob, I enjoyed watching your talk (on video, not live), and I certainly see the appeal of a Haskell-like type system. However, what we seem to be discussing here with mypy annotations looks a lot closer to a C type system than to a Haskell type system. All those things that PyContracts get us are easy enough in Haskell--why aim so low if we are thinking of a change in Python? On Wed, Aug 20, 2014 at 10:42 AM, Bob Ippolito wrote:

...

On Wed, Aug 20, 2014 at 10:23 AM, David Mertz wrote:

...
I have to say that I find the capabilities in PyContracts--which are absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile.

It's easy to check any expressible condition at runtime, but this is not the case ahead of time as with a static analysis tool or linter. It'd be great to have this sort of capability in mypy, but what you're asking for is at the fringes of current research and will not be practical to add to Python any time soon.

-bob

Bob Ippolito

11:14 a.m.

There's the misunderstanding: PyContracts style contracts are not "easy enough" in Haskell. mypy's types are not like a C type system. There are a few missing features that are being worked on, but it is much better than some here perceive it to be. On Wednesday, August 20, 2014, David Mertz wrote:

...

Hi Bob,

I enjoyed watching your talk (on video, not live), and I certainly see the appeal of a Haskell-like type system. However, what we seem to be discussing here with mypy annotations looks a lot closer to a C type system than to a Haskell type system. All those things that PyContracts get us are easy enough in Haskell--why aim so low if we are thinking of a change in Python?

On Wed, Aug 20, 2014 at 10:42 AM, Bob Ippolito javascript:_e(%7B%7D,'cvml','bob@redivi.com');> wrote:

...
On Wed, Aug 20, 2014 at 10:23 AM, David Mertz javascript:_e(%7B%7D,'cvml','mertz@gnosis.cx');> wrote:

...
I have to say that I find the capabilities in PyContracts--which are absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile.

It's easy to check any expressible condition at runtime, but this is not the case ahead of time as with a static analysis tool or linter. It'd be great to have this sort of capability in mypy, but what you're asking for is at the fringes of current research and will not be practical to add to Python any time soon.

-bob

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

David Mertz

11:38 a.m.

On Wed, Aug 20, 2014 at 11:14 AM, Bob Ippolito wrote:

...

There's the misunderstanding: PyContracts style contracts are not "easy enough" in Haskell.

...

mypy's types are not like a C type system. There are a few missing features that are being worked on, but it is much better than some here

Well, for example, I found something like this for Haskell: newtype Digit = Digit { digitVal :: Int } deriving (Eq, Ord, Show) mkDigit :: Int -> Maybe Digit mkDigit n | n >= 0 && n < 10 = Just (Digit n) | otherwise = Nothing OK, sure it's not just one line. But now we have a predicate-restricted data type right in the type system. If we introduce a static type system in Python, I'd like it to be able to do that. PyContracts--or something close to it--lets us do that in a DSL. But I would be equally happy to use some Python code that could be tucked away but reused. E.g., completely hypothetical syntax: class Digit(mypy.Int): def __predicate__(self): return 0 <= self < 10 def times_modulo(incr: Digit, num: Int) -> Digit: result = 0 for i in range(num): result += incr result %= 10 return result I could just stick Digit and all my other custom types in 'mytypes.py', and the actual annotations would have a richer type system, plus remain readable (if I chose decent names for the types). perceive it to be.

...

On Wednesday, August 20, 2014, David Mertz wrote:

...
Hi Bob,

I enjoyed watching your talk (on video, not live), and I certainly see

the appeal of a Haskell-like type system. However, what we seem to be discussing here with mypy annotations looks a lot closer to a C type system than to a Haskell type system. All those things that PyContracts get us are easy enough in Haskell--why aim so low if we are thinking of a change in Python?

...

...
On Wed, Aug 20, 2014 at 10:42 AM, Bob Ippolito wrote:

...
On Wed, Aug 20, 2014 at 10:23 AM, David Mertz wrote:

...
I have to say that I find the capabilities in PyContracts--which are

absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile.

...
...
It's easy to check any expressible condition at runtime, but this is

not the case ahead of time as with a static analysis tool or linter. It'd be great to have this sort of capability in mypy, but what you're asking for is at the fringes of current research and will not be practical to add to Python any time soon.

...
-bob

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

Alex Hammel

12:42 p.m.

The problem is that the proposal is to use mypy syntax for *static* type checking. It's really hard to prove that values of Digit never go below zero without doing checks at runtime. Your Haskell example doesn't do that either, actually. Sure, the value of Digit can never be a negative number, but neither is it always a positive number (it might be Nothing). Say I've got a function that requires a non-negative number to work properly, so I specify that it takes one of your Digits. If I mess up and pass it a negative number, the Digit class converts it to Nothing, resulting in a runtime error (or some exceptional runtime behaviour, depending on what I do with that Nothing). What I really want if for the compiler to say "sorry, I'm not compiling this because I can't prove that the input to this function is non-negative". You could probably do this with a sufficiently clever Digit type in Haskell, but I don't see how youc could do it with __predicate__. On Wed, Aug 20, 2014 at 11:38 AM, David Mertz wrote:

...

On Wed, Aug 20, 2014 at 11:14 AM, Bob Ippolito wrote:

...
There's the misunderstanding: PyContracts style contracts are not "easy enough" in Haskell.

Well, for example, I found something like this for Haskell:

newtype Digit = Digit { digitVal :: Int } deriving (Eq, Ord, Show) mkDigit :: Int -> Maybe Digit mkDigit n | n >= 0 && n < 10 = Just (Digit n) | otherwise = Nothing

OK, sure it's not just one line. But now we have a predicate-restricted data type right in the type system. If we introduce a static type system in Python, I'd like it to be able to do that. PyContracts--or something close to it--lets us do that in a DSL. But I would be equally happy to use some Python code that could be tucked away but reused. E.g., completely hypothetical syntax:

class Digit(mypy.Int):

def __predicate__(self):

return 0 <= self < 10

def times_modulo(incr: Digit, num: Int) -> Digit:

result = 0

for i in range(num):

result += incr

result %= 10

return result

I could just stick Digit and all my other custom types in 'mytypes.py', and the actual annotations would have a richer type system, plus remain readable (if I chose decent names for the types).

...
mypy's types are not like a C type system. There are a few missing features that are being worked on, but it is much better than some here perceive it to be.

On Wednesday, August 20, 2014, David Mertz wrote:

...
Hi Bob,

I enjoyed watching your talk (on video, not live), and I certainly see

the appeal of a Haskell-like type system. However, what we seem to be discussing here with mypy annotations looks a lot closer to a C type system than to a Haskell type system. All those things that PyContracts get us are easy enough in Haskell--why aim so low if we are thinking of a change in Python?

...
On Wed, Aug 20, 2014 at 10:42 AM, Bob Ippolito wrote:

...
On Wed, Aug 20, 2014 at 10:23 AM, David Mertz wrote:

...
I have to say that I find the capabilities in PyContracts--which are

absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile.

...
...
It's easy to check any expressible condition at runtime, but this is

not the case ahead of time as with a static analysis tool or linter. It'd be great to have this sort of capability in mypy, but what you're asking for is at the fringes of current research and will not be practical to add to Python any time soon.

...
-bob

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

_______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/

Andrew Barnert

1:14 p.m.

On Aug 20, 2014, at 12:42, Alex Hammel wrote:

...

The problem is that the proposal is to use mypy syntax for static type checking. It's really hard to prove that values of Digit never go below zero without doing checks at runtime.

Your Haskell example doesn't do that either, actually. Sure, the value of Digit can never be a negative number, but neither is it always a positive number (it might be Nothing).

Say I've got a function that requires a non-negative number to work properly, so I specify that it takes one of your Digits. If I mess up and pass it a negative number, the Digit class converts it to Nothing, resulting in a runtime error (or some exceptional runtime behaviour, depending on what I do with that Nothing). What I really want if for the compiler to say "sorry, I'm not compiling this because I can't prove that the input to this function is non-negative".

If the compiler could say, "I am compiling it because I can prove it's either non-negative or from an un-checkable source, but I'll keep track of which so I can propagate that information", that could be useful too. Of course this is only useful if uncheckable sources are rare and contained in your app, the checker makes it easy to read out what did and didn't get infected with permissiveness, and the type system makes it easy to write things so that you don't have to make each type handle permissiveness manually the way you would in Haskell. There are a couple of ML variants aimed at making this easier, and there's no reason PyConstrajnts couldn't do something similar.

...

You could probably do this with a sufficiently clever Digit type in Haskell, but I don't see how youc could do it with __predicate__.

On Wed, Aug 20, 2014 at 11:38 AM, David Mertz wrote:

...
On Wed, Aug 20, 2014 at 11:14 AM, Bob Ippolito wrote:

...
There's the misunderstanding: PyContracts style contracts are not "easy enough" in Haskell.

Well, for example, I found something like this for Haskell:

newtype Digit = Digit { digitVal :: Int } deriving (Eq, Ord, Show) mkDigit :: Int -> Maybe Digit mkDigit n | n >= 0 && n < 10 = Just (Digit n) | otherwise = Nothing

OK, sure it's not just one line. But now we have a predicate-restricted data type right in the type system. If we introduce a static type system in Python, I'd like it to be able to do that. PyContracts--or something close to it--lets us do that in a DSL. But I would be equally happy to use some Python code that could be tucked away but reused. E.g., completely hypothetical syntax:

class Digit(mypy.Int): def __predicate__(self): return 0 <= self < 10

def times_modulo(incr: Digit, num: Int) -> Digit: result = 0 for i in range(num): result += incr result %= 10 return result

I could just stick Digit and all my other custom types in 'mytypes.py', and the actual annotations would have a richer type system, plus remain readable (if I chose decent names for the types).

...
mypy's types are not like a C type system. There are a few missing features that are being worked on, but it is much better than some here perceive it to be.

On Wednesday, August 20, 2014, David Mertz wrote:

...
Hi Bob,

I enjoyed watching your talk (on video, not live), and I certainly see the appeal of a Haskell-like type system. However, what we seem to be discussing here with mypy annotations looks a lot closer to a C type system than to a Haskell type system. All those things that PyContracts get us are easy enough in Haskell--why aim so low if we are thinking of a change in Python?

On Wed, Aug 20, 2014 at 10:42 AM, Bob Ippolito wrote:

...
On Wed, Aug 20, 2014 at 10:23 AM, David Mertz wrote:

...
I have to say that I find the capabilities in PyContracts--which are absent currently in mypy--to be very compelling. If we are going to add encouragement to use type annotations, adding richer types seems extremely worthwhile.

It's easy to check any expressible condition at runtime, but this is not the case ahead of time as with a static analysis tool or linter. It'd be great to have this sort of capability in mypy, but what you're asking for is at the fringes of current research and will not be practical to add to Python any time soon.

-bob

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

-- Keeping medicines from the bloodstreams of the sick; food from the bellies of the hungry; books from the hands of the uneducated; technology from the underdeveloped; and putting advocates of freedom in prisons. Intellectual property is to the 21st century what the slave trade was to the 16th.

_______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/

_______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/

Bob Ippolito

1:03 p.m.

On Wed, Aug 20, 2014 at 11:38 AM, David Mertz wrote:

...

On Wed, Aug 20, 2014 at 11:14 AM, Bob Ippolito wrote:

...
There's the misunderstanding: PyContracts style contracts are not "easy enough" in Haskell.

Well, for example, I found something like this for Haskell:

newtype Digit = Digit { digitVal :: Int } deriving (Eq, Ord, Show) mkDigit :: Int -> Maybe Digit mkDigit n | n >= 0 && n < 10 = Just (Digit n) | otherwise = Nothing

OK, sure it's not just one line. But now we have a predicate-restricted data type right in the type system. If we introduce a static type system in Python, I'd like it to be able to do that. […]

This isn't in the type system. This is what is called a smart constructor [1]. These predicates are strictly a runtime construct, not compile time. Guard syntax (a sequence of pipes each followed by a predicate and then an equal sign and some term) is just a convenient way to write if[/else if…]/else. There are ways to do this specific sort of dependent typing [2] in Haskell using an unholy combination of GHC-specific extensions and the absolute latest compiler. This is exciting research, but not so practical today. [1] http://www.haskell.org/haskellwiki/Smart_constructors [2] http://en.wikipedia.org/wiki/Dependent_type -bob

3528

Age (days ago)

3530

Last active (days ago)

List overview

Download

16 comments

10 participants

participants (10)

Alex Hammel
Andrea Censi
Andrew Barnert
Ben Finney
Bob Ippolito
Chris Angelico
David Mertz
Ethan Furman
Steven D'Aprano
Tennessee Leeuwenburg