[swift-evolution] Proposal: named invariants for variable declarations

[Jérôme Duquennoy]

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 at 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 at 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 at 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 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

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