Escribiendo Un polimórfica función en una familia Tipo

Question

Estaba experimentando con las familias de tipo ayer y me encontré con un obstáculo con el siguiente código:

{-# LANGUAGE TypeFamilies #-} 

    class C a where 
     type A a 
     myLength :: A a -> Int 

    instance C String where 
     type A String = [String] 
     myLength = length 

    instance C Int where 
     type A Int = [Int] 
     myLength = length 

    main = let a1 = [1,2,3] 
      a2 = ["hello","world"] 
     in print (myLength a1) 
      >> print (myLength a2) 

Aquí he un tipo asociado con la clase C y una función que calcula la longitud del tipo asociado. Sin embargo el código anterior me da este error:

/tmp/type-families.hs:18:30: 
    Couldn't match type `A a1' with `[a]' 
    In the first argument of `myLength', namely `a1' 
    In the first argument of `print', namely `(myLength a1)' 
    In the first argument of `(>>)', namely `print (myLength a1)' 
/tmp/type-families.hs:19:30: 
    Couldn't match type `A a2' with `[[Char]]' 
    In the first argument of `myLength', namely `a2' 
    In the first argument of `print', namely `(myLength a2)' 
    In the second argument of `(>>)', namely `print (myLength a2)' 
Failed, modules loaded: none. 

Si, por el cambio "tipo" a "datos" del código se compila y funciona:

{-# LANGUAGE TypeFamilies #-} 

    class C a where 
     data A a 
     myLength :: A a -> Int 

    instance C String where 
     data A String = S [String] 
     myLength (S a) = length a 

    instance C Int where 
     data A Int = I [Int] 
     myLength (I a) = length a 

    main = let a1 = I [1,2,3] 
      a2 = S ["hello","world"] 
      in 
       print (myLength a1) >> 
       print (myLength a2) 

¿Por qué la "longitud" no funciona como se esperaba ¿en el primer caso? Las líneas "tipo A Cadena ..." y "tipo A Int ..." especifican que el tipo "A a" es una lista, por lo que myLength debe tener los siguientes tipos respectivamente: "myLength :: [String] -> Int" o "myLength :: [Int] -> Int".

Answer 1

Hm. Olvidémonos de los tipos por un momento.

Digamos que usted tiene dos funciones:

import qualified Data.IntMap as IM 

a :: Int -> Float 
a x = fromInteger (x * x)/2 

l :: Int -> String 
l x = fromMaybe "" $ IM.lookup x im 
    where im = IM.fromList -- etc... 

dicen existe algún valor n :: Int que le interesan. Dado solo el valor de a n, ¿cómo se encuentra el valor de l n? Usted no, por supuesto.

¿Qué es esto? Bueno, el tipo de myLength es A a -> Int, donde A a es el resultado de aplicar la "función de tipo" A a algún tipo a. Sin embargo, myLength formando parte de una clase de tipo, el parámetro de clase a se usa para seleccionar qué implementación de myLength usar. Por lo tanto, dado un valor de algún tipo específico B, aplicando myLength a que da un tipo de B -> Int, donde B ~ A a y lo que necesita saber la a con el fin de buscar la implementación de myLength. Dado solo el valor de A a, ¿cómo se encuentra el valor de a? Usted no, por supuesto.

Se podría objetar razonablemente que en su código aquí, la función A es invertible, a diferencia de la función a en mi ejemplo anterior. Esto es cierto, pero el compilador no puede hacer nada con eso debido a la suposición open world donde están involucradas las clases de tipo; el módulo podría, en teoría, ser importado por otro módulo que define su propia instancia, ej .:

instance C Bool where 
    type A Bool = [String] 

tonto? Sí. ¿Codigo valido? También sí

En muchos casos, el uso de constructores en Haskell sirve para crear funciones trivialmente inyectivos: El constructor introduce una nueva entidad que se define sólo y exclusivamente por los argumentos que se le da, por lo que es fácil de recuperar los valores originales. Esta es precisamente la diferencia entre las dos versiones de tu código; la familia de datos hace que la función de tipo sea invertible definiendo un nuevo tipo distinto para cada argumento.