Scrivendo Un polimorfico Funzione in una famiglia tipo

Question

stavo sperimentando con le famiglie di tipo ieri e sono imbattuto in un ostacolo con il seguente codice:

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

Qui ho un tipo associato di classe C e una funzione che calcola la lunghezza del tipo associato. Tuttavia, il codice di cui sopra mi dà questo errore:

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

Se, tuttavia cambio "tipo" a "dati" il codice compila e funziona:

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

Perché la "lunghezza" non funzionare come previsto nel primo caso? Le righe "tipo A String ..." e "tipo A Int ..." specificano che il tipo "A a" è un elenco, quindi myLength dovrebbe avere rispettivamente i seguenti tipi: "myLength :: [String] -> Int" o "myLength :: [Int] -> Int".

Answer 1

Hm. Dimentichiamo i tipi per un momento.

Diciamo che hanno due funzioni:

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 esista un certo valore n :: Int che vi preoccupate. Dato solo il valore di a n, come si trova il valore di l n? Non lo sai, naturalmente.

Com'è pertinente? Bene, il tipo di myLength è A a -> Int, dove A a è il risultato dell'applicazione della "funzione tipo" A ad un tipo a. Tuttavia, myLength fa parte di una classe di tipi, il parametro di classe a viene utilizzato per selezionare l'implementazione di myLength da utilizzare. Quindi, dato un valore un certo tipo specifico B, applicando myLength ad esso dà un tipo di B -> Int, dove B ~ A a ed è necessario conoscere l'a al fine di cercare l'attuazione di myLength. Dato solo il valore di A a, come si trova il valore di a? Non lo sai, naturalmente.

Si potrebbe ragionevolmente obiettare che nel codice qui, la funzione Aè invertibile, a differenza della funzione di a nel mio precedente esempio. Questo è vero, ma il compilatore non può fare nulla con quello a causa del presupposto open world in cui sono coinvolte classi di tipi; il tuo modulo potrebbe, in teoria, essere importato da un altro modulo che definisce la sua istanza, ad esempio

instance C Bool where 
    type A Bool = [String] 

Sciocco? Sì. Codice valido? Anche sì

In molti casi, l'uso di costruttori in Haskell serve per creare funzioni banalmente iniettive: Il costruttore introduce una nuova entità che viene definito solo ed unicamente dagli argomenti è dato, rendendo più semplice per recuperare i valori originali. Questa è esattamente la differenza tra le due versioni del tuo codice; la famiglia di dati rende invertibile la funzione di tipo definendo un nuovo tipo distinto per ogni argomento.