Исправление quasimoto, (текущая версия) :
Конечно же, нет.
http://en.wikipedia.org/wiki/Initial_algebra. List как тип (конструктор типа) это эндофунктор на Type, то есть List : Type -> Type с сигнатурой 1 + A * _, сам ADT получается отсюда уникально как начальная алгебра для данного эндофунктора.
АДТ - не функторы.
Ещё - открываем «Basic Category Theory for Computer Scientists» и ищем в индексе functor -> List.
Update: и ещё - http://ncatlab.org/nlab/show/initial algebra of an endofunctor.
Нет, конечно же. Отображение на типах не может быть функтором, никак.
Нет, конечно. Вот же перед глазами весь код начиная с категорий и далее до функторов, эндофункторов, категории Type, эндофункторов на ней и доказательства что List это такой эндофунктор. Функторные законы доказаны тоже, прошу заметить (экстенсионально, правда).
Не знаю. По построению, видимо.
Ага, а вопрос был «почему» слитно. Ну ладно.
На что?
«макросы, в отличии от систем типов, это _актуальное_ направление в исследованиях» - на эти самые актуальные исследования.
Исходная версия quasimoto, :
Конечно же, нет.
http://en.wikipedia.org/wiki/Initial_algebra. List как тип (конструктор типа) это эндофунктор на Type, то есть List : Type -> Type с сигнатурой 1 + A * _, сам ADT получается отсюда уникально как начальная алгебра для данного эндофунктора.
АДТ - не функторы.
Ещё - открываем «Basic Category Theory for Computer Scientists» и ищем в индексе functor -> List.
Нет, конечно же. Отображение на типах не может быть функтором, никак.
Нет, конечно. Вот же перед глазами весь код начиная с категорий и далее до функторов, эндофункторов, категории Type, эндофункторов на ней и доказательства что List это такой эндофунктор. Функторные законы доказаны тоже, прошу заметить (экстенсионально, правда).
Не знаю. По построению, видимо.
Ага, а вопрос был «почему» слитно. Ну ладно.
На что?
«макросы, в отличии от систем типов, это _актуальное_ направление в исследованиях» - на эти самые актуальные исследования.