Связанные типы и элементы контейнера

Думаю, я мог бы спросить об этом в Haskell-Cafe в какой-то момент, но, черт возьми, если я смогу найти ответ сейчас... Так что я снова прошу об этом здесь, поэтому, надеюсь, в будущем я смогу найти ответ!

Хаскелл фантастичен в борьбе с параметрическим полиморфизмом. Но проблема в том, что не все параметрическое. В качестве тривиального примера предположим, что мы хотим извлечь первый элемент данных из контейнера. Для параметрического типа это тривиально:

class HasFirst c where
  first :: c x -> Maybe x

instance HasFirst [] where
  first []    = Nothing
  first (x:_) = Just x

Теперь попробуйте написать экземпляр для ByteString. Вы не можете. Его тип не упоминает тип элемента. Вы также не можете написать экземпляр для Set, потому что для него требуется ограничение Ord, но глава класса не упоминает тип элемента, поэтому вы не можете его ограничить.

Связанные типы обеспечивают аккуратный способ полностью решить эти проблемы:

class HasFirst c where
  type Element c :: *
  first :: c -> Maybe (Element c)

instance HasFirst [x] where
  type Element [x] = x
  first []    = Nothing
  first (x:_) = Just x

instance HasFirst ByteString where
  type Element ByteString = Word8
  first b = b ! 0

instance Ord x => HasFirst (Set x) where
  type Element (Set x) = x
  first s = findMin s

Теперь у нас есть новая проблема. Попробуйте "исправить" Functor, чтобы он работал для всех типов контейнеров:

class Functor f where
  type Element f :: *
  fmap :: (Functor f2) => (Element f -> Element f2) -> f -> f2

Это не работает вообще. Он говорит, что если у нас есть функция от типа элемента f до типа элемента f2, мы можем превратить f в f2. Все идет нормально. Однако, по-видимому, нет способа потребовать, чтобы f и f2 были контейнерами одного и того же типа!

В соответствии с существующим определением Functor мы имеем

fmap :: (x -> y) -> [x] -> [y]
fmap :: (x -> y) -> Seq x -> Seq y
fmap :: (x -> y) -> IO x -> IO y

Но мы не имеем fmap :: (x -> y) -> IO x -> [y]. Это совершенно невозможно. Но определение класса выше позволяет это.

Кто-нибудь знает, как объяснить системе типов то, что я на самом деле имел в виду?

Edit

Вышеописанное работает, определяя способ вычисления типа элемента из типа контейнера. Что произойдет, если вы попытаетесь сделать это наоборот? Определить функцию для вычисления типа контейнера из типа элемента? Легко ли это работает?

Ответы

Ответ 1

Ну, проблема в том, что неясно, что означает пересмотренный Functor. Например, рассмотрим ByteString. A ByteString может отображаться только путем замены каждого элемента Word8 на элемент того же типа. Но Functor - для параметрических отображаемых структур. На самом деле существуют два противоречивых понятия отображения:

  • Жесткое отображение (т.е. преобразование каждого элемента структуры без изменения его типа)
  • Параметрическое отображение (т.е. преобразование каждого элемента структуры в любой тип)

Итак, в этом случае вы не можете объяснить системе типов, что вы имели в виду, потому что это не имеет большого смысла. Вы можете, однако, изменить то, что вы имеете в виду:)

Жесткое отображение легко выразить с помощью семейств типов:

class RigidMap f where
  type Element f :: *
  rigidMap :: (Element f -> Element f) -> f -> f

Что касается параметрического отображения, существует множество способов сделать это. Самый простой способ - сохранить текущий Functor как есть. Вместе эти классы охватывают такие структуры, как ByteString, [], Seq и т.д. Однако все они падают на Set и Map из-за ограничения Ord на значения. К счастью, расширение в GHC 7.4 позволяет решить эту проблему:

class RFunctor f where
  type Element f a :: Constraint
  type Element f a = ()  -- default empty constraint
  fmap :: (Element f a, Element f b) => (a -> b) -> f a -> f b

Здесь мы говорим, что каждый экземпляр должен иметь связанное ограничение типа. Например, экземпляр Set будет иметь Element Set a = Ord a, чтобы обозначить, что Set можно построить, только если для типа доступен экземпляр Ord. Все, что может появиться в левой части =>, принимается. Мы можем определить наши предыдущие экземпляры точно так, как они были, но мы также можем сделать Set и Map:

instance RFunctor Set where
  type Element Set a = Ord a
  fmap = Set.map

instance RFunctor Map where
  type Element Map a = Ord a
  fmap = Map.map

Однако, это довольно раздражает необходимость использования двух отдельных интерфейсов для жесткого сопоставления и ограниченного параметрического отображения. На самом деле, не последнее ли обобщение первого? Рассмотрим разницу между Set, которая может содержать только экземпляры Ord и ByteString, которые могут содержать только Word8 s. Неужели мы можем выразить это как просто другое ограничение?

Мы применяем тот же трюк, сделанный с помощью HasFirst (т.е. даем экземпляры всей структуры и используем семейство типов для раскрытия типа элемента) и вводим новое связанное семейство ограничений:

class Mappable f where
  type Element f :: *
  type Result f a r :: Constraint
  map :: (Result f a r) => (Element f -> a) -> f -> r

Идея здесь заключается в том, что Result f a r выражает ограничения, необходимые для типа значения (например, Ord a), а также ограничивает результирующий тип контейнера, но ему нужно; предположительно, чтобы гарантировать, что он имеет тип контейнера такого же типа a s. Например, Result [a] b r предположительно потребует, чтобы r был [b], а Result ByteString b r потребовал, чтобы b был Word8, а r - ByteString.

Типичные семейства уже дают нам то, что нам нужно, чтобы выразить "есть" здесь: ограничение равенства типа. Мы можем сказать, что (a ~ b) => ... требует, чтобы a и b были одного типа. Разумеется, мы можем использовать это в определениях семейств ограничений. Итак, у нас есть все, что нам нужно; на экземпляры:

instance Mappable [a] where
  type Element [a] = a
  type Result [a] b r = r ~ [b]
  -- The type in this case works out as:
  --   map :: (r ~ [b]) => (a -> b) -> [a] -> r
  -- which simplifies to:
  --   map :: (a -> b) -> [a] -> [b]
  map = Prelude.map

instance Mappable ByteString where
  type Element ByteString = Word8
  type Result ByteString a r = (a ~ Word8, r ~ ByteString)
  -- The type is:
  --   map :: (b ~ Word8, r ~ ByteString) => (Word8 -> b) -> ByteString -> r
  -- which simplifies to:
  --   map :: (Word8 -> Word8) -> ByteString -> ByteString
  map = ByteString.map

instance (Ord a) => Mappable (Set a) where
  type Element (Set a) = a
  type Result (Set a) b r = (Ord b, r ~ Set b)
  -- The type is:
  --   map :: (Ord a, Ord b, r ~ Set b) => (a -> b) -> Set a -> r
  -- (note the (Ord a) constraint from the instance head)
  -- which simplifies to:
  --   map :: (Ord a, Ord b) => (a -> b) -> Set a -> Set b
  map = Set.map

Perfect! Мы можем определить экземпляры для любого типа контейнера, который мы хотим, жесткого, параметрического или параметрического, но ограниченного, и типы отлично работают.

Отказ от ответственности: я еще не пробовал GHC 7.4, поэтому я не знаю, действительно ли какой-либо из них действительно компилируется или работает, но я думаю, что основные идеи звучат.