В Haskell функтор класса типов Functor определяется следующим образом (см., Например, вики Haskell ):
class Functor (f :: * -> *) where
fmap :: (a -> b) -> f a -> f b
Насколько я понимаю (пожалуйста, исправьте меня, если я ошибаюсь), такой функтор может иметь только в качестве целевой категории категорию, созданную с помощью конструктора типов, например []
, Maybe
и т. Д. С другой стороны, можно подумать о функторах, имеющих любую категорию в качестве цели функтора, например, категория всех типов Haskell. Например, Int
может быть объект в целевой категории функтора, а не просто Maybe Int
или [Int]
.
Какова мотивация для этого ограничения на функторы Хаскеля?
f
права? И в вашем сценарии онаf
должна быть похожа на обычную функцию Haskell и отображать типы на типы. В 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
источник
f a
, гдеf
, насколько я знаю, конструктор типов. Из того, что я помню из теории категорий, это должно быть какое-то каноническое представление (исходный объект в категории категорий? Возможно, я неправильно использую терминологию.) В любом случае, я внимательно прочитаю ваш ответ. Большое спасибо.[]
и:
. Я имел в виду это под каноническим представлением.(_, int)
который принимает типa
к типу продукта(a, int)
и функциюf : 'a -> 'b
дляg : 'a * int -> 'a * int
не индуктивный.f : 'a -> 'b
чтобыg : 'a * int -> 'b * int
?