Haskell Language
Tipo Familias

Tipo de familias de sinónimos

Las familias de sinónimos de tipo son solo funciones de nivel de tipo: asocian tipos de parámetros con tipos de resultados. Estos vienen en tres variedades diferentes.

Familias de sinónimos de tipo cerrado

Estos funcionan de manera muy similar a las funciones Haskell de nivel de valor ordinarias: usted especifica algunas cláusulas, asignando ciertos tipos a otros:

{-# LANGUAGE TypeFamilies #-}
type family Vanquisher a where
    Vanquisher Rock = Paper
    Vanquisher Paper = Scissors
    Vanquisher Scissors = Rock

data Rock=Rock; data Paper=Paper; data Scissors=Scissors

Abrir familias de sinónimos de tipo

Estos funcionan más como instancias de typeclass: cualquiera puede agregar más cláusulas en otros módulos.

type family DoubledSize w

type instance DoubledSize Word16 = Word32
type instance DoubledSize Word32 = Word64
-- Other instances might appear in other modules, but two instances cannot overlap
-- in a way that would produce different results.

Sinónimos asociados a clases

Una familia de tipo abierto también se puede combinar con una clase real. Esto generalmente se hace cuando, al igual que con las familias de datos asociadas , algún método de clase necesita objetos auxiliares adicionales, y estos objetos auxiliares pueden ser diferentes para diferentes instancias, pero posiblemente también se pueden compartir. Un buen ejemplo es la clase VectorSpace :

class VectorSpace v where
  type Scalar v :: *
  (*^) :: Scalar v -> v -> v

instance VectorSpace Double where
  type Scalar Double = Double
  μ *^ n = μ * n

instance VectorSpace (Double,Double) where
  type Scalar (Double,Double) = Double
  μ *^ (n,m) = (μ*n, μ*m)
  
instance VectorSpace (Complex Double) where
  type Scalar (Complex Double) = Complex Double
  μ *^ n = μ*n

Observe cómo en las dos primeras instancias, la implementación de Scalar es la misma. Esto no sería posible con una familia de datos asociada: las familias de datos son inyectivas , pero las familias sinónimo de tipo no lo son.

Si bien la no inyectividad abre algunas posibilidades como la anterior, también dificulta la inferencia de tipos. Por ejemplo, lo siguiente no verificará:

class Foo a where
  type Bar a :: *
  bar :: a -> Bar a
instance Foo Int where
  type Bar Int = String
  bar = show
instance Foo Double where
  type Bar Double = Bool
  bar = (>0)

main = putStrLn (bar 1)

En este caso, el compilador no puede saber qué instancia usar, porque el argumento de la bar es en sí mismo un literal Num polimórfico. Y la función de Bar tipo no se puede resolver en "dirección inversa", precisamente porque no es inyectiva ^† y, por lo tanto, no es invertible (podría haber más de un tipo con Bar a = String ).

^† _{Con solo estas dos instancias, en realidad es inyectivo, pero el compilador no puede saber que alguien no agregará más instancias más adelante y, por lo tanto, romperá el comportamiento.}

Familias de tipos de datos

Las familias de datos se pueden usar para construir tipos de datos que tienen diferentes implementaciones basadas en sus argumentos de tipo.

Familias de datos independientes

{-# LANGUAGE TypeFamilies #-}
data family List a
data instance List Char = Nil | Cons Char (List Char)
data instance List () = UnitList Int

En la declaración anterior, Nil :: List Char y UnitList :: Int -> List ()

Familias de datos asociados

Las familias de datos también pueden asociarse con typeclasses. Esto suele ser útil para los tipos con "objetos auxiliares", que son necesarios para los métodos de clase de tipos genéricos, pero deben contener información diferente según la instancia concreta. Por ejemplo, las ubicaciones de indexación en una lista solo requieren un solo número, mientras que en un árbol necesita un número para indicar la ruta en cada nodo:

class Container f where
  data Location f
  get :: Location f -> f a -> Maybe a

instance Container [] where
  data Location [] = ListLoc Int
  get (ListLoc i) xs
    | i < length xs  = Just $ xs!!i
    | otherwise      = Nothing

instance Container Tree where
  data Location Tree = ThisNode | NodePath Int (Location Tree)
  get ThisNode (Node x _) = Just x
  get (NodePath i path) (Node _ sfo) = get path =<< get i sfo

La inyectividad

Tipo Las familias no son necesariamente inyectivas. Por lo tanto, no podemos inferir el parámetro de una aplicación. Por ejemplo, en servant , dado un Server a tipo Server a no podemos inferir el tipo a . Para resolver este problema, podemos utilizar Proxy . Por ejemplo, en el servant , la función de serve tiene tipo ... Proxy a -> Server a -> ... Podemos inferir a de Proxy a porque Proxy está definido por data que son inyectivos.