<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Jan 8, 2016, at 11:16 AM, Dennis Weissmann <<a href="mailto:dennis@dennisweissmann.me" class="">dennis@dennisweissmann.me</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69); min-height: 14px;" class=""><blockquote type="cite" class=""><div class=""><div class="">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.</div></div></blockquote><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">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.</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69); min-height: 14px;" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">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.)?</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69); min-height: 14px;" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">“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.</div></div></div></blockquote><div><br class=""></div><div>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. </div><div><br class=""></div><div>The good news is that they are not mutually exclusive.</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69); min-height: 14px;" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">This allows (e.g.) for</div>
<ul class="">
<li style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">making sure you’re not accessing an array’s element that is out of bounds (without runtime checks)</li></ul></div></div></blockquote><div>I’m pretty sure refinement types can do this, at least in many cases. I’m not sure about the rest of your list.</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><ul class="">
<li style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">validating that a string conforms to a specific DSL (e.g. Regular expressions, Autolayout, printf-like strings [e.g. NSLocalizedString])</li>
<li style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">calculate types of functions (e.g. the number and type of it’s arguments, the return type) based on one or more values</li>
<li style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">formally proving a program (or a function) correct</li></ul><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">And all this happens at compile time!</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69); min-height: 14px;" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">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).</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69); min-height: 14px;" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">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.</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class=""><br class=""></div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class="">- Dennis</div><div style="margin: 0px; line-height: normal; color: rgb(69, 69, 69);" class=""><br class=""></div><div class=""><blockquote type="cite" class=""><div class="">On Jan 7, 2016, at 7:31 PM, Matthew Johnson via swift-evolution <<a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" class=""><div class=""><br class="Apple-interchange-newline">On Jan 7, 2016, at 9:32 AM, Jérôme Duquennoy via swift-evolution <<a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="">Hi everyone</div><div class=""><br class=""></div><div class="">There are multiple discussions ongoing related to typing currently.</div><div class="">Two other discussions that are related are :</div><div class="">- <span class="" style="font-family: 'Helvetica Neue';">Support for newtype feature/typesafe calculations</span></div><div class=""><span class="" style="font-family: 'Helvetica Neue';">- </span><font face="Helvetica Neue" class="">Type Safe Algorithms</font></div><div class=""><span class="" style="font-family: 'Helvetica Neue';"><br class=""></span></div><div class=""><font face="Helvetica Neue" class="">I also have the feeling all those discussions are moving toward a more advanced typing system, with things such as type hierarchy, and contracts.</font></div><div class=""><span class="" style="font-family: 'Helvetica Neue';">One such system I have worked with is implemented the Ada language (a language that also emphasise on making code secure).</span></div><div class=""><span class="" style="font-family: 'Helvetica Neue';">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.</span></div><div class=""><font face="Helvetica Neue" class="">Ada has plenty of possibilities that can be great thanks to that typing system. For exemple:</font></div><div class=""><font face="Helvetica Neue" class="">- there is a notion of compatibility between types and subtypes, which enable such things as declaring a “NumberOfMelons” type and a “NumberOfApples” </font><span class="" style="font-family: 'Helvetica Neue';">type</span><span class="" style="font-family: 'Helvetica Neue';">, and have the compiler warn you that you cannot add melons and apple when you try to do such operations.</span></div><div class=""><font face="Helvetica Neue" class="">- it makes it possible to declare mod types, with values that will cycle between two values</font></div><div class=""><font face="Helvetica Neue" class="">- 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 ?”</font></div><div class=""><font face="Helvetica Neue" class="">- ...</font></div><div class=""><span class="" style="font-family: 'Helvetica Neue';"><br class=""></span></div><div class=""><span class="" style="font-family: 'Helvetica Neue';">Type invariants and subtypes predicates were added in Ada 2012 (</span><font face="Helvetica Neue" class="">see </font><font color="#4787ff" class=""><u class=""><a href="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" class="">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</a></u></font><font face="Helvetica Neue" class="">).</font></div><div class=""><font face="Helvetica Neue" class="">There is an explanation of the Ada typing system here : <a href="https://en.wikibooks.org/wiki/Ada_Programming/Type_System" class="">https://en.wikibooks.org/wiki/Ada_Programming/Type_System</a></font></div><div class=""><font face="Helvetica Neue" class=""><br class=""></font></div><div class=""><font face="Helvetica Neue" class="">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.</font></div><div class=""><font face="Helvetica Neue" class="">That might address all three discussions (this one, and the two other ones, listed at the beginning of this message).</font></div><div class=""><font face="Helvetica Neue" class="">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 :-).</font></div></div><div class=""><font face="Helvetica Neue" class=""><br class=""></font></div><div class=""><font face="Helvetica Neue" class="">What do you think guys ?</font></div></div></div></blockquote><div class=""><br class=""></div><div class="">I don’t know Ada so I won’t comment on that part.</div><div class=""><br class=""></div><div class="">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.</div><br class=""><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><br class=""></div><div class="">Jerome</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><blockquote type="cite" class=""><div class="">On 05 Jan 2016, at 07:20, Árpád Goretity via swift-evolution <<a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">This suspiciously starts to resemble a mixture of dependent types and explicit contracts (something like the Midori variant of C#).<br class=""><br class="">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).<br class=""><br class="">Sent from my iPhone<br class=""><br class=""><blockquote type="cite" class="">On 04 Jan 2016, at 21:33, Howard Lovatt <<a href="mailto:howard.lovatt@gmail.com" class="">howard.lovatt@gmail.com</a>> wrote:<br class=""><br class="">Alternatively the Properties Behaviour syntax proposal could be applied to any declaration, assuming that it is accepted.<span class="Apple-converted-space"> </span><br class=""><br class=""><br class=""><blockquote type="cite" class="">On 5 Jan 2016, at 4:18 AM, Amir Michail via swift-evolution <<a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a>> wrote:<br class=""><br class="">Examples:<br class=""><br class="">invariant vectorIndex(v:Int) { return 0..<3 ~= v }<br class=""><br class="">var i:Int,vectorIndex: = 2<br class="">i = 3 // run-time error<br class=""><br class="">invariant positive(v:Int) { return v > 0 }<br class="">invariant odd(v:Int) { return v % 2 == 1 }<br class=""><br class="">var x:Int, positive, odd = 5<br class=""><br class="">x = 2 // run-time error<br class=""><br class="">func f(z:Int, positive, odd) {<br class="">…<br class="">}<br class=""><br class="">f(-3) // run-time error<br class=""><br class=""><br class=""><br class=""><br class=""><br class=""><br class="">_______________________________________________<br class="">swift-evolution mailing list<br class=""><a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a><br class=""><a href="https://lists.swift.org/mailman/listinfo/swift-evolution" class="">https://lists.swift.org/mailman/listinfo/swift-evolution</a><br class=""></blockquote><br class=""><br class=""></blockquote>_______________________________________________<br class="">swift-evolution mailing list<br class=""><a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a><br class=""><a href="https://lists.swift.org/mailman/listinfo/swift-evolution" class="">https://lists.swift.org/mailman/listinfo/swift-evolution</a><br class=""></div></div></blockquote></div><br class=""><img src="https://u2002410.ct.sendgrid.net/wf/open?upn=eLFMrKDT8iBxZ-2Fbnk-2BZqvSchNN-2FvYXdceA0T7VxwkAe3K-2Bn-2B3dG2Q7y5JkXpFMITwgZ9xPLCYl8V6-2F1Bodb2XIbo68pVWrf-2FesfqSHaqCMJZ5qD4sSFIYqG2xQgIitJbtLJEPybqD39voBz-2FnLuNsE-2BunYdh65cMvhpcV8qyeHK5czyig4-2FOCWFQL263pxLcmRzpePLSQK3KykvPxPRkU0eR-2FnLjjmSMfhqtlvcDZbI-3D" alt="" width="1" height="1" border="0" class="" style="height: 1px !important; width: 1px !important; border-width: 0px !important; margin: 0px !important; padding: 0px !important;"></div>_______________________________________________<br class="">swift-evolution mailing list<br class=""><a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a><br class=""><a href="https://lists.swift.org/mailman/listinfo/swift-evolution" class="">https://lists.swift.org/mailman/listinfo/swift-evolution</a><br class=""></div></blockquote></div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><img src="https://u2002410.ct.sendgrid.net/wf/open?upn=8K1sNvSH2KR-2BkHEodrUTpQZHB-2FpIKiIDctUruYn4gQQ71juXm7fO4Ws-2BxoNnPH5RWrZtH3Q6ZVr4JO6lBWa-2FpSk7rYKIpVGoo1WqLO0z9-2FMiC9YtmLozbgtt-2F0BHg2GrnHYr8D5SMkUvp3pKP1u0m-2FPlymFEmrk8rGsHIhbQSRpC5JMVaZJuufTlbHw9pw-2FiUsY4qSD4e4E-2FjxhcUbCj4UUIHU9K5SzmuXGy59g60gQ-3D" alt="" width="1" height="1" border="0" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; height: 1px !important; width: 1px !important; border-width: 0px !important; margin: 0px !important; padding: 0px !important;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class=""><span class="Apple-converted-space"> </span>_______________________________________________</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">swift-evolution mailing list</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="mailto:swift-evolution@swift.org" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">swift-evolution@swift.org</a><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="https://lists.swift.org/mailman/listinfo/swift-evolution" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">https://lists.swift.org/mailman/listinfo/swift-evolution</a></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""></body></html>