Haskell Language
Семейство типов

Типовые синонимы

Семейство синонимов типов - это только функции на уровне шрифта: они связывают типы параметров с типами результатов. Они представлены в трех разных вариантах.

Закрытые семейства синонимов

Они работают так же, как обычные функции Haskell на уровне значений: вы указываете некоторые предложения, сопоставляя некоторые типы с другими:

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

Открытые семейства синонимов типа

Они больше похожи на экземпляры typeclass: каждый может добавлять дополнительные предложения в другие модули.

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.

Синонимы, связанные с классом

Семейство открытого типа также можно комбинировать с фактическим классом. Обычно это делается, когда, как и в случае связанных семейств данных , некоторый метод класса нуждается в дополнительных вспомогательных объектах, и эти вспомогательные объекты могут быть разными для разных экземпляров, но могут также совместно использоваться. Хорошим примером является класс 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

Обратите внимание, что в первых двух случаях реализация Scalar одинакова. Это было бы невозможно с ассоциированным семейством данных: семейства данных инъективны , семейства синонимов типа нет.

Хотя неинъективность открывает некоторые возможности, подобные описанным выше, это также затрудняет определение типа. Например, следующее правило не будет выглядеть:

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)

В этом случае компилятор не может знать, какой экземпляр использовать, потому что аргумент bar является собственно полиморфным литералом Num . И Bar функции типа не может быть разрешен в «обратном направлении», именно потому, что он не является инъективным ^† и, следовательно, не обратим (может быть более одного типа с Bar a = String ).

^† _{Только с этими двумя экземплярами он фактически является инъективным, но компилятор не может знать, что кто-то не добавит больше экземпляров позже и тем самым нарушит поведение.}

Типы данных

Семейства данных могут использоваться для создания типов данных, которые имеют разные реализации на основе их аргументов типа.

Автономные семейства данных

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

В приведенной выше декларации Nil :: List Char и UnitList :: Int -> List ()

Связанные семейства данных

Семейства данных также могут быть связаны с классами. Это часто полезно для типов с «вспомогательными объектами», которые требуются для универсальных методов класса, но должны содержать различную информацию в зависимости от конкретного экземпляра. Например, для индексирования местоположений в списке требуется только одно число, тогда как в дереве вам нужно число, указывающее путь на каждом узле:

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

приемистости

Тип Семьи не обязательно инъективны. Поэтому мы не можем вывести параметр из приложения. Например, в servant , заданном Server a типа Server a мы не можем вывести тип a . Чтобы решить эту проблему, мы можем использовать Proxy . Например, в servant функция serve имеет тип ... Proxy a -> Server a -> ... Мы можем сделать вывод , из a Proxy a потому , что Proxy определяются data , которые инъективны.