Почему функторы Haskell имеют только производные типы в своей целевой категории?

12

В Haskell функтор класса типов Functor определяется следующим образом (см., Например, вики Haskell ):

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b 

Насколько я понимаю (пожалуйста, исправьте меня, если я ошибаюсь), такой функтор может иметь только в качестве целевой категории категорию, созданную с помощью конструктора типов, например [], Maybeи т. Д. С другой стороны, можно подумать о функторах, имеющих любую категорию в качестве цели функтора, например, категория всех типов Haskell. Например, Intможет быть объект в целевой категории функтора, а не просто Maybe Intили [Int].

Какова мотивация для этого ограничения на функторы Хаскеля?

Джорджио
источник
4
Простота? У Haskell нет функций типа первого класса, поэтому все функции на самом деле являются просто конструкторами типов.
Даниэль Гратцер
2
@jozefg: простите мое невежество: что такое «функции первого класса»?
Джорджио
4
Таким образом, в этой функции мы бросаем вокруг fправа? И в вашем сценарии она fдолжна быть похожа на обычную функцию Haskell и отображать типы на типы. В Haskell единственными вещами, которые могут иметь тип, * -> *являются конструкторы типов. Типовые семьи носят более общий характер, но они всегда должны применяться полностью
Даниэль Гратцер,
Этот вопрос связан.
Пламя Птариена
@jozefg: я иногда думаю об этом вопросе снова и снова. Я полагаю, что ограничение Haskell не влияет на выразительную силу функторов. Например, предположим, что у нас есть функтор, который изоморфен функтору списка, но не отображает, скажем, Int -> [Int], но Int -> <причудливый тип, не используя конструктор типов>. Тогда, я думаю, можно доказать, что <необычный тип без конструктора типов> изоморфен [Int]. Поэтому выбор объектов, определенных с помощью конструктора типов, просто удобен и не жертвует выразительной силой.
Джорджио

Ответы:

1

Там нет никаких ограничений на всех! Когда я начал изучать теоретико-категорийную основу для конструкторов типов, этот момент меня и смутил. Мы доберемся до этого. Но сначала позвольте мне прояснить некоторую путаницу. Эти две цитаты:

такой функтор может иметь только в качестве целевой категории категорию, созданную с использованием конструктора типа

и

можно думать о функторах, имеющих любую категорию как цель функтора, например, категорию всех типов Haskell

покажите, что вы неправильно понимаете, что такое функтор (или, по крайней мере, вы неправильно используете терминологию).

Функторы не сооружать категории. Функтор - это отображение между категориями. Функторы переносят объекты и морфизмы (типы и функции) в исходной категории к объекту и морфизмы в целевой категории.

Обратите внимание, что это означает, что функтор - это действительно пара отображений: отображение объектов F_obj и отображение морфизмов F_morph . В Haskell объектная часть F_obj функтора - это имя конструктора типа (например List), в то время как часть морфизма - это функция fmap(компилятор Haskell должен разобраться, на что fmapмы ссылаемся в любом данном выражении). Таким образом, мы не можем сказать, что Listэто функтор; только комбинация Listи fmapявляется функтором. Тем не менее, люди злоупотребляют нотацией; программисты вызывают Listфунктор, в то время как теоретики категорий используют один и тот же символ для ссылки на обе части функтора.

Кроме того, в программировании почти все функторы являются эндофункторами , то есть исходная и целевая категории одинаковы - категория всех типов в нашем языке. Давайте назовем эту категорию типом . Endofunctor F в Type отображает тип T в другой тип FT, а функцию T -> S в другую функцию FT -> FS . Это отображение должно, конечно, подчиняться законам функторов.

В Listкачестве примера: у нас есть конструктор типа List : Type -> Typeи функция fmap: (a -> b) -> (List a -> List b), которые вместе образуют функтор. T

Есть один последний момент, чтобы прояснить. Запись List intне создает новый тип списков целых чисел. Этот тип уже существовал . Это был объект в нашей категории Type . List Intэто просто способ сослаться на это.

Теперь вам интересно, почему функтор не может сопоставить тип, скажем, Intили String. Но это может! Нужно просто использовать функтор идентичности. Для любой категории C функтор идентичности отображает каждый объект на себя и морфизм на себя. Нетрудно убедиться, что это отображение удовлетворяет законам функторов. В Haskell это будет конструктор типов, id : * -> *который отображает каждый тип на себя. Например, id intоценивает до int.

Более того, можно даже создавать постоянные функторы, которые отображают все типы в один тип. Например, функтор ToInt : * -> *, где ToInt a = intдля всех типов a, и отображает все морфизмы в целочисленную функцию идентичности: fmap f = \x -> x

gardenhead
источник
Спасибо за ваш ответ, этому вопросу более двух лет. «Функторы не создают категории». Я этого не говорил. Я сказал, что функторы отображают две категории, где целевая категория должна иметь форму f a, где f, насколько я знаю, конструктор типов. Из того, что я помню из теории категорий, это должно быть какое-то каноническое представление (исходный объект в категории категорий? Возможно, я неправильно использую терминологию.) В любом случае, я внимательно прочитаю ваш ответ. Большое спасибо.
Джорджио
@ Джорджио, блин, я не заметил, сколько лет было, ха-ха. Это только обнаружилось в "неотвеченных вопросах". Я не уверен, что вы подразумеваете под "каноническим представлением". Насколько я знаю (и я могу ошибаться), между функторами и начальными / терминальными объектами нет никакой связи.
садовник
Я имею в виду это: en.wikipedia.org/wiki/Initial_algebra (см. Использование в информатике). В Haskell (большинство) функторы определены на алгебраических типах данных. Целевым объектом такого функтора является начальная алгебра. Исходная алгебра изоморфна множеству членов, построенных с использованием конструкторов значений. Например, для списков []и :. Я имел в виду это под каноническим представлением.
Джорджио
Да, я знаю, что такое начальный объект, и что индуктивные типы данных являются начальными объектами в F-алгебре категории. Вы правы, что многие конструкторы типов определены индуктивно. Но это не обязательно. Например, функтор , (_, int)который принимает тип aк типу продукта (a, int)и функцию f : 'a -> 'bдля g : 'a * int -> 'a * intне индуктивный.
садовник
Возможно , вы имели в виду: «берет ... функцию , f : 'a -> 'bчтобы g : 'a * int -> 'b * int?
Giorgio