[swift-evolution] Code Contracts

[Matt Whiteside]

>>> On Jan 15, 2016, at 8:53 AM, Dennis Weissmann via swift-evolution <swift-evolution at swift.org <mailto:swift-evolution at swift.org>> wrote:
>>> 
>>>> 
>>>> On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution at haravikk.com <mailto:swift-evolution at haravikk.com>> wrote:
>>>> 
>>>> This is pretty interesting; while the actual compile-time type-checking could be complex and take some time to implement, it seems to me that the actual notation could be implemented in advance and simply perform runtime assertions until the real type-checking is ready? In cases where the type-checker can’t be certain of a value’s safety, a run-time assertion might make sense anyway, so this short-term behaviour could actually be left in, with the caveat being that your restriction could still fail at run-time (which is what I think most people would want when the compile-time check isn’t enough).
>>>> 
>>> 
>>> That’s an interesting approach! I like it :)

I agree this approach is interesting, and I’ve had similar thoughts.

Regarding your syntax idea,

>     typealias RGBAInt = Int where Type >= 0 && Type <= 255                            // Can be rewritten as a range (0...255)
>     typealias RGBADouble = Double where Type >= 0 && Type <= 1.0                      // Can be rewritten as a range (0...1.0)
>     typealias BatteryLevel = Int where Type >= 0 && Type <= 100                       // Can be rewritten as a range (0...100)
>     typealias Primes10 = Int where Type == 2 || Type == 3 || Type == 5 || Type == 7   // Cannot be rewritten as a range
>     typealias EvenNumber = Int where Type % 2 == 0                                    // Cannot be rewritten as a range
>   
> What do you think?
> 
> - Dennis

I was discussing something like this on another thread, about compile time execution, and this is close to the syntax that I imagined.  The only thing I might suggest is that `typealias` doesn't seem like the ideal keyword here, since that is meant to indicate that the 2 types are one and the same.  These are some options that I thought might be good:

struct InvertibleMatrix: SquareMatrix where determinant() != 0 

typedef InvertibleMatrix = SquareMatrix where determinant() != 0 

typerefinement InvertibleMatrix = SquareMatrix where determinant() != 0 

Matt




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20160116/a11ef0ee/attachment.html>