Is there a language with constrainable types?

Question

Is there a typed programming language where I can constrain types like the following two examples?

1. A Probability is a floating point number with minimum value 0.0 and maximum value 1.0.

   type Probability subtype of float
   where
       max_value = 0.0
       min_value = 1.0
   

2. A Discrete Probability Distribution is a map, where: the keys should all be the same type, the values are all Probabilities, and the sum of the values = 1.0.

   type DPD<K> subtype of map<K, Probability>
   where
       sum(values) = 1.0
   

As far as I understand, this is not possible with Haskell or Agda.

Answer 1

What you want is called refinement types.

It's possible to define Probability in Agda: Prob.agda

The probability mass function type, with sum condition is defined at line 264.

There are languages with more direct refinement types than in Agda, for example ATS

Answer 2

You can do this in Haskell with Liquid Haskell which extends Haskell with refinement types. The predicates are managed by an SMT solver at compile time which means that the proofs are fully automatic but the logic you can use is limited by what the SMT solver handles. (Happily, modern SMT solvers are reasonably versatile!)

One problem is that I don't think Liquid Haskell currently supports floats. If it doesn't though, it should be possible to rectify because there are theories of floating point numbers for SMT solvers. You could also pretend floating point numbers were actually rational (or even use Rational in Haskell!). With this in mind, your first type could look like this:

{p : Float | p >= 0 && p <= 1}

Your second type would be a bit harder to encode, especially because maps are an abstract type that's hard to reason about. If you used a list of pairs instead of a map, you could write a "measure" like this:

measure total :: [(a, Float)] -> Float
total []          = 0 
total ((_, p):ps) = p + probDist ps

(You might want to wrap [] in a newtype too.)

Now you can use total in a refinement to constrain a list:

{dist: [(a, Float)] | total dist == 1}

The neat trick with Liquid Haskell is that all the reasoning is automated for you at compile time, in return for using a somewhat constrained logic. (Measures like total are also very constrained in how they can be written—it's a small subset of Haskell with rules like "exactly one case per constructor".) This means that refinement types in this style are less powerful but much easier to use than full-on dependent types, making them more practical.