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

[Alex Hammel]

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 <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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20140820/ba1c6ab6/attachment-0001.html>