Code Contracts


(Suminda Dharmasena) #1

Hello,

One feature that might be very useful to have in Swift is code contracts.
Is it possible to see how this can be added to the language?

Suminda


(Javier Soto) #2

Hi!

Maybe it's unfamiliarity on my part, but "code contract" seems like a very
vague term.
Do you have an example of what this could look like in swift and what the
benefits of such feature would be?

Thanks!

···

On Wed, Jan 13, 2016 at 6:59 PM Suminda Dharmasena via swift-evolution < swift-evolution@swift.org> wrote:

Hello,

One feature that might be very useful to have in Swift is code contracts.
Is it possible to see how this can be added to the language?

Suminda
_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

--
Javier Soto


(Suminda Dharmasena) #3

E.g.

   1. var @where("myVariable <= 100 && myVariable >= 0") myVariable = 42

   1. @where("myVariable <= 80 && myVariable >= 50")
   2. {
   3. ...
   4. }

   1. @where("score <= 100 && score >= 0")
   2. for score in individualScores {
   3. ...
   4. }


(David Sweeris) #4

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/

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.

- Dave Sweeris

···

On Jan 14, 2016, at 20:32, Suminda Dharmasena via swift-evolution <swift-evolution@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@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Robert Widmann) #5

Mhm, -1 for this reason. If there were richer preconditions (say, a refinement typing scheme) here rather than C0-style contracts it'd be worth the extra syntax.

~Robert Widmann

2016/01/14 23:36、Javier Soto via swift-evolution <swift-evolution@swift.org> のメッセージ:

···

Is this something that in your opinion is worth extra, special syntax? Those examples could be implement easily like:

didSet {
precondition(score <= 100)
}

On Thu, Jan 14, 2016 at 8:32 PM Suminda Dharmasena <sirinath1978m@gmail.com> 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 {
    ...
}

--
Javier Soto
_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Javier Soto) #6

Is this something that in your opinion is worth extra, special syntax?
Those examples could be implement easily like:

didSet {
precondition(score <= 100)
}

···

On Thu, Jan 14, 2016 at 8:32 PM Suminda Dharmasena <sirinath1978m@gmail.com> wrote:

E.g.

   1. var @where("myVariable <= 100 && myVariable >= 0") myVariable = 42

   1. @where("myVariable <= 80 && myVariable >= 50")
   2. {
   3. ...
   4. }

   1. @where("score <= 100 && score >= 0")
   2. for score in individualScores {
   3. ...
   4. }

--

Javier Soto


(Dennis Weissmann) #7

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/

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 :innocent:) which need to be thought of before the finalization.

- Dennis

···

On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution@swift.org> wrote:

- Dave Sweeris

On Jan 14, 2016, at 20:32, Suminda Dharmasena via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@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@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution


(Suminda Dharmasena) #8

This is how C# does it -
https://msdn.microsoft.com/en-us/library/dd264808(v=vs.110).aspx

There is a language called WhyML which has it buildin -
http://why3.lri.fr/doc-0.80/manual004.html. Another such language is:
http://whiley.org/ and Ada (Spark subset) :
https://en.wikipedia.org/wiki/SPARK_(programming_language)

In F* see section on "Statically checked assertions" -
https://www.fstar-lang.org/tutorial/

This can give a better idea on available syntax and how this can be adopted
to Swift.


(Haravikk) #9

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

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

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.

- Haravikk

···

On 15 Jan 2016, at 12:27, Dennis Weissmann via swift-evolution <swift-evolution@swift.org> wrote:

On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@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/

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 :innocent:) 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@swift.org <mailto:swift-evolution@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@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Dennis Weissmann) #10

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 :slight_smile:

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 :slight_smile: If the type is precise enough the compiler can actually write (infer) a lot of your code)

···

On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution@haravikk.com> wrote:

- Haravikk

On 15 Jan 2016, at 12:27, Dennis Weissmann via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@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/

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 :innocent:) 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@swift.org <mailto:swift-evolution@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@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org <mailto:swift-evolution@swift.org>
https://lists.swift.org/mailman/listinfo/swift-evolution


(Sean Heber) #11

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@swift.org> wrote:

On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution@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 :slight_smile:

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 :slight_smile: 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@swift.org> wrote:

On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution@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 :innocent:) 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@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@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Dennis Weissmann) #12

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 :thinking:):
    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@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@swift.org> wrote:

On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution@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 :slight_smile:

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 :slight_smile: 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@swift.org> wrote:

On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution@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 :innocent:) 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@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@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Sean Heber) #13

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@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 :thinking:):
    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@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@swift.org> wrote:

On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution@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 :slight_smile:

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 :slight_smile: 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@swift.org> wrote:

On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution@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 :innocent:) 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@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@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Matt Whiteside) #14

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 :slight_smile:

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

···

On Jan 15, 2016, at 8:53 AM, Dennis Weissmann via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution@haravikk.com <mailto:swift-evolution@haravikk.com>> wrote:


(TJ Usiyan) #15

From what I understand of the goals of Swift, I think that any addition to

runtime machinery will be hard won. The Swift runtime is deliberately
small. I completely support refinement types and their logical conclusion
of dependent types but I don't think that the approach of "runtime checking
until capable of compile time checking" will gain much traction. I suggest
that we work primarily on creating a syntax so that, by the time that we
can implement it in the compiler, we have a truly compelling case.
TJ

···

On Sat, Jan 16, 2016 at 6:04 PM, Matt Whiteside via swift-evolution < swift-evolution@swift.org> wrote:

On Jan 15, 2016, at 8:53 AM, Dennis Weissmann via swift-evolution < > swift-evolution@swift.org> wrote:

On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution@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 :slight_smile:

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

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution