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

[Matthew Johnson]

> On Jan 7, 2016, at 9:32 AM, Jérôme Duquennoy via swift-evolution <swift-evolution at 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 <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 at swift.org <mailto: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 <mailto: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 <mailto: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 <mailto:swift-evolution at swift.org>
>>>> 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
> 
> 
> _______________________________________________
> 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/e25d1c10/attachment.html>