[swift-evolution] Code Contracts

[T.J. Usiyan]

>From what I understand of the goals of Swift, I think that any addition to
runtime machinery will be hard won. The Swift runtime is deliberately
small. I completely support refinement types and their logical conclusion
of dependent types but I don't think that the approach of "runtime checking
until capable of compile time checking" will gain much traction. I suggest
that we work primarily on creating a syntax so that, by the time that we
can implement it in the compiler, we have a truly compelling case.
TJ

On Sat, Jan 16, 2016 at 6:04 PM, Matt Whiteside via swift-evolution <
swift-evolution at swift.org> wrote:

>
> On Jan 15, 2016, at 8:53 AM, Dennis Weissmann via swift-evolution <
> swift-evolution at swift.org> wrote:
>
>
> On Jan 15, 2016, at 1:56 PM, Haravikk <swift-evolution at haravikk.com>
> wrote:
>
> This is pretty interesting; while the actual compile-time type-checking
> could be complex and take some time to implement, it seems to me that the
> actual notation could be implemented in advance and simply perform runtime
> assertions until the real type-checking is ready? In cases where the
> type-checker can’t be certain of a value’s safety, a run-time assertion
> might make sense anyway, so this short-term behaviour could actually be
> left in, with the caveat being that your restriction could still fail at
> run-time (which is what I think most people would want when the
> compile-time check isn’t enough).
>
>
> That’s an interesting approach! I like it :)
>
>
> I agree this approach is interesting, and I’ve had similar thoughts.
>
> Regarding your syntax idea,
>
>     typealias RGBAInt = Int where Type >= 0 && Type <= 255
>              // Can be rewritten as a range (0...255)
>     typealias RGBADouble = Double where Type >= 0 && Type <= 1.0
>             // Can be rewritten as a range (0...1.0)
>     typealias BatteryLevel = Int where Type >= 0 && Type <= 100
>             // Can be rewritten as a range (0...100)
>     typealias Primes10 = Int where Type == 2 || Type == 3 || Type == 5 ||
> Type == 7   // Cannot be rewritten as a range
>     typealias EvenNumber = Int where Type % 2 == 0
>             // Cannot be rewritten as a range
>
> What do you think?
>
> - Dennis
>
>
> I was discussing something like this on another thread, about compile time
> execution, and this is close to the syntax that I imagined.  The only thing
> I might suggest is that `typealias` doesn't seem like the ideal keyword
> here, since that is meant to indicate that the 2 types are one and the
> same.  These are some options that I thought might be good:
>
> struct InvertibleMatrix: SquareMatrix where determinant() != 0
>
> typedef InvertibleMatrix = SquareMatrix where determinant() != 0
>
> typerefinement InvertibleMatrix = SquareMatrix where determinant() != 0
>
> Matt
>
>
>
>
>
> _______________________________________________
> swift-evolution mailing list
> swift-evolution at swift.org
> https://lists.swift.org/mailman/listinfo/swift-evolution
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20160116/8d341149/attachment.html>