Dlaczego funktory Haskell mają typy pochodne tylko w swojej kategorii docelowej?

W Haskell funktor typu Functor jest zdefiniowany następująco (patrz np. Wiki Haskell ):

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

O ile mi zrozumieć (proszę mnie poprawić, jeśli się mylę), taki funktor może mieć tylko jako kategoria docelowej kategorii zbudowanego z użyciem konstruktora typu, na przykład [], Maybeitd Z drugiej strony, można myśleć o żadnej kategorii funktorów jako cel funktora, np. kategoria wszystkich typów Haskell. Na przykład Intmoże być obiektem w docelowej kategorii funktora, nie tylko Maybe Intlub [Int].

Jaka jest motywacja tego ograniczenia dla funktorów Haskell?

Nie ma żadnych ograniczeń! Kiedy zacząłem uczyć się teoretycznych podstaw dla konstruktorów typów, ten punkt również mnie zdezorientował. Dojdziemy do tego. Ale najpierw pozwól mi wyjaśnić pewne zamieszanie. Te dwa cytaty:

taki funktor może mieć tylko kategorię docelową kategorię skonstruowaną przy użyciu konstruktora typów

i

można myśleć o funktorach mających dowolną kategorię jako cel funktora, np. kategoria wszystkich typów Haskella

pokaż, że nie rozumiesz, czym jest funktor (a przynajmniej niewłaściwie używasz terminologii).

Functors nie konstruują kategorii. Funktor to odwzorowanie między kategoriami. Funktory wprowadzają obiekty i morfizmy (typy i funkcje) w kategorii źródłowej do obiektów i morfizmów w kategorii docelowej.

Zauważ, że oznacza to, że funktor to tak naprawdę para mapowań: mapowanie na obiektach F_obj i mapowanie na morfizmach F_morph . W Haskell, obiektowa część F_obj funktora jest nazwą konstruktora typu (np. List), Podczas gdy część morfizmu jest funkcją fmap(to do kompilatora Haskell należy uporządkowanie, o którym fmapmowa w dowolnym wyrażeniu). Nie możemy zatem powiedzieć, że Listjest to funktor; tylko połączenie Listi fmapjest funktorem. Mimo to ludzie znoszą notację; programiści nazywają Listfunktor, a teoretycy kategorii używają tego samego symbolu w odniesieniu do obu części funktora.

Ponadto w programowaniu prawie wszystkie funktory są endofunkorami , to znaczy kategoria źródłowa i docelowa są takie same - kategoria wszystkich typów w naszym języku. Nazwijmy tę kategorię Typem . Endofunkcja F na Type mapuje typ T na inny typ FT, a funkcja T -> S na inną funkcję FT -> FS . To odwzorowanie musi oczywiście być zgodne z prawami funktorów.

Korzystając Listz przykładu: mamy konstruktor typów List : Type -> Typei funkcję fmap: (a -> b) -> (List a -> List b), które razem tworzą funktor. T.

Jest jeszcze jeden punkt do wyjaśnienia. Pisanie List intnie tworzy nowego typu list liczb całkowitych. Ten typ już istniał . To był obiekt w naszej kategorii Typ . List Intjest po prostu sposobem na odniesienie się do tego.

Zastanawiasz się teraz, dlaczego funktor nie może odwzorować typu na, powiedzmy, Intlub String. Ale może! Wystarczy użyć funktora tożsamości. Dla każdej kategorii C funktor tożsamości odwzorowuje każdy obiekt na siebie, a morfizm na siebie. Łatwo jest sprawdzić, czy to odwzorowanie spełnia prawa funktora. W Haskell byłby to konstruktor typów, id : * -> *który mapuje każdy typ na siebie. Na przykład id intocenia na int.

Co więcej, można nawet tworzyć stałe funktory, które mapują wszystkie typy na jeden typ. Na przykład funktor ToInt : * -> *, gdzie ToInt a = intdla wszystkich typów ai mapuje wszystkie morfizmy na funkcję tożsamości liczb całkowitych: fmap f = \x -> x