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

Fri Jan 8 12:36:51 CST 2016

> On Jan 8, 2016, at 11:16 AM, Dennis Weissmann <dennis at dennisweissmann.me> wrote:
> 
>> 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.

> 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 at swift.org <mailto:swift-evolution at swift.org>> wrote:
>> 
>>> 
>>> On Jan 7, 2016, at 9:32 AM, Jérôme Duquennoy via swift-evolution <swift-evolution at swift.org <mailto: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 <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 <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 <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 <https://lists.swift.org/mailman/listinfo/swift-evolution>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20160108/17245c62/attachment.html>