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