Proposal: named invariants for variable declarations


(Amir Michail) #1

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error


(Howard Lovatt) #2

Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.

···

On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <swift-evolution@swift.org> wrote:

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error

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


(Árpád Goretity) #3

This suspiciously starts to resemble a mixture of dependent types and explicit contracts (something like the Midori variant of C#).

By the way, while we are at it: if the compiler supports this kind of feature, we could (and should) statically check most of the constraints. Accordingly, in your example, f(-3) would be a compiler error (the two pure invariants applied to the constant argument would both trivially constant-fold to false).

···

Sent from my iPhone

On 04 Jan 2016, at 21:33, Howard Lovatt <howard.lovatt@gmail.com> wrote:

Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.

On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <swift-evolution@swift.org> wrote:

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error

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


(Jerome Duquennoy) #4

Hi everyone

There are multiple discussions ongoing related to typing currently.
Two other discussions that are related are :
- Support for newtype feature/typesafe calculations
- Type Safe Algorithms

I also have the feeling all those discussions are moving toward a more advanced typing system, with things such as type hierarchy, and contracts.
One such system I have worked with is implemented the Ada language (a language that also emphasise on making code secure).
In that language, you have the possibility to build a full hierarchy of types and subtypes. For exemple, by default, there is a Natural type, that is a subtype of Integer, that can only receive values >= 0. There is another subtype called Positive, that can only receive values > 0.
Ada has plenty of possibilities that can be great thanks to that typing system. For exemple:
- there is a notion of compatibility between types and subtypes, which enable such things as declaring a “NumberOfMelons” type and a “NumberOfApples” type, and have the compiler warn you that you cannot add melons and apple when you try to do such operations.
- it makes it possible to declare mod types, with values that will cycle between two values
- it makes it possible to request a float type that will provide a given precision on a range of values (no need for the dev to think “should I use a double or would a simple float be enough ?”
- ...

Type invariants and subtypes predicates were added in Ada 2012 (see https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI).
There is an explanation of the Ada typing system here : https://en.wikibooks.org/wiki/Ada_Programming/Type_System

The system is pretty complex (maybe a bit too much sometimes), but maybe it could be a great source of inspiration for a big evolution toward a typing system that would be even more robust that Swift’s current one.
That might address all three discussions (this one, and the two other ones, listed at the beginning of this message).
I haven’t thought a lot about that, and it is probably beyong my current skills to design a typing system. So i’m just throwing some vague ideas here. But I definitely find that topic very interesting : Swift’s orientation toward code safety is super appealing to me, if we can take it one step further with an evolution of the typing system, I’m all for it :-).

What do you think guys ?

Jerome

···

On 05 Jan 2016, at 07:20, Árpád Goretity via swift-evolution <swift-evolution@swift.org> wrote:

This suspiciously starts to resemble a mixture of dependent types and explicit contracts (something like the Midori variant of C#).

By the way, while we are at it: if the compiler supports this kind of feature, we could (and should) statically check most of the constraints. Accordingly, in your example, f(-3) would be a compiler error (the two pure invariants applied to the constant argument would both trivially constant-fold to false).

Sent from my iPhone

On 04 Jan 2016, at 21:33, Howard Lovatt <howard.lovatt@gmail.com> wrote:

Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.

On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <swift-evolution@swift.org> wrote:

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error

_______________________________________________
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


(Matthew Johnson) #5

Hi everyone

There are multiple discussions ongoing related to typing currently.
Two other discussions that are related are :
- Support for newtype feature/typesafe calculations
- Type Safe Algorithms

I also have the feeling all those discussions are moving toward a more advanced typing system, with things such as type hierarchy, and contracts.
One such system I have worked with is implemented the Ada language (a language that also emphasise on making code secure).
In that language, you have the possibility to build a full hierarchy of types and subtypes. For exemple, by default, there is a Natural type, that is a subtype of Integer, that can only receive values >= 0. There is another subtype called Positive, that can only receive values > 0.
Ada has plenty of possibilities that can be great thanks to that typing system. For exemple:
- there is a notion of compatibility between types and subtypes, which enable such things as declaring a “NumberOfMelons” type and a “NumberOfApples” type, and have the compiler warn you that you cannot add melons and apple when you try to do such operations.
- it makes it possible to declare mod types, with values that will cycle between two values
- it makes it possible to request a float type that will provide a given precision on a range of values (no need for the dev to think “should I use a double or would a simple float be enough ?”
- ...

Type invariants and subtypes predicates were added in Ada 2012 (see https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI <https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI>).
There is an explanation of the Ada typing system here : https://en.wikibooks.org/wiki/Ada_Programming/Type_System

The system is pretty complex (maybe a bit too much sometimes), but maybe it could be a great source of inspiration for a big evolution toward a typing system that would be even more robust that Swift’s current one.
That might address all three discussions (this one, and the two other ones, listed at the beginning of this message).
I haven’t thought a lot about that, and it is probably beyong my current skills to design a typing system. So i’m just throwing some vague ideas here. But I definitely find that topic very interesting : Swift’s orientation toward code safety is super appealing to me, if we can take it one step further with an evolution of the typing system, I’m all for it :-).

What do you think guys ?

I don’t know Ada so I won’t comment on that part.

As far as type system enhancements go, refinement types look very interesting as a possible direction supporting the kind of thing discussed in this thread. I don’t expect enhancements like this will be considered any time soon though.

···

On Jan 7, 2016, at 9:32 AM, Jérôme Duquennoy via swift-evolution <swift-evolution@swift.org> wrote:

Jerome

On 05 Jan 2016, at 07:20, Árpád Goretity via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

This suspiciously starts to resemble a mixture of dependent types and explicit contracts (something like the Midori variant of C#).

By the way, while we are at it: if the compiler supports this kind of feature, we could (and should) statically check most of the constraints. Accordingly, in your example, f(-3) would be a compiler error (the two pure invariants applied to the constant argument would both trivially constant-fold to false).

Sent from my iPhone

On 04 Jan 2016, at 21:33, Howard Lovatt <howard.lovatt@gmail.com <mailto:howard.lovatt@gmail.com>> wrote:

Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.

On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error

_______________________________________________
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) #6

As far as type system enhancements go, refinement types look very interesting as a possible direction supporting the kind of thing discussed in this thread. I don’t expect enhancements like this will be considered any time soon though.

So do I. Refinement types are very interesting and promising (I have a radar open on that) and I think that powerful type systems are the future.

However, what do you (all) think about going one step further and introducing dependent types (Disclaimer: I’m not at all an expert on dependent types - just learning Idris right now.)?

“Dependent types” basically means that types are first-class citizens (i.e. they can be passed as arguments, returned from functions and be used and manipulated just like values) and can be computed from (or be dependent on) a value.

This allows (e.g.) for
making sure you’re not accessing an array’s element that is out of bounds (without runtime checks)
validating that a string conforms to a specific DSL (e.g. Regular expressions, Autolayout, printf-like strings [e.g. NSLocalizedString])
calculate types of functions (e.g. the number and type of it’s arguments, the return type) based on one or more values
formally proving a program (or a function) correct
And all this happens at compile time!

Just like refinement types they can be used where you *want* (or need) them (data model, etc.) but you don’t have to use them (e.g. UI).

This is not (if at all) gonna happen anytime soon but maybe it’s worth discussing this change now (at least superficially) as it touches upon some of the discussions in other threads, too. In addition to that, I have no idea whether or not dependent types (or refinement types for that matter) have an implication on the language ABI which will be finalized later this year - so maybe we need to discuss a bit of this now to make sure nothing prevents it from being implemented in the future.

- Dennis

···

On Jan 7, 2016, at 7:31 PM, Matthew Johnson via swift-evolution <swift-evolution@swift.org> wrote:

On Jan 7, 2016, at 9:32 AM, Jérôme Duquennoy via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

Hi everyone

There are multiple discussions ongoing related to typing currently.
Two other discussions that are related are :
- Support for newtype feature/typesafe calculations
- Type Safe Algorithms

I also have the feeling all those discussions are moving toward a more advanced typing system, with things such as type hierarchy, and contracts.
One such system I have worked with is implemented the Ada language (a language that also emphasise on making code secure).
In that language, you have the possibility to build a full hierarchy of types and subtypes. For exemple, by default, there is a Natural type, that is a subtype of Integer, that can only receive values >= 0. There is another subtype called Positive, that can only receive values > 0.
Ada has plenty of possibilities that can be great thanks to that typing system. For exemple:
- there is a notion of compatibility between types and subtypes, which enable such things as declaring a “NumberOfMelons” type and a “NumberOfApples” type, and have the compiler warn you that you cannot add melons and apple when you try to do such operations.
- it makes it possible to declare mod types, with values that will cycle between two values
- it makes it possible to request a float type that will provide a given precision on a range of values (no need for the dev to think “should I use a double or would a simple float be enough ?”
- ...

Type invariants and subtypes predicates were added in Ada 2012 (see https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI <https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI>).
There is an explanation of the Ada typing system here : https://en.wikibooks.org/wiki/Ada_Programming/Type_System

The system is pretty complex (maybe a bit too much sometimes), but maybe it could be a great source of inspiration for a big evolution toward a typing system that would be even more robust that Swift’s current one.
That might address all three discussions (this one, and the two other ones, listed at the beginning of this message).
I haven’t thought a lot about that, and it is probably beyong my current skills to design a typing system. So i’m just throwing some vague ideas here. But I definitely find that topic very interesting : Swift’s orientation toward code safety is super appealing to me, if we can take it one step further with an evolution of the typing system, I’m all for it :-).

What do you think guys ?

I don’t know Ada so I won’t comment on that part.

As far as type system enhancements go, refinement types look very interesting as a possible direction supporting the kind of thing discussed in this thread. I don’t expect enhancements like this will be considered any time soon though.

Jerome

On 05 Jan 2016, at 07:20, Árpád Goretity via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

This suspiciously starts to resemble a mixture of dependent types and explicit contracts (something like the Midori variant of C#).

By the way, while we are at it: if the compiler supports this kind of feature, we could (and should) statically check most of the constraints. Accordingly, in your example, f(-3) would be a compiler error (the two pure invariants applied to the constant argument would both trivially constant-fold to false).

Sent from my iPhone

On 04 Jan 2016, at 21:33, Howard Lovatt <howard.lovatt@gmail.com <mailto:howard.lovatt@gmail.com>> wrote:

Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.

On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error

_______________________________________________
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

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


(Matthew Johnson) #7

As far as type system enhancements go, refinement types look very interesting as a possible direction supporting the kind of thing discussed in this thread. I don’t expect enhancements like this will be considered any time soon though.

So do I. Refinement types are very interesting and promising (I have a radar open on that) and I think that powerful type systems are the future.

However, what do you (all) think about going one step further and introducing dependent types (Disclaimer: I’m not at all an expert on dependent types - just learning Idris right now.)?

“Dependent types” basically means that types are first-class citizens (i.e. they can be passed as arguments, returned from functions and be used and manipulated just like values) and can be computed from (or be dependent on) a value.

Dependent types are interesting, but add a lot of complexity to the programmer model. The most interesting thing about refinement types is that they can achieve many of the same safety guarantees as dependent types, but with a much simpler programmer model.

The good news is that they are not mutually exclusive.

This allows (e.g.) for
making sure you’re not accessing an array’s element that is out of bounds (without runtime checks)

I’m pretty sure refinement types can do this, at least in many cases. I’m not sure about the rest of your list.

···

On Jan 8, 2016, at 11:16 AM, Dennis Weissmann <dennis@dennisweissmann.me> wrote:

validating that a string conforms to a specific DSL (e.g. Regular expressions, Autolayout, printf-like strings [e.g. NSLocalizedString])
calculate types of functions (e.g. the number and type of it’s arguments, the return type) based on one or more values
formally proving a program (or a function) correct
And all this happens at compile time!

Just like refinement types they can be used where you *want* (or need) them (data model, etc.) but you don’t have to use them (e.g. UI).

This is not (if at all) gonna happen anytime soon but maybe it’s worth discussing this change now (at least superficially) as it touches upon some of the discussions in other threads, too. In addition to that, I have no idea whether or not dependent types (or refinement types for that matter) have an implication on the language ABI which will be finalized later this year - so maybe we need to discuss a bit of this now to make sure nothing prevents it from being implemented in the future.

- Dennis

On Jan 7, 2016, at 7:31 PM, Matthew Johnson via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

On Jan 7, 2016, at 9:32 AM, Jérôme Duquennoy via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

Hi everyone

There are multiple discussions ongoing related to typing currently.
Two other discussions that are related are :
- Support for newtype feature/typesafe calculations
- Type Safe Algorithms

I also have the feeling all those discussions are moving toward a more advanced typing system, with things such as type hierarchy, and contracts.
One such system I have worked with is implemented the Ada language (a language that also emphasise on making code secure).
In that language, you have the possibility to build a full hierarchy of types and subtypes. For exemple, by default, there is a Natural type, that is a subtype of Integer, that can only receive values >= 0. There is another subtype called Positive, that can only receive values > 0.
Ada has plenty of possibilities that can be great thanks to that typing system. For exemple:
- there is a notion of compatibility between types and subtypes, which enable such things as declaring a “NumberOfMelons” type and a “NumberOfApples” type, and have the compiler warn you that you cannot add melons and apple when you try to do such operations.
- it makes it possible to declare mod types, with values that will cycle between two values
- it makes it possible to request a float type that will provide a given precision on a range of values (no need for the dev to think “should I use a double or would a simple float be enough ?”
- ...

Type invariants and subtypes predicates were added in Ada 2012 (see https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI <https://books.google.fr/books?id=req3AwAAQBAJ&pg=PA399&lpg=PA399&dq=ada+type+invariants&source=bl&ots=5pinYE9PSc&sig=aKeNIEfsG0r2xeiNBOcPoEkvERw&hl=fr&sa=X&sqi=2&ved=0ahUKEwjVxd6g_pfKAhWH1xQKHZh6BroQ6AEIXjAI>).
There is an explanation of the Ada typing system here : https://en.wikibooks.org/wiki/Ada_Programming/Type_System

The system is pretty complex (maybe a bit too much sometimes), but maybe it could be a great source of inspiration for a big evolution toward a typing system that would be even more robust that Swift’s current one.
That might address all three discussions (this one, and the two other ones, listed at the beginning of this message).
I haven’t thought a lot about that, and it is probably beyong my current skills to design a typing system. So i’m just throwing some vague ideas here. But I definitely find that topic very interesting : Swift’s orientation toward code safety is super appealing to me, if we can take it one step further with an evolution of the typing system, I’m all for it :-).

What do you think guys ?

I don’t know Ada so I won’t comment on that part.

As far as type system enhancements go, refinement types look very interesting as a possible direction supporting the kind of thing discussed in this thread. I don’t expect enhancements like this will be considered any time soon though.

Jerome

On 05 Jan 2016, at 07:20, Árpád Goretity via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

This suspiciously starts to resemble a mixture of dependent types and explicit contracts (something like the Midori variant of C#).

By the way, while we are at it: if the compiler supports this kind of feature, we could (and should) statically check most of the constraints. Accordingly, in your example, f(-3) would be a compiler error (the two pure invariants applied to the constant argument would both trivially constant-fold to false).

Sent from my iPhone

On 04 Jan 2016, at 21:33, Howard Lovatt <howard.lovatt@gmail.com <mailto:howard.lovatt@gmail.com>> wrote:

Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.

On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <swift-evolution@swift.org <mailto:swift-evolution@swift.org>> wrote:

Examples:

invariant vectorIndex(v:Int) { return 0..<3 ~= v }

var i:Int,vectorIndex: = 2
i = 3 // run-time error

invariant positive(v:Int) { return v > 0 }
invariant odd(v:Int) { return v % 2 == 1 }

var x:Int, positive, odd = 5

x = 2 // run-time error

func f(z:Int, positive, odd) {

}

f(-3) // run-time error

_______________________________________________
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

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