1. 29

From the blog post:

Typed Racket supports refinement types and dependent function types. Previously an experimental feature, refinement types allow types to describe more interesting properties of values, especially integers. For example, this type shows that the max function always produces a number at least as big as its inputs: (-> [x : Integer] [y : Integer] (Refine [z : Integer] (and (>= z x) (>= z y))))

  1.  

  2. 7

    At what point does the type become rich enough that it might as well just be the implementation?

    Or to be less facetious: When do we start seeing mainstream languages with integrated relational and constraint programming?

    1. 3

      Are these like pre- and post-conditions in Clojure, or can they be enforced before runtime in a language like Racket?

      1. 2

        They’re compile-time. I’m not sure if the documentation is up to date with this release, but you can check https://docs.racket-lang.org/ts-reference/Experimental_Features.html#%28part._.Refinements_and_.Linear_.Integer_.Reasoning%29.

        1. 2

          Racket’s runtime contract system does integrate nicely with Typed Racket, but I don’t think that’s what these more recent changes are about.