[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