Usar los tipos de Haskell para reemplazar afirmaciones o verificaciones en otros idiomas

Question

Disculpe si la pregunta es muy elemental, todavía soy muy nuevo en Haskell. Digamos que tengo una función que solo puede funcionar con dos números que están en la ración dorada (1.618), ¿cómo puedo definir los tipos de myfunx y para tomar solo los números de proporción áurea? ¿Qué sucede si invoco myfun sin números de relación de oro desde mi programa (un error de compilación?)? ¿Qué sucede si la llamada sin números de relación de oro se realiza en tiempo de ejecución a través de la entrada del usuario?

Answer 1

Puede que desee un ADT que solo se puede construir con números de proporción áurea y luego escriba myfun para aceptar ese tipo de datos.

He asumido Entero como tipo base, pero puede usar otros (por ejemplo: Doble o Flotante) o incluso ser polimórfico.

1) Hacer el ADT

module Golden (Gold, getGold, buildGold) where 

data Gold = G Integer Integer 

getGold :: Gold -> (Integer, Integer) 
getGold (G x y) = (x, y) 

buildGold :: Integer -> Integer -> Maybe Gold 
buildGold x y 
    | isGolden x y = Just (G x y) 
    | otherwise = Nothing 

Aviso este módulo exporta el tipo Gold pero no el constructor (es decir, no G). Por lo tanto, la única forma de obtener un valor de tipo Gold es con buildGold que realiza una comprobación en tiempo de ejecución, pero solo una, de modo que los valores de Gold pueden ser utilizados y asumidos como una proporción áurea por todos los consumidores sin verificar.

2) utilizar el ADT para construir myfun

myfun :: Gold -> ??? 
myfun g = expr 
    where (x, y) = getGold g 

Ahora bien, si se intenta llamar myfun con un número no de oro (un valor no de tipo Gold) por lo que recibirá un error de tiempo de compilación.

Recap Para construir los números dorados buildGold debe utilizarse la función, lo que obliga a comprobar el número.

¡Observe qué se comprueba cuando! Usted tiene una garantía de tiempo de compilación que myfun, y todas las demás funciones que desea utilizar con Gold, siempre se proporcionan proporciones de oro. La entrada del programa (desde el usuario, la red o donde sea) aún necesita verificaciones en tiempo de ejecución y eso es lo que buildGold proporciona; obviamente nunca habrá un programa que prometa que el humano no escribirá algo indeseable.

Las alternativas dadas en los comentarios a su pregunta también son dignas de consideración.Un ADT es un poco pesado si todo lo que necesita es una sola función, myfun, que puede fallar, solo tiene myfun :: (Integer, Integer) -> Maybe ???.

Answer 2

Lo mejor que puede hacer prácticamente es un control en tiempo de ejecución. Podría haber algún cálculo de nivel de tipo que no sé (ver el comentario de luqui), pero eso no es práctico en Haskell.

Usted podría utilizar an assert, que es lo que desea reemplazar,

checker :: a -> b -> Bool 
checker x y = x * 1.618 `approxEqual` y 

unsafeMyfun :: a -> b -> c 
unsafeMyfun x y = assert (checker x y) (doRealThingWith a b) 

o devolver un Maybe a (o Either err a) para evitar excepciones que no se pueden capturar en funciones puras,

myfun :: a -> b -> Maybe c 
myfun x y = do 
       guard $ checker x y 
       return $ doRealThingWith x y 

o utilice un tipo de contrato personalizado como en la respuesta de Tom, etc. En cualquier caso, no es posible verificar la restricción en tiempo de compilación. De hecho, debido a la mónada IO, cualquier restricción en tiempo de compilación no puede ser precisa.

Answer 3

La técnica más fácil es usar smart constructors, que usa una función de Int a GoldenInt, que verifica que sus valores estén en las proporciones requeridas.

Con más esfuerzo, puede usar type level numbers para asegurarse de que no es necesario verificar el tiempo de ejecución, sin embargo, dado que es un principiante, me apegaré al método del constructor inteligente.

La respuesta de Tom anterior es un ejemplo de este modismo.