title: Is there a language with constrainable types?
body: <p>Is there a typed programming language where I can constrain types like the following two examples?</p>
  
  <ol>
  <li><p>A Probability is a floating point number with minimum value 0.0 and maximum value 1.0.</p>
  
  <pre><code>type Probability subtype of float
  where
      max_value = 0.0
      min_value = 1.0
  </code></pre></li>
  <li><p>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.</p>
  
  <pre><code>type DPD&lt;K&gt; subtype of map&lt;K, Probability&gt;
  where
      sum(values) = 1.0
  </code></pre></li>
  </ol>
  
  <p>As far as I understand, this is not possible with Haskell or Agda.</p>