<div dir="ltr">The problem is that the proposal is to use mypy syntax for <i>static</i> type checking. It's really hard to prove that values of Digit never go below zero without doing checks at runtime.<br><br>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).<br>

<br>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__.<br>

</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Aug 20, 2014 at 11:38 AM, David Mertz <span dir="ltr"><<a href="mailto:mertz@gnosis.cx" target="_blank">mertz@gnosis.cx</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div class=""><div>On Wed, Aug 20, 2014 at 11:14 AM, Bob Ippolito <<a href="mailto:bob@redivi.com" target="_blank">bob@redivi.com</a>> wrote:<br>> There's the misunderstanding: PyContracts style contracts are not "easy enough" in Haskell.<br>


</div><div><br></div></div>Well, for example, I found something like this for Haskell:<br><br><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><font face="courier new, monospace">newtype Digit = Digit { digitVal :: Int }<br>


  deriving (Eq, Ord, Show)<br>mkDigit :: Int -> Maybe Digit<br>mkDigit n<br>  | n >= 0 && n < 10 = Just (Digit n)<br>  | otherwise = Nothing</font></blockquote><br>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:<div>


<br></div><div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="courier new, monospace">class Digit(mypy.Int):</font></div></blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px">


<div><font face="courier new, monospace">    def __predicate__(self):</font></div></blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="courier new, monospace">        return 0 <= self < 10</font></div>


<div><font face="courier new, monospace"><br></font></div></blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="courier new, monospace">def times_modulo(incr: Digit, num: Int) -> Digit:</font></div>


</blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="courier new, monospace">    result = 0</font></div></blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div>


<font face="courier new, monospace">    for i in range(num):</font></div></blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="courier new, monospace">        result += incr</font></div>


</blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="courier new, monospace">        result %= 10</font></div></blockquote><blockquote style="margin:0 0 0 40px;border:none;padding:0px">


<div><font face="courier new, monospace">    return result</font></div></blockquote><div><br></div>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).<div>

<div class="h5"><br>
<br>> 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.<br>><br>><br>> On Wednesday, August 20, 2014, David Mertz <<a href="mailto:mertz@gnosis.cx" target="_blank">mertz@gnosis.cx</a>> wrote:<br>


>><br>>> Hi Bob,<br>>><br>>> 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?<br>


>><br>>><br>>> On Wed, Aug 20, 2014 at 10:42 AM, Bob Ippolito <<a href="mailto:bob@redivi.com" target="_blank">bob@redivi.com</a>> wrote:<br>>>><br>>>> On Wed, Aug 20, 2014 at 10:23 AM, David Mertz <<a href="mailto:mertz@gnosis.cx" target="_blank">mertz@gnosis.cx</a>> wrote:<br>


>>>><br>>>>> 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.  <br>


>>><br>>>><br>>>> 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.<br>


>>><br>>>> -bob<br>>>><br>>><br>>><br>>><br>>> --<br>>> Keeping medicines from the bloodstreams of the sick; food<br>>> from the bellies of the hungry; books from the hands of the<br>


>> uneducated; technology from the underdeveloped; and putting<br>>> advocates of freedom in prisons.  Intellectual property is<br>>> to the 21st century what the slave trade was to the 16th.<br><br><br>


<br><br>--<br>Keeping medicines from the bloodstreams of the sick; food<br>from the bellies of the hungry; books from the hands of the<br>uneducated; technology from the underdeveloped; and putting<br>advocates of freedom in prisons.  Intellectual property is<br>


to the 21st century what the slave trade was to the 16th.</div></div></div></div>
<br>_______________________________________________<br>
Python-ideas mailing list<br>
<a href="mailto:Python-ideas@python.org">Python-ideas@python.org</a><br>
<a href="https://mail.python.org/mailman/listinfo/python-ideas" target="_blank">https://mail.python.org/mailman/listinfo/python-ideas</a><br>
Code of Conduct: <a href="http://python.org/psf/codeofconduct/" target="_blank">http://python.org/psf/codeofconduct/</a><br></blockquote></div><br></div>