L'écriture d'un polymorphes de fonction dans un type de famille

Question

J'expérimentais avec les familles de type hier et a couru dans un obstacle avec le code suivant:

{-# 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) 

Ici, je suis un type associé à la classe C et une fonction qui calcule la longueur du type associé. Cependant, le code ci-dessus me donne cette erreur:

/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, mais je change « type » à « données » le code compile et fonctionne:

{-# 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) 

Pourquoi ne « longueur » fonctionne pas comme prévu dans le premier cas? Les lignes "type A String ..." et "type A Int ..." spécifient que le type "A a" est une liste donc myLength doit avoir respectivement les types suivants: "myLength :: [String] -> Int" ou "myLength :: [Int] -> Int".

Answer 1

Hm. Oublions les types pour un moment.

Disons que vous avez deux fonctions:

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... 

dire qu'il existe une valeur n :: Int que vous aimez. Étant donné seulement la valeur de a n, comment trouvez-vous la valeur de l n? Vous ne le faites pas, bien sûr.

En quoi cela est-il pertinent? Eh bien, le type de myLength est A a -> Int, où A a est le résultat de l'application de la "fonction de type" A à un certain type a. Cependant, myLength faisant partie d'une classe de type, le paramètre de classe a est utilisé pour sélectionner l'implémentation de myLength à utiliser. Donc, étant donné une valeur de un certain type spécifique B, l'application myLength lui donne un type de B -> Int, où B ~ A a et vous avez besoin de connaître le a afin d'examiner la mise en œuvre de myLength. Étant donné seulement la valeur de A a, comment trouvez-vous la valeur de a? Vous ne le faites pas, bien sûr.

Vous pouvez raisonnablement objecter que dans votre code ici, la fonction est A inversible, contrairement à la fonction a dans mon exemple précédent. C'est vrai, mais le compilateur ne peut rien faire avec ça à cause de l'hypothèse open world où les classes de types sont impliquées; votre module pourrait, en théorie, être importé par un autre module qui définit sa propre instance, par exemple .:

instance C Bool where 
    type A Bool = [String] 

idiot? Oui. Code valide? Aussi oui.

Dans de nombreux cas, l'utilisation des constructeurs dans Haskell sert à créer trivialement fonctions injectives: Le constructeur introduit une nouvelle entité qui est définie seulement et uniquement par les arguments qu'il a donnés, ce qui rend simple de récupérer les valeurs d'origine. C'est précisément la différence entre les deux versions de votre code; la famille de données rend la fonction de type inversible en définissant un nouveau type distinct pour chaque argument.