<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=""><div><blockquote type="cite" class=""><div class="">On Jan 15, 2016, at 6:53 AM, Dave 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=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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="">This is the same thing as Refinement Types, right?</span><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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;"><a href="https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_types" class="">https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_types</a></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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;"><a href="http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/" class="">http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/</a></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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;"><br class=""></div></div></blockquote><div><br class=""></div><div><div>Yes, it seems they are. There is a pretty nice and easy to understand explanation [here](<a href="https://github.com/tomprimozic/type-systems/tree/master/refined_types" class="">https://github.com/tomprimozic/type-systems/tree/master/refined_types</a>):</div><div><br class=""></div><div><div class=""><em style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 16px;" class="">Refined types</em><span style="color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 16px; background-color: rgb(255, 255, 255);" class=""> or </span><em style="box-sizing: border-box; color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 16px;" class="">contracts</em><span style="color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 16px; background-color: rgb(255, 255, 255);" class=""> are a restricted form of dependent types that combine base datatypes with logical predicates; for example, the type of natural numbers could be written </span><code style="box-sizing: border-box; font-family: Consolas, 'Liberation Mono', Menlo, Courier, monospace; font-size: 14px; padding: 0.2em 0px; margin: 0px; background-color: rgba(0, 0, 0, 0.0392157); border-top-left-radius: 3px; border-top-right-radius: 3px; border-bottom-right-radius: 3px; border-bottom-left-radius: 3px; color: rgb(51, 51, 51);" class="">x : int if x ≥ 0</code><span style="color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 16px; background-color: rgb(255, 255, 255);" class=""> (the notation most commonly used in academic literature is </span><code style="box-sizing: border-box; font-family: Consolas, 'Liberation Mono', Menlo, Courier, monospace; font-size: 14px; padding: 0.2em 0px; margin: 0px; background-color: rgba(0, 0, 0, 0.0392157); border-top-left-radius: 3px; border-top-right-radius: 3px; border-bottom-right-radius: 3px; border-bottom-left-radius: 3px; color: rgb(51, 51, 51);" class="">{ν : int | ν ≥ 0}</code><span style="color: rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol'; font-size: 16px; background-color: rgb(255, 255, 255);" class="">).</span></div></div></div><br class=""><blockquote type="cite" class=""><div class=""><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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;">I’m in favor of it, but I think someone’s already made that suggestion… At the very least, I didn’t know what the phrase meant until a few days ago, and I know I learned about it from reading something on swift-evolution.</div></div></blockquote><div><br class=""></div><div>That was probably Matthew (<a href="https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005925.html" class="">https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005925.html</a>) or me (<a href="https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005918.html" class="">https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005918.html</a>) - the thread is called '<span style="font-family: 'Helvetica Neue';" class="">Proposal: named invariants for variable declarations'</span></div><div><br class=""></div><div>And I agree with Matthew that this won’t happen anytime soon. That’s why I didn’t want to discuss that topic too much. It’s just that the ABI will be finalized later this year and I wanted to mention that there is definitely interest in this area in case some ABI-related things are needed for refinement types (or even dependent types, someday, one can dream 😇) which need to be thought of before the finalization.</div><div><br class=""></div>- Dennis</div><div><br class=""><blockquote type="cite" class=""><div class=""><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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;"><div class="">- Dave Sweeris</div><br class=""><div class=""><blockquote type="cite" class=""><div class="">On Jan 14, 2016, at 20:32, Suminda Dharmasena 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 dir="ltr" class=""><div class="gmail_extra">E.g. </div><div class="gmail_extra"><br class=""></div><div class="gmail_extra"><ol class="" style="border: 0px; font-size: 14px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; line-height: 1.6em; list-style: none; font-family: Helvetica, Arial, sans-serif;"><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent; background-position: initial initial; background-repeat: initial initial;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-position: initial initial; background-repeat: initial initial;"><span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(170, 51, 145); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">var @where("<span class="" style="font-size: 11.9px; line-height: 22.4px; border: 0px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">myVariable</span><span class="" style="font-size: 11.9px; line-height: 22.4px;"> </span><= 100 && <span class="" style="font-size: 11.9px; line-height: 22.4px; border: 0px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">myVariable</span> >= 0")</span> <span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">myVariable</span> = <span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(28, 0, 207); background-color: transparent; background-repeat: initial initial;">42</span></code></li></ol><div class="" style="text-indent: -13px;"><br class=""></div><div class="" style="text-indent: -13px;"><div class=""><font color="#aa3391" face="Menlo, monospace" class=""><span class="" style="font-size: 11.9px; line-height: 22.4px; white-space: pre-wrap;"><br class=""></span></font></div><div class=""><ol class="" style="border: 0px; font-size: 14px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; line-height: 1.6em; list-style: none; font-family: Helvetica, Arial, sans-serif; text-indent: 0px; background-repeat: initial initial;"><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-position: initial initial; background-repeat: initial initial;"><span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(170, 51, 145); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">@where("<span class="" style="font-size: 11.9px; line-height: 22.4px; border: 0px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">myVariable</span><span class="" style="font-size: 11.9px; line-height: 22.4px;"> </span><= 80 && <span class="" style="font-size: 11.9px; line-height: 22.4px; border: 0px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">myVariable</span><span class="" style="font-size: 11.9px; line-height: 22.4px;"> </span><span class="" style="font-size: 11.9px; line-height: 22.4px;">>= 50</span>")</span></code></li><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-position: initial initial; background-repeat: initial initial;">{</code></li><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent; background-repeat: initial initial;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-repeat: initial initial;"><font class=""> </font><font color="#aa3391" class="">...</font></code></li><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-position: initial initial; background-repeat: initial initial;">}</code></li></ol></div><div class=""><font color="#aa3391" face="Menlo, monospace" class=""><span class="" style="font-size: 11.9px; line-height: 22.4px; white-space: pre-wrap;"><br class=""></span></font></div><div class=""><font color="#aa3391" face="Menlo, monospace" class=""><span class="" style="font-size: 11.9px; line-height: 22.4px; white-space: pre-wrap;"><br class=""></span></font></div><ol class="" style="border: 0px; font-size: 14px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; line-height: 1.6em; list-style: none; font-family: Helvetica, Arial, sans-serif; text-indent: 0px;"><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-position: initial initial; background-repeat: initial initial;"><span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(170, 51, 145); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">@where("score <= 100 && <span class="" style="font-size: 11.9px; line-height: 22.4px;">score >= 0</span>")</span></code></li><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-position: initial initial; background-repeat: initial initial;"><span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(170, 51, 145); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">for</span> <span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">score</span> <span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(170, 51, 145); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">in</span> <span class="" style="border: 0px; font-size: 11.9px; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; color: rgb(63, 110, 116); background-color: transparent; background-position: initial initial; background-repeat: initial initial;">individualScores</span> {</code></li><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent; background-repeat: initial initial;"><font class=""> </font><font color="#aa3391" class="">...</font></code></li><li class="" style="border-width: 0px 0px 0px 18px; border-left-style: solid; border-left-color: transparent; margin: 0px; outline: 0px; padding: 0px 10px 0px 0px; vertical-align: baseline; white-space: pre-wrap; list-style-type: none; background-color: transparent;"><code class="" style="border: 0px; font-size: 0.85em; margin: 0px; outline: 0px; padding: 0px; vertical-align: baseline; font-family: Menlo, monospace; word-wrap: break-word; background-color: transparent;">}</code></li></ol></div></div></div><img src="https://u2002410.ct.sendgrid.net/wf/open?upn=mnFI6pg-2FTCMHnIXafbniMQOkvAOxgYUwbalcxNWA5RdDGNV8iM2feO0rvLraT0CXvJhPMa-2FKtBLAehYslsrqIzTyY7UO6tpTiuZmCIKk-2BDsj4z9Ne7s6Si-2B8z8IEoadwjfRNWqDAnEq9tjLL3PuiKKRVlXyEb5MUhxq3gRP-2FBBtGwkGlVsi1HLdCHWiv3PtRXoj3ljvlTENcdyRyZiHiNE-2B1yrc73VAuDnNDRXB1Zy8-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;"><span class="Apple-converted-space"> </span>_______________________________________________<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=""></div><img src="https://u2002410.ct.sendgrid.net/wf/open?upn=8CZIdLciSFC-2BO5jF-2FiP8qI4HoRkMSGQZzNYm-2FNO1boKFmxqU0G3w878abGTSELn-2Fb7BuHHDik1FCnuD-2Fx-2B5GVkH2yGEufvJZh9ynZJ82k6wjqceBKjLQfW2FYivn2nfbUEb53xm-2FdK-2FSWqb5-2FZTkC-2BBKDZsjBfyUaoqmtnfKZVvm-2FZzKq-2FGfuUIVcHpnCBlJJ3Y0bLTmqCpBaGulYpqaDo-2FdyfPmvQ-2BhhsnhYkkEWJk-3D" alt="" width="1" height="1" border="0" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: 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-caps: 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-caps: 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-caps: 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-caps: 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-caps: 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-caps: 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-caps: 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=""></body></html>