[swift-evolution] Code Contracts

Dennis Weissmann dennis at dennisweissmann.me
Fri Jan 15 06:27:28 CST 2016


> On Jan 15, 2016, at 6:53 AM, Dave via swift-evolution <swift-evolution at swift.org> wrote:
> 
> This is the same thing as Refinement Types, right?
> https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_types <https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_types>
> http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ <http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/>
> 

Yes, it seems they are. There is a pretty nice and easy to understand explanation [here](https://github.com/tomprimozic/type-systems/tree/master/refined_types):

Refined types or contracts are a restricted form of dependent types that combine base datatypes with logical predicates; for example, the type of natural numbers could be written x : int if x ≥ 0 (the notation most commonly used in academic literature is {ν : int | ν ≥ 0}).

> 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.

That was probably Matthew (https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005925.html) or me (https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20160104/005918.html) - the thread is called 'Proposal: named invariants for variable declarations'

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.

- Dennis

> - Dave Sweeris
> 
>> On Jan 14, 2016, at 20:32, Suminda Dharmasena via swift-evolution <swift-evolution at swift.org <mailto:swift-evolution at swift.org>> wrote:
>> 
>> E.g. 
>> 
>> var @where("myVariable <= 100 && myVariable >= 0") myVariable = 42
>> 
>> 
>> @where("myVariable <= 80 && myVariable >= 50")
>> {
>>     ...
>> }
>> 
>> 
>> @where("score <= 100 && score >= 0")
>> for score in individualScores {
>>     ...
>> }
>>  _______________________________________________
>> 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/20160115/d4f11ca1/attachment.html>


More information about the swift-evolution mailing list