Подтвердить что ты не робот

"Семейство типов" с "семейством данных", вкратце?

Я смущен тем, как выбирать между 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". Это хорошо, но я хотел бы лучше понять это. Есть ли диаграмма Венна или дерево решений, которое я могу отслеживать, чтобы отличить, когда использовать?

4b9b3361

Ответ 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