[swift-evolution] Code Contracts

Fri Jan 15 08:53:39 CST 2016

> On Jan 15, 2016, at 1:56 PM, Haravikk <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’d be particularly interested in getting the notation available sooner if it's concise enough to make it worth using in place of current if statements. For example, it’d be nice if there were some shorthand for integers, as these seem like they’d be a particularly common use-case, for example:
> 
> var @where(“0 <= myVariable <= 100”) myVariable = 42
> var @where(“0 <= $1 <= 100) myVariable = 42
> 
> Though personally I’d prefer something even more concise like:
> 
> var myVariable(0…100) = 42
> var myVariable:Int(0…100) = 42
> 

I don’t like the @where syntax too much either (but I don’t have the time right now to come up with a better, well-thought-out and practical syntax myself).
Here are just some quick thoughts:

// Annotating the type
let value: Int<1...100> = 42                // Generics?
let value: Int(1...100) = 42                // Initializer?
let value: Int{1...100} = 42                // Scope?
let value: {value: Int | 1...100} = 42      // LiquidHaskell
let value: Int where Type == 1...100 = 42   // `where` already is a keyword that acts very similar (but at runtime)

// Annotating the variable (the inferred type)
let value<1...100> = 42
let value(1...100) = 42
let value{1...100} = 42
let value{value: Int | 1...100} = 42
let value where Type == 1...100 = 42

Even though it is more verbose, I like the last approach best. I think the common use-case is to predefine some very common ones (e.g. RGBA) in typealiases like so:

typealias RGBAValue = Int where Type == 0...255

This makes it much nicer (IMO) to declare (e.g.) functions. `UIColor` for example could gain an initializer taking values from 0 to 255:

init(red: RGBAValue, green: RGBAValue, blue: RGBAValue, alpha: RGBAValue)

> Leaving the @where clause for more complex (i.e- non-numeric) cases. A really powerful alternative would be to allow us some mechanism to define how to handle restrictions in our classes and structs; these would be compiled first so that they can be executed by the type checker (which may limit what they can do) but could allow us full control of how they work. So, for example, an integer definition might look like:
> 
> struct Int… {
> 	...
> 	restriction(range:Range<Int>) -> Bool { return range.contains(self) }
> }
> var myVariable(0…100) = 42
> 
> At run-time this would be equivalent to:
> 
> var myVariable = 42
> assert(myVariable.restriction(0…100), “Value of myVariable is out of bounds [0…100]”)
> 
> With the idea being that in future the type-checker would call the restriction check, find 42 to be in range and omit the assertion entirely.
> 
> Just some thoughts, but the main thing for me is that this is something that I’d like to use a lot if implemented, so the more concise it can be, the better.
> 
Exactly :) If the type is precise enough the compiler can actually write (infer) a lot of your code)

> - Haravikk
> 
>> On 15 Jan 2016, at 12:27, Dennis Weissmann via swift-evolution <swift-evolution at swift.org <mailto:swift-evolution at swift.org>> wrote:
>> 
>>> On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution at swift.org <mailto:swift-evolution at swift.org>> wrote:
>>> 
>>> This is the same thing as Refinement Types, right?
>>> https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_types <https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_types>
>>> http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ <http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/>
>>> 
>> 
>> Yes, it seems they are. There is a pretty nice and easy to understand explanation [here](https://github.com/tomprimozic/type-systems/tree/master/refined_types <https://github.com/tomprimozic/type-systems/tree/master/refined_types>):
>> 
>> Refined types or contracts are a restricted form of dependent types that combine base datatypes with logical predicates; for example, the type of natural numbers could be written x : int if x ≥ 0 (the notation most commonly used in academic literature is {ν : int | ν ≥ 0}).
>> 
>>> I’m in favor of it, but I think someone’s already made that suggestion… At the very least, I didn’t know what the phrase meant until a few days ago, and I know I learned about it from reading something on swift-evolution.
>> 
>> That was probably Matthew (https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005925.html <https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005925.html>) or me (https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005918.html <https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005918.html>) - the thread is called 'Proposal: named invariants for variable declarations'
>> 
>> And I agree with Matthew that this won’t happen anytime soon. That’s why I didn’t want to discuss that topic too much. It’s just that the ABI will be finalized later this year and I wanted to mention that there is definitely interest in this area in case some ABI-related things are needed for refinement types (or even dependent types, someday, one can dream 😇) which need to be thought of before the finalization.
>> 
>> - Dennis
>> 
>>> - Dave Sweeris
>>> 
>>>> On Jan 14, 2016, at 20:32, Suminda Dharmasena via swift-evolution <swift-evolution at swift.org <mailto:swift-evolution at swift.org>> wrote:
>>>> 
>>>> E.g. 
>>>> 
>>>> var @where("myVariable <= 100 && myVariable >= 0") myVariable = 42
>>>> 
>>>> 
>>>> @where("myVariable <= 80 && myVariable >= 50")
>>>> {
>>>>     ...
>>>> }
>>>> 
>>>> 
>>>> @where("score <= 100 && score >= 0")
>>>> for score in individualScores {
>>>>     ...
>>>> }
>>>>  _______________________________________________
>>>> swift-evolution mailing list
>>>> swift-evolution at swift.org <mailto:swift-evolution at swift.org>
>>>> https://lists.swift.org/mailman/listinfo/swift-evolution <https://lists.swift.org/mailman/listinfo/swift-evolution>
>>> 
>>>  _______________________________________________
>>> swift-evolution mailing list
>>> swift-evolution at swift.org <mailto:swift-evolution at swift.org>
>>> https://lists.swift.org/mailman/listinfo/swift-evolution <https://lists.swift.org/mailman/listinfo/swift-evolution>
>> 
>> _______________________________________________
>> swift-evolution mailing list
>> swift-evolution at swift.org <mailto:swift-evolution at swift.org>
>> https://lists.swift.org/mailman/listinfo/swift-evolution
> 

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