1. 30

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

      The flaw in your facetious statement is the definite article, the. The type can be a implementation: a slow (or otherwise inefficient), but ascertained-to-be-correct implementation, while “the implementation” is a fast, less-likely-to-be-precise one.

      I don’t see this as connected to relational and constraint programming. These are ideas I use on a regular basis; there are other times when I use relations and constraints; and when I’m doing one I’m rarely (by choice) doing the other.

      Though Racket comes with Datalog built-in, if that’s really your thing. (-:

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