"Семейство типов" с "семейством данных", вкратце?
Я смущен тем, как выбирать между data family
и type family
. Страница wiki на TypeFamilies подробно освещена. Иногда он неофициально ссылается на Haskell data family
как на "семейство типов" в прозе, но, конечно, в Haskell также есть type family
.
Существует простой пример, показывающий, где показаны две версии кода, отличающиеся только тем, объявляется ли data family
или type family
:
-- BAD: f is too ambiguous, due to non-injectivity
-- type family F a
-- OK
data family F a
f :: F a -> F a
f = undefined
g :: F Int -> F Int
g x = f x
type
и data
здесь имеют одинаковое значение, но версия type family
не может проверять тип, а версия data family
в порядке, потому что data family
"создает новые типы и поэтому является инъективной" (говорит на странице wiki).
Мой взнос от всего этого - "попробуйте data family
для простых случаев, и, если он недостаточно мощный, попробуйте type family
". Это хорошо, но я хотел бы лучше понять это. Есть ли диаграмма Венна или дерево решений, которое я могу отслеживать, чтобы отличить, когда использовать?
Ответы
Ответ 1
Я не думаю, что любое дерево решений или диаграмма Венна будут существовать, потому что приложения для семейств типов и данных довольно широки.
Как правило, вы уже выделили ключевые отличия в дизайне, и я согласился бы с вашим вынос, чтобы сначала увидеть, можете ли вы уйти с data family
.
Для меня ключевым моментом является то, что каждый экземпляр data family
создает новый тип, который существенно ограничивает власть, потому что вы не можете делать то, что часто является наиболее естественным, и сделать существующий тип экземпляром.
Например, пример GMapKey
на странице Haskell на "индексированных типах" является естественным образом подходит для семейств данных:
class GMapKey k where
data GMap k :: * -> *
empty :: GMap k v
lookup :: k -> GMap k v -> Maybe v
insert :: k -> v -> GMap k v -> GMap k v
Ключевым типом карты k
является аргумент семейства данных, и фактический тип карты является результатом семейства данных (GMap k
). Как пользователь экземпляра GMapKey
, вы, вероятно, вполне довольны тем, что тип GMap k
является абстрактным для вас и просто манипулировать им с помощью общих операций отображения в классе типов.
Напротив, пример Collects
на той же странице wiki выглядит как-то наоборот:
class Collects ce where
type Elem ce
empty :: ce
insert :: Elem ce -> ce -> ce
member :: Elem ce -> ce -> Bool
toList :: ce -> [Elem ce]
Тип аргумента - это коллекция, а тип результата - это элемент коллекции. В общем, пользователь захочет работать с этими элементами напрямую, используя обычные операции над этим типом. Например, коллекция может быть IntSet
, а элемент может быть Int
. Приобложение Int
в какой-то другой тип было бы неудобным.
Примечание. Эти два примера относятся к классам классов и поэтому не нуждаются в ключевом слове family
, поскольку объявление типа внутри класса типа подразумевает, что оно должно быть семейством. Точно такие же соображения применяются, как и для автономных семей, но это всего лишь вопрос о том, как организована абстракция.
Ответ 2
(Включение полезной информации из комментариев в ответ.)
Автономный против объявления внутри класса
Два синтаксически разных способа объявления семейства типов и/или семейства данных, которые семантически эквивалентны:
автономный:
type family Foo
data family Bar
или как часть класса:
class C where
type Foo
data Bar
оба объявляют семейство типов, но внутри класса класса family
подразумевается контекст class
, поэтому GHC/Haskell аббревиатура декларации.
"Новый тип" против "Синоним типа" / "Псевдоним типа"
data family F
создает новый тип, аналогичный тому, как data F = ...
создает новый тип.
type family F
не создает новый тип, аналогичный тому, как type F = Bar Baz
не создает новый тип (он просто создает псевдоним/синоним существующего типа).
Пример неинъективности type family
Пример (слегка измененный) из Data.MonoTraversable.Element
:
import Data.ByteString as S
import Data.ByteString.Lazy as L
-- Declare a family of type synonyms, called `Element`
-- `Element` has kind `* -> *`; it takes one parameter, which we call `container`
type family Element container
-- ByteString is a container for Word8, so...
-- The Element of a `S.ByteString` is a `Word8`
type instance Element S.ByteString = Word8
-- and the Element of a `L.ByteString` is also `Word8`
type instance Element L.ByteString = Word8
В семействе типов правая часть уравнений Word8
называет существующий тип; то есть левая сторона создает новые синонимы: Element S.ByteString
и Element L.ByteString
Имея синоним, мы можем обменять Element Data.ByteString
на Word8
:
-- `w` is a Word8....
>let w = 0::Word8
-- ... and also an `Element L.ByteString`
>:t w :: Element L.ByteString
w :: Element L.ByteString :: Word8
-- ... and also an `Element S.ByteString`
>:t w :: Element S.ByteString
w :: Element S.ByteString :: Word8
-- but not an `Int`
>:t w :: Int
Couldn't match expected type `Int' with actual type `Word8'
Синонимы этих типов являются "неинъективными" ( "односторонними" ) и поэтому не обратимы.
-- As before, `Word8` matches `Element L.ByteString` ...
>(0::Word8)::(Element L.ByteString)
-- .. but GHC can't infer which `a` is the `Element` of (`L.ByteString` or `S.ByteString` ?):
>(w)::(Element a)
Couldn't match expected type `Element a'
with actual type `Element a0'
NB: `Element' is a type function, and may not be injective
The type variable `a0' is ambiguous
Хуже того, GHC не может даже решить недвусмысленные случаи!:
type instance Element Int = Bool
> True::(Element a)
> NB: `Element' is a type function, and may not be injective
Обратите внимание, что использование "может не быть"! Я думаю, что GHC консервативен и отказывается проверить, действительно ли Element
инъективен. (Возможно, потому, что программист мог добавить еще один type instance
позже, после импорта предварительно скомпилированного модуля, добавляя неоднозначность.
Пример инъективности data family
Напротив: в семействе данных каждая правая часть содержит уникальный конструктор, поэтому определения являются инъективными ( "обратимыми" ) уравнениями.
-- Declare a list-like data family
data family XList a
-- Declare a list-like instance for Char
data instance XList Char = XCons Char (XList Char) | XNil
-- Declare a number-like instance for ()
data instance XList () = XListUnit Int
-- ERROR: "Multiple declarations of `XListUnit'"
data instance XList () = XListUnit Bool
-- (Note: GHCI accepts this; the new declaration just replaces the previous one.)
С data family
, видя имя конструктора справа (XCons
или XListUnit
)
достаточно, чтобы знать тип-указатель, мы должны работать с XList ()
не a XList Char
. Поскольку имена конструкторов уникальны, эти определения являются инъективными/обратимыми.
Если type
"just" объявляет синоним, почему он семантически полезен?
Обычно синонимы type
- это просто аббревиатуры, но синонимы семейства type
добавили силу: они могут сделать простой тип (вид *
), стать синонимом "конструктора типов (вида * -> *
)) к аргументу":
type instance F A = B
делает B
совпадением F a
. Это используется, например, в Data.MonoTraversable
, чтобы сделать простые функции соответствия типа Word8
типа Element a -> a
(Element
).
Например, (немного глупо), предположим, что у нас есть версия const
, которая работает только со связанными типами:
> class Const a where constE :: (Element a) -> a -> (Element a)
> instance Const S.ByteString where constE = const
> constE (0::Word8) undefined
ERROR: Couldn't match expected type `Word8' with actual type `Element a0'
-- By providing a match `a = S.ByteString`, `Word8` matches `(Element S.ByteString)`
> constE (0::Word8) (undefined::S.ByteString)
0
-- impossible, since `Char` cannot match `Element a` under our current definitions.
> constF 'x' undefined