[swift-evolution] Code Contracts
Sean Heber
sean at fifthace.com
Fri Jan 15 10:55:06 CST 2016
The “where” keyword makes a lot of sense - I like it. I use “where” this way myself all over the place in for loops, etc, so it’s a pretty natural thing to imagine it showing up here, IMO. To me the most important aspect of this would be to ensure the compiler could (eventually) prove as many of them as possible at compile time and emit the appropriate warnings/errors.
I think this sort of idea would pair nicely with the “newtype” concept, but I have not been following that discussion and don’t know all of the details there. Perhaps something like:
newtype Scaler = Float where self >= -1 && self <= 1
And that would create a new distinct type called Scaler that is based on Float but with those value ranges applied as a kind of contract where the compiler would attempt to ensure as much as it can at compile time, and when not possible, could insert precondition() checks appropriately to catch mistakes at runtime.
For example:
func scaleSomething(amount: Scalar) {
var newAmount: Scalar = amount * 2 // allowed since it cannot prove this *always* violates the rule
precondition(newAmount >= -1 && newAmount <= 1) // inserted by the compiler due to the ambiguity of previous line
newAmount = amount + 5 // ideally this is a compiler error since there’s no way this doesn’t violate the rules for Scalar
}
func doThing(val: Float) {
precondition(val >= -1 && val <= 1) // inserted by the compiler because we’re “converting” a bare Float to a Scaler and we don’t know the value here
scaleSomething(val)
}
let var: Float = 42
scaleSomething(val) // compiler error since it can plainly see that 42 is not a valid scalar value
l8r
Sean
> On Jan 15, 2016, at 10:30 AM, Dennis Weissmann <dennis at dennisweissmann.me> wrote:
>
> Hey Sean,
>
> + 1
>
> That’s indeed very similar, I must have overlooked your email in the flood of emails at the time.
>
> Especially
>
>> I like the idea of this always being a compile-time check when possible, but it could also be useful to force the requirement to be evaluated at runtime by adding a force operator to it:
>>
>> func scale(x: Float in! 0…1) -> Float {
>> return someValue * x
>> }
>> In this scenario the compiler would probably still try to prove it statically - and if it could, it’d skip runtime checks - but if it cannot, it would then insert runtime guards that catch requirement failures and crash as necessary - similar to a forced unwrap - instead of being a compile time error.
>
> The reasons I think `in` isn’t the best choice for this keyword are
>
> - `in` already is a keyword with a totally different meaning
> - a range is just an example of such a predicate, here are some examples (using the `Type` version of my last email, though I think the name doesn’t make much sense, we’re refining the type, yes, but the calculation in the predicate is applied to an instance of that type 🤔):
> 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
>
>> On Jan 15, 2016, at 4:41 PM, Sean Heber <sean at fifthace.com> wrote:
>>
>> I had a similar idea in the early days of the mailing list before I knew it had a name. I don’t think it got much (any, really) discussion at the time: https://lists.swift.org/pipermail/swift-evolution/2015-December/000022.html
>>
>> l8r
>> Sean
>>
>>
>>> On Jan 15, 2016, at 8:53 AM, Dennis Weissmann via swift-evolution <swift-evolution at swift.org> wrote:
>>>
>>>>
>>>> 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> wrote:
>>>>>
>>>>>> On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution at swift.org> wrote:
>>>>>>
>>>>>> This is the same thing as Refinement Types, right?
>>>>>> 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/
>>>>>>
>>>>>
>>>>> 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):
>>>>>
>>>>> 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) or me (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> 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
>>>>>>> https://lists.swift.org/mailman/listinfo/swift-evolution
>>>>>>
>>>>>> _______________________________________________
>>>>>> swift-evolution mailing list
>>>>>> swift-evolution at swift.org
>>>>>> https://lists.swift.org/mailman/listinfo/swift-evolution
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> swift-evolution mailing list
>>>>> swift-evolution at swift.org
>>>>> https://lists.swift.org/mailman/listinfo/swift-evolution
>>>>
>>>
>>> _______________________________________________
>>> swift-evolution mailing list
>>> swift-evolution at swift.org
>>> https://lists.swift.org/mailman/listinfo/swift-evolution
>>
>
More information about the swift-evolution
mailing list