[Python-ideas] Optional static typing -- late to the party

[Andrew Barnert]

On Aug 20, 2014, at 12:42, Alex Hammel <ahammel87 at gmail.com> 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 <mertz at gnosis.cx> wrote:
>> On Wed, Aug 20, 2014 at 11:14 AM, Bob Ippolito <bob at redivi.com> 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 <mertz at gnosis.cx> 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 <bob at redivi.com> wrote:
>> >>>
>> >>> On Wed, Aug 20, 2014 at 10:23 AM, David Mertz <mertz at 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.
>> 
>> 
>> 
>> 
>> --
>> 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 at python.org
>> https://mail.python.org/mailman/listinfo/python-ideas
>> Code of Conduct: http://python.org/psf/codeofconduct/
> 
> _______________________________________________
> Python-ideas mailing list
> Python-ideas at python.org
> https://mail.python.org/mailman/listinfo/python-ideas
> Code of Conduct: http://python.org/psf/codeofconduct/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20140820/b60beb00/attachment-0001.html>