escribe declaraciones en 'donde' - ¿qué está pasando?

Question

Mientras lee el QuickCheck Manual, me encontré con el siguiente ejemplo:

prop_RevRev xs = reverse (reverse xs) == xs 
    where types = xs::[Int] 

El manual pasa a decir:

propiedades deben tener tipos monomorfas. Las propiedades `Polimórficas ', como la de arriba, deben estar restringidas a un tipo particular que se utilizará para las pruebas. Es conveniente hacerlo indicando los tipos de uno o más argumentos en un

donde tipos = (x1 :: t1, t2 :: x2, ...) Cláusula

. Tenga en cuenta que los tipos no son palabras clave; esto es solo una declaración local que proporciona un lugar conveniente para restringir los tipos de x1, x2, etc.

Nunca antes había visto un truco semejante en Haskell. Esto es lo que realmente tengo problemas con:

1. ¿Por qué existe esta sintaxis para las declaraciones de tipo? ¿Qué puede hacer por mí que el siguiente no podría?

   prop_RevRev :: [Int] -> Bool 
   prop_RevRev xs = reverse (reverse xs) == xs 
   

2. ¿Este uso de where constituyen la sintaxis 'especial' para las declaraciones de tipo? ¿O es consistente y lógico (y si es así, cómo?)?

3. ¿Es este uso Haskell estándar o convencional?

Answer 1

where no es una sintaxis especial para las declaraciones de tipo. Por ejemplo, esto funciona:

prop_RevRev :: [Int] -> Bool 
prop_RevRev xs = ys == xs 
    where ys = reverse (reverse xs) 

y lo mismo ocurre esto:

prop_RevRev xs = ys == xs 
    where ys = reverse (reverse xs) 
     ys :: [Int] 

La ventaja de where type = (xs :: [Int]) sobre prop_RevRev :: [Int] -> Bool es que en este último caso se tiene que especificar el tipo de retorno, mientras que en el primer caso el compilador puede inferirlo por ti. Esto importaría si tuviera un no Boolean propiedad, por ejemplo:

prop_positiveSum xs = 0 < length xs && all (0 <) xs ==> 0 < sum xs 
    where types = (xs :: [Int]) 

Answer 2

No es ninguna sintaxis especial, y en algún momento se acaba lo necesitan, como en el caso siguiente:

foo :: String -> String 
foo s = show (read s) 

Como está parado, esto no se puede escribir porque no se puede identificar el tipo del valor read s. Todo lo que se sabe es que debe ser una instancia de Show y de Read. Pero este tipo no aparece en la firma de tipo, por lo que tampoco es posible dejarlo así e inferir un tipo restringido. (Simplemente no hay una variable de tipo que pueda estar restringida).)

Es interesante notar que lo hace read s depende enteramente de la firma de tipo se da a read s, por ejemplo:

read "Just True" :: (Maybe Bool) 

tendrán éxito, mientras que

read "Just True" :: (Maybe Int) 

no lo hará.