<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 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=""><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 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 style="font-family: 'Helvetica Neue';" class="">Support for newtype feature/typesafe calculations</span></div><div class=""><span style="font-family: 'Helvetica Neue';" class="">- </span><font face="Helvetica Neue" class="">Type Safe Algorithms</font></div><div class=""><span style="font-family: 'Helvetica Neue';" class=""><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 style="font-family: 'Helvetica Neue';" class="">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 style="font-family: 'Helvetica Neue';" class="">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 style="font-family: 'Helvetica Neue';" class="">type</span><span style="font-family: 'Helvetica Neue';" class="">, 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 style="font-family: 'Helvetica Neue';" class=""><br class=""></span></div><div class=""><span style="font-family: 'Helvetica Neue';" class="">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><br class=""></div><div>I don’t know Ada so I won’t comment on that part.</div><div><br class=""></div><div>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 style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><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. <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" style="height:1px !important;width:1px !important;border-width:0 !important;margin-top:0 !important;margin-bottom:0 !important;margin-right:0 !important;margin-left:0 !important;padding-top:0 !important;padding-bottom:0 !important;padding-right:0 !important;padding-left:0 !important;" class="">
</div>
_______________________________________________<br class="">swift-evolution mailing list<br class=""><a href="mailto:swift-evolution@swift.org" class="">swift-evolution@swift.org</a><br class="">https://lists.swift.org/mailman/listinfo/swift-evolution<br class=""></div></blockquote></div><br class=""></body></html>