haskell - ¿Hay un lenguaje con tipos restringibles?

agda dependent-type

Question

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

1. Una probabilidad es un número de coma 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

2. Una Distribución de Probabilidad Discreta es un mapa, donde: las claves deben ser 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 yo entiendo, esto no es posible con Haskell o Agda.

Answer 1

El lenguaje de While admite algo muy parecido a lo que dices. Por ejemplo:

type natural is (int x) where x >= 0
type probability is (real x) where 0.0 <= x && x <= 1.0

Estos tipos también se pueden implementar como condiciones previas / posteriores de esta manera:

function abs(int x) => (int r)
ensures r >= 0:
    //
    if x >= 0:
        return x
    else:
        return -x

El lenguaje es muy expresivo. Estas invariantes y las condiciones previas / posteriores se verifican estáticamente utilizando un solucionador SMT. Esto maneja muy bien ejemplos como el anterior, pero actualmente tiene problemas con ejemplos más complejos que involucran matrices e invariantes de bucle.

Answer 2

Lo que quieres se llama tipos de refinamiento .

Es posible definir Probability en Agda: Prob.agda

El tipo de función de masa de probabilidad, con la condición de suma se define en la línea 264.

Hay idiomas con tipos de refinamiento más directos que en Agda, por ejemplo ATS

Answer 3

Modula 3 tiene tipos de subrango. (Subrangos de ordinales). Por lo tanto, para su Ejemplo 1, si está dispuesto a asignar la probabilidad a un rango entero de cierta precisión, podría usar esto:

TYPE PROBABILITY = [0..100]

Agregue dígitos significativos según sea necesario.

Ref .: Más sobre los ordinales de subrango here .

Answer 4

Nimrod es un nuevo lenguaje que admite este concepto. Se llaman Subrangos. Aquí hay un ejemplo. Puede obtener más información sobre el idioma aquí link

type
  TSubrange = range[0..5]

Answer 5

Para la primera parte, sí, ese sería Pascal, que tiene subintervalos enteros.

Answer 6

Perl6 tiene una noción de "subconjuntos de tipos" que puede agregar condiciones arbitrarias para crear un "subtipo".

Para su pregunta específicamente:

subset Probability of Real where 0 .. 1;

y

role DPD[::T] {
  has Map[T, Probability] $.map
    where [+](.values) == 1; # calls `.values` on Map
}

(nota: en las implementaciones actuales, la parte "where" está marcada en tiempo de ejecución, pero dado que "tipos reales" están marcados en tiempo de compilación (que incluye sus clases), y dado que hay anotaciones puras ( is pure ) dentro del std (que es principalmente perl6) (también están en operadores como * , etc.), es solo cuestión de esfuerzo ponerlo (y no debería ser mucho más).

Más generalmente:

# (%% is the "divisible by", which we can negate, becoming "!%%")
subset Even of Int where * %% 2; # * creates a closure around its expression
subset Odd of Int where -> $n { $n !%% 2 } # using a real "closure" ("pointy block")

Luego puede verificar si un número coincide con el operador Smart Matching ~~ :

say 4 ~~ Even; # True
say 4 ~~ Odd; # False
say 5 ~~ Odd; # True

Y, gracias a multi sub s (o multi-lo que sea, en realidad -múltiples métodos u otros), podemos despachar basado en eso:

multi say-parity(Odd $n) { say "Number $n is odd" }
multi say-parity(Even) { say "This number is even" } # we don''t name the argument, we just put its type
#Also, the last semicolon in a block is optional

Answer 7

Puedes hacerlo en Haskell con Liquid Haskell, que amplía Haskell con tipos de refinamiento . Los predicados son gestionados por un solucionador SMT en tiempo de compilación, lo que significa que las pruebas son totalmente automáticas, pero la lógica que puede usar está limitada por lo que maneja el solucionador SMT. (Afortunadamente, los solucionadores de SMT modernos son razonablemente versátiles).

Un problema es que no creo que Liquid Haskell soporte flotadores actualmente. Sin embargo, si no es así, debería ser posible rectificar porque existen teorías de números de coma flotante para solucionadores de SMT. También podría pretender que los números de punto flotante eran realmente racionales (¡o incluso usar Rational en Haskell!). Con esto en mente, su primer tipo podría verse así:

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

Su segundo tipo sería un poco más difícil de codificar, especialmente porque los mapas son un tipo abstracto del que es difícil razonar. Si utilizó una lista de pares en lugar de un mapa, podría escribir una "medida" como esta:

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

(Es posible que desee envolver [] en un newtype también).

Ahora puede usar total en un refinamiento para restringir una lista:

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

El truco perfecto con Liquid Haskell es que todo el razonamiento está automatizado para usted en tiempo de compilación, a cambio de usar una lógica algo limitada. (Medidas como el total también están muy restringidas en cómo se pueden escribir; es un pequeño subconjunto de Haskell con reglas como "exactamente un caso por constructor"). Esto significa que los tipos de refinamiento en este estilo son menos potentes pero mucho más fáciles de usar que tipos dependientes completos, haciéndolos más prácticos.