¿Existe un lenguaje de programación mecanografiado donde pueda restringir tipos como los dos ejemplos siguientes?

Una probabilidad es un número de punto flotante con un valor mínimo de 0.0 y un valor máximo de 1.0.

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

Una distribución de probabilidad discreta es un mapa, donde: las claves deben ser todas del mismo tipo, los valores son todas las probabilidades y la suma de los valores = 1.0.

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

Por lo que entiendo, esto no es posible con Haskell o Agda.