Классы типов их инстанцирование, как читать?

Э-э-э, а при чём тут стрелки? Arrows - это нечто другое.

Правильно ли что запись instance Functor Something я должен читать, как - «для типа Something инстанцирован/описан/реализован Functor», но не «Something - это Functor»?

Да.

стрелка - синоним для морфизм

но не описано отображение для объектов (как pure из класса Applicative)?

Тебе нужна функция с сигнатурой a -> f a в классе Functor?

быть корректны такие высказывания, если функтор - это отображение из категории в категорию?

Могут, так как хаскелл - это не теория категорий.

Это какое-то изобретение русской языка? Как уже говорил, обычно под arrow понимают другой объект.

Тебе нужна функция с сигнатурой a -> f a в классе Functor?

я хочу порядка

Могут, так как хаскелл - это не теория категорий.

Но тем не менее он напичкан понятиями из нее. То есть ты считаешь, что List - это функтор и я могу рассматривать функтор, как контейнер?

я могу рассматривать функтор, как контейнер?

Скорее наоборот.

Это какое-то изобретение русской языка? Как уже говорил, обычно под arrow понимают другой объект.

Category theory is used to formalize mathematics and its concepts as a collection of objects and arrows (also called morphisms)

я пользуюсь википедией

я могу рассматривать функтор, как контейнер?

Скорее наоборот.

Я пытаюсь понять высказывание «apply functions inside the functor»

я хочу порядка

В хаскелле порядка и близко нету, ищи лучше в другом месте.

То есть ты считаешь, что List - это функтор и я могу рассматривать функтор, как контейнер?

Если дать определение функтору как контейнеру, для которого определена операция fmap, то [] - это функтор, да.

Вот еще класс

class Category cat where
  id :: cat a a
  (.) :: cat b c -> cat a b -> cat a c

Я понимаю, что cat здесь не категория, но тип морфизмов(стрелок), просто на основании типов которыми характеризуется этот морфизм - мы можем также описать категорию.

На предмет строгого математического объяснения нужно спрашивать quasimoto.

Если я правильно помню, функтор - отображение одной категории в другую. При этом должен быть гомоморфизм и между объектами и морфизмами. Думаю, «apply functions inside the functor» - это формулировка второго требования. Надеюсь, я не слишком заблуждаюсь и меня поправят.

Сам я пишу на C++ и привык читать инстанцирование класса, как «ConcreteObject - это SomeClass». Как мне показалось, в haskell так делать нельзя.

То что в C++ называется классами и объектами в Haskell называется ADT и значениями (термами).

Например, такой код с классами, объектами и методами:

#include <cstdio>

struct a_t {
    int x, y;
    int sum() { return x + y; }
};

class ab_t {

    // @tagged_union
    enum { a_tag, b_tag } tag;
    union {
        a_t a;
        struct {
            int x, y, z;
            int sum() { return x + y + z; }
        } b;
    } ab_u;

  public:

    ab_t(a_t a_) : tag(a_tag) { ab_u.a = a_; }
    ab_t(int x_, int y_, int z_) : tag(b_tag) { ab_u.b = { x_, y_, z_ }; }

    int sum() { return tag == a_tag ? ab_u.a.sum() : ab_u.b.sum(); }

};

int main()
{
    ab_t ab1({1, 2});
    ab_t ab2(3, 4, 5);
    printf("ab1.sum = %d; ab2.sum = %d\n", ab1.sum(), ab2.sum());
}

В Haskell переводится в код с ADT, значениями и функциями:

import Text.Printf

data A = A Int Int

data AB = A_ A | B Int Int Int

a_ :: Int -> Int -> AB
a_ x y = A_ $ A x y

sumA :: A -> Int
sumA (A x y) = x + y

sumAB :: AB -> Int
sumAB (A_ a) = sumA a
sumAB (B x y z) = x + y + z

main :: IO ()
main = printf "sumAB a = %d; sumAB b = %d\n" (sumAB $ a_ 1 2) (sumAB $ B 3 4 5)

«объект класса» превращается в «терм/значение (алгебраического) типа».

Разница между классами и методами C++ и ADT и функциями Haskell в том, что в C++ может легко начаться наследование, подтипирование и динамическая диспетчеризация, тогда как в Haskell это делается не так легко.

Теперь, если применить в Haskell концепцию классов типов:

class Sum t where
  sumt :: t -> Int

instance Sum A where
  sumt (A x y) = x + y

instance Sum AB where
  sumt (A_ a) = sumt a
  sumt (B x y z) = x + y + z

main :: IO ()
main = printf "sum a = %d; sum b = %d\n" (sumt $ a_ 1 2) (sumt $ B 3 4 5)

то, наоборот, в С++ это уже не так легко. Классы типов не имеют отношения к классам С++, они имеют отношения к интерфейсам и концептам - первые в С++ довольно неудобны:

struct sum_i {
    virtual ~sum_i() {}
    virtual int sum() const = 0;
};

struct a_t : public sum_i {
    int x, y;
    a_t(int x_, int y_) : x(x_), y(y_) {}
    int sum() const { return x + y; }
};

class ab_t : public sum_i {
    // ?
};

а вторых ещё нет (про функторы на них можно посмотреть тут - http://www.pik-potsdam.de/members/lincke/papers/Lincke_et_al_SCP.pdf).

говорит о том что для типа [] определен функтор осуществляющий отображение стрелок над элементами списка в стрелки над списками

[] это и есть функтор - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.9637. Класс типов Functor это не функтор и не тип, если мы его интернализируем в язык, это будет класс. То есть если 5 :: Int :: * :: **, тогда Functor :: (* -> *) -> ** (Functor :: (* -> *) -> Constraint в нынешнем GHC, то есть оно там «constraint»).

В зависимости от того, каким функтором является ADT, можно про него сказать разные вещи, в том числе, является ли этот ADT хорошим, то есть не приведёт ли его существование к противоречиям в языке («строго-позитивные функторы»).

А сущность Functor это вещь (класс/constraint) которая нужна либо для того чтобы принять на веру что данный ADT это функтор, объявить функторный интерфейс и реализовать его для данного ADT, либо для того чтобы _доказать_ что данный ADT это функтор (ну и тоже - объявить функторный интерфейс и реализовать его для данного ADT).

«для типа Something инстанцирован/описан/реализован Functor», но не «Something - это Functor»?

Тип Something :: * -> * это функтор (с маленькой буквы и если это ещё функтор, конечно), что подтверждается существованием для этого типа инстанса класса типов (класса) Functor (с большой буквы), если в языке выразимы аксиомы функтора это будет буквальным подтверждением, то есть строгим доказательством того что Something - функтор.

Ну и почему в классе Functor описано отображение для стрелок, но не описано отображение для объектов (как pure из класса Applicative)?

Отображением стрелок/значений/конструкторов/термов/функций/программ занимается стрелка/функция/программа fmap :: (a -> b) -> (f a -> f b) в рантайме, отображением объектов/типов занимается функтор/конструктор типов f :: * -> * во время компиляции. Все Functor, Pointed, Applicative, Monad описывают, на самом деле, только эндофункторы только одной категории Hask - категории всех типов и термов/конструкторов/классов эквивалентности функций-программ (если мы ограничиваемся 1-категорией). Kind * это как раз класс-универсум всех типов, то есть объектов Hask, так что выхлоп GHCi [] :: * -> * на :k [] это, натурально, [] : Hask -> Hask, то есть повод задуматься о том, что конструктор типов [] это эндофунктор на Hask (это нужно доказать основываясь на индуктивном определении []).

[] это и есть функтор

s/ADT/тип/g после этой фразы.

Правильно ли что запись instance Functor Something я должен читать, как - «для типа Something инстанцирован/описан/реализован Functor», но не «Something - это Functor»?

Не вполне.

Класс — это интерфейс. instance Functor Something означает «тип Something реализует этот интерфейс вот так». Поскольку, если ты не обращаешься к чёрной магии, двух разных реализаций одного и того же интерфейса (класса) быть не может, ты можешь считать, что тип Something таким образом СТАЛ функтором.

если функтор - это отображение из категории в категорию

Класс Functor описывает несколько более узкое понятие — отображение из категории Hask в категорию Hask. Категория Hask — это категория, в которой объектами являются хаскельные типы, а морфизмами — функции между ними. Поэтому [] — вполне себе функтор.

Ну и почему в классе Functor описано отображение для стрелок, но не описано отображение для объектов (как pure из класса Applicative)?

Описано. Видишь там буковку «f»? В строчке «class Functor f where»? Вот эта буковка и означает отображение. Объекту Hask (т.е., некоторому типу) a сопоставляется объект Hask (т.е., некоторый тип) f a.

А при чём тут pure?

[] это и есть функтор ...

Хорошо, я понял, что для списка конструктор одного аргумента осуществляет отображение a -> [a]

List (и другой ADT с инстансом Functor) можно назвать эндофунктором из Hask в Hask, это обеспечивается самим существованием этого ADT и инстанса Functor (конструктор и fmap).

А можно ли сказать что конструктор одного аргумента для списка и функция map создают функтор из категории значений в категорию списков значений (или слишком по дилетантски =) )?

А при чём тут pure?

по сигнатуре подошел

из категории значений в категорию списков значений

Как уже выше сказали, категория здесь одна - Hask, и все функторы являются эндофункторами. Ну а ф-я map даже по сигнатуре не имеет отношения к функторам, имелась в виду fmap?

абстрактно без привязки к категории Hask и к классу типов Functor

то есть категория с объектами a, стрелками a -> a (пусть даже с ограничением, что a - это не список)

а есть категория с объектами [a], стрелками [a] -> [a]

и есть между ними функтор состоящий из [] и map

можно ли так говорить?

по сигнатуре подошел

pure — морфизм. Точнее, семейство морфизмов. Каким раком оно подходит к функтору?

я понял, что для списка конструктор одного аргумента осуществляет отображение a -> [a]

По моему, не понял :) Ты говоришь про возможность получить из значения «element» значение [«element»]? То есть про pure/return = \x -> [x]? Это совсем не то. Есть типы которые являются функторами, но для которых нельзя написать функцию return/pure (они не являются точечными функторами):

-- | Простейший класс (Set₁) описывающий эндофунктор (F) на классе всех типов (Set).
-- 
--   Функторные законы принимаются на веру и не проверяются.
-- 
record Functor (F : Set → Set) : Set₁ where
  field fmap : ∀ {A B} → (A → B) → (F A → F B)

-- | Класс для точечных функторов (опять без теорем).
-- 
record Pointed (F : Set → Set) (f : Functor F) : Set₁ where
  open Functor f
  field pure : ∀ {A} → A → F A

-- | Тип (Set) населённых типов (Set).
-- 
record Inhabited (A : Set) : Set where
  field point : A

open import Function
open import Data.Unit

-- | Всякий населённый функтор будет точечным.
-- 
inhabited-functor-is-pointed : ∀ {F} → (f : Functor F) → Inhabited (F ⊤) → Pointed F f
inhabited-functor-is-pointed f i = record
  { pure = λ x → fmap (const x) point
  } where open Functor f; open Inhabited i

open import Data.Product

-- | Функтор.
-- 
left-product-is-functor : ∀ {A} → Functor (λ B → A × B)
left-product-is-functor = record
  { fmap = λ f ab → proj₁ ab , f (proj₂ ab)
  }

-- | Точечный?
-- 
left-product-is-pointed? : ∀ {A} → Pointed (λ B → A × B) left-product-is-functor
left-product-is-pointed? = record
  { pure = {!!} -- ?0 : {A : Set} → A → .A × A
  }

open import Data.Empty

-- | Нет.
-- 
no-wai : ⊤ → ⊤ × ⊥ → ⊥
no-wai tt (tt , ())

А можно ли сказать что конструктор одного аргумента

Что такое «конструктор одного аргумента»? Тут есть особенность в терминологии ─ просто конструктор это, например, (:) или Just. Опять же, они тут не играют ключевой роли. А вот «одно-параметрический конструктор типа» это непосредственно параметрически-полиморфный тип с одним параметром, например, контейнеры List :: * -> * и Maybe :: * -> *. Они работают в type-level и их вообще можно стереть во время компиляции, образовав всевозможные специализации ListInt, MaybeDouble и т.п. (так же как в случае с шаблонами плюсов).

функтор из категории значений в категорию списков значений

Hask, так же как и изначальная конструкция Lambekа (ну и Scottа ещё) вообще не умеет конкретные значения, в ней есть типы (вроде Int или [Int]) в качестве объектов и классы эквивалентности (modulo β/η) термов (функций, вроде Int -> [Int] или Maybe [a -> b] -> [Maybe [a -> b]]) в качестве морфизмов. Также Hask замкнута, поэтому такой класс эквивалентности может играть роль типа (internal hom), этим отражаются ФВП. В таком случае функтор f : Hask -> Hask работает на уровне типов ─ из любых типов a (Int, Double, ...) можно получить типы f a ([Int], [Double], ..., Maybe Int, Maybe Double, ...). На уровне термов необходимо, чтобы все функции вида a -> a (Int -> Int, Double -> Double, ...) можно было отобразить в функции вида f a -> f a ([Int] -> [Int], [Double] -> [Double], ..., Maybe Int -> Maybe Int, Maybe Double -> Maybe Double, ...) так, чтобы выполнялись функторные законы.

А чтобы категорно рассуждать про конкретные значения, редукции и переписывания нужны высшие категории (2-категории ─ Seely, Hilken, например) и струнные диаграммы в дополнение к коммутативным. При этом возникают вопросы типа «если 5 ─ стрелка, то является ли она типом на правах экспоненциала или категория уже не замкнута относительно таких стрелок?».

Но и в Hask можно строить разные категории и прочие функторы. Например, подкатегорию с объектами {1, ℕ} и числовыми функциями в качестве стрелок, или подкатегорию из {1, List} и функций на списках, и потом строить функцию length как (не эндо) функтор который переводит {1, ℕ} -> {1, List} и функции из списков длины m в списки длины n в функции из чисел m в числа n. Либо можно взять Hask или любую её подкатегорию и построить какую-нибудь comma категорию, например, категорию ℕ→ в которой стрелки-числовые-функции станут объектами, а стрелками из числовых функций f и g будут пары числовых функций f' и g' таких, что f' ∘ f ≡ g ∘ g', то есть f'(f(n)) ≡ g(g'(n)) для всех n. В общем, была бы необходимость.

абстрактно без привязки к категории Hask и к классу типов Functor

Вот абстрактное определение категории:

open import Level
open import Relation.Binary hiding ( _⇒_ )

-- | Класс объектов размера o, стрелок размера a, internal эквивалентность стрелок размера e.
-- 
record Category {o a e} : Set (suc (o ⊔ a ⊔ e)) where

  infix 9 _∘_
  infix 4 _≡_

  field

    Obj       : Set o
    _⇒_       : Obj → Obj → Set a -- Rel obj a
    _≡_       : ∀ {A B} → A ⇒ B → A ⇒ B → Set e -- Rel (A ⇒ B) e

    dom       : ∀ {A B} → A ⇒ B → A ⇒ A
    cod       : ∀ {A B} → A ⇒ B → B ⇒ B

    id        : ∀ {A} → A ⇒ A
    _∘_       : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C

    dom-id    : ∀ {A} → dom (id {A}) ≡ id 
    cod-id    : ∀ {A} → cod (id {A}) ≡ id 

    dom-com   : ∀ {A B C} {f : A ⇒ B} {g : B ⇒ C} → dom (g ∘ f) ≡ dom f
    cod-com   : ∀ {A B C} {f : A ⇒ B} {g : B ⇒ C} → cod (g ∘ f) ≡ cod g

    id-com    : ∀ {A B} {f : A ⇒ B} → id ∘ f ≡ f
    com-id    : ∀ {A B} {f : A ⇒ B} → f ∘ id ≡ f

    com-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)

    equiv     : ∀ {A B} → IsEquivalence (_≡_ {A} {B})
    com-equiv : ∀ {A B C} {x y : A ⇒ B} {u v : B ⇒ C} → x ≡ y → u ≡ v → u ∘ x ≡ v ∘ y

Где Obj это множество либо класс (и далее по иерархии) «объектов», _⇒_ ─ бинарное отношение на объектах задающее стрелки, _≡_ ─ отношение на стрелках задающее эквивалентность. Остальное ─ типичные конструкции на стрелках (dom, cod, id, _∘_) и законы категории (всё что использует внутреннюю ≡-эквивалентность).

И функтора:

record Functor {o a e o′ a′ e′} (C₁ : Category {o} {a} {e}) (C₂ : Category {o′} {a′} {e′}) : Set (o ⊔ a ⊔ e ⊔ o′ ⊔ a′ ⊔ e′) where

  open Category C₁ using () renaming (Obj to O₁; _⇒_ to _⇒₁_; id to id₁; _∘_ to _∘₁_; _≡_ to _≡₁_)
  open Category C₂ using () renaming (Obj to O₂; _⇒_ to _⇒₂_; id to id₂; _∘_ to _∘₂_; _≡_ to _≡₂_)

  field

    F            : O₁ → O₂
    F′           : ∀ {A B} → A ⇒₁ B → F A ⇒₂ F B

    identity     : ∀ {A} → F′ id₁ ≡₂ id₂ {F A}
    homomorphism : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → F′ (g ∘₁ f) ≡₂ F′ g ∘₂ F′ f

Тут F отображает объекты, F′ ─ стрелки, identity и homomorphism задают функторные законы (опять с использованием ≡--эквивалентности).

Если упростить такой функтор до действия на одной категории, получится эндофунктор:

EndoFunctor : ∀ {o a e} → Category {o} {a} {e} → Set _
EndoFunctor C = Functor C C

Если теперь выбрать в качестве действуемой категории категорию языковых типов и функций:

open import Function
open import Relation.Binary.PropositionalEquality

Agdask : Category
Agdask = record

  { Obj = Set
  ; _⇒_ = λ a b → a → b
  ; _≡_ = _≡_

  ; dom = const id
  ; cod = const id

  ; id = id
  ; _∘_ = _∘′_
  
  ; dom-id = refl
  ; cod-id = refl

  ; dom-com = refl
  ; cod-com = refl

  ; id-com = refl
  ; com-id = refl

  ; com-assoc = refl

  ; equiv = isEquivalence
  ; com-equiv = cong₂ (flip _∘′_)
  }

то можно получить ещё более простой функтор:

SimpleFunctor = EndoFunctor Agdask

вот это то что является концептом Functor в Haskell. Например, список является таким функтором:

open import Data.List
open import Data.List.Properties

postulate
  extensionality : ∀ {a b} → Extensionality a b

List-is-Functor : SimpleFunctor
List-is-Functor = record
  { F = List
  ; F′ = map
  ; identity = extensionality map-id
  ; homomorphism = extensionality map-compose
  }

Тут отображением занимаются List ([] :: * -> *) и map, то есть совсем не pure = × -> [x] и map.

Вообще же понятия «категория», «функтор» и т.п. шире, такой функтор это весьма специальный случай, но в ЯП, в которых полно типов-функторов, он может иметь смысл как полезный интерфейс.

inhabited-functor-is-pointed : ∀ {F A} → (f : Functor F) → Inhabited (F A) → Pointed F f

fix

Спасибо за такие развернутые ответы. А что это за синтаксис в выкладках? Какой-то более низкий уровень ghc?

Agda, насколько я могу судить.

Спасибо

Вот как оказывается опасно иметь дело с хаскелем для непосвященного, можно утонуть в теории =)

Какой-то более низкий уровень ghc?

Скорее наоборот - http://wiki.portal.chalmers.se/agda/pmwiki.php.

«для типа Something инстанцирован/описан/реализован Functor»

как-то криво звучит, аналогия с крестами не совсем уместна: класс над adt используется лишь в плане наследования

по-простому конкретный функтор можно воспринимать как тип (имеющий kind * -> *, то есть принмающий тип а и возвращающий f a), для которого определена «apply functions inside the functor», то есть fmap

а сам класс - как подмножество типов вида * -> *.

корректны такие высказывания

просто разная интерпетация: 1-ая (function `fmap` someFunctor) - возвращает новый фунтор, 2-ая (fmap function) - из фукции, возвращает другую, оперирующую уже над функторами