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?

haskell

— Giorgio
źródło

Prostota? Haskell nie ma funkcji typu pierwszej klasy, więc wszystkie funkcje są tak naprawdę tylko konstruktorami typów.

— Daniel Gratzer

@jozefg: Przepraszam za moją ignorancję: czym są „funkcje typu pierwszej klasy”?

— Giorgio,

Więc w tej funkcji rzucamy się w fprawo? W twoim scenariuszu fpowinno być tak jak normalna funkcja Haskell i mapować typy na typy. W Haskell jedyne, co mogą mieć tego rodzaju, * -> *to konstruktory typów. Rodziny typów są bardziej ogólne, ale zawsze muszą być w pełni stosowane

— Daniel Gratzer

To pytanie jest powiązane.

— Ptharien's Flame

@ jozefg: Od czasu do czasu zastanawiam się nad tym pytaniem. Przypuszczam, że ograniczenie Haskella nie wpływa na ekspresyjną moc funktorów. Załóżmy na przykład, że mamy funktor, który jest izomorficzny do funktora listy, ale nie odwzorowuje, powiedzmy, Int -> [Int], ale Int -> <fantazyjny typ bez konstruktora typu>. Więc chyba można udowodnić, że <fantazyjny typ bez konstruktora typu> jest izomorficzny dla [Int]. Zatem wybieranie obiektów zdefiniowanych za pomocą konstruktora typów jest po prostu wygodne i nie poświęca mocy ekspresji.

— Giorgio

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

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

— ogrodnik
źródło

Dziękuję za odpowiedź, to pytanie ma ponad dwa lata. „Functors nie konstruują kategorii.”: Nie powiedziałem tego. Powiedziałem, że funktory odwzorowują dwie kategorie, gdzie kategoria docelowa musi mieć postać f a, gdzie f, o ile mi wiadomo, jest konstruktorem typów. Z tego, co pamiętam z teorii kategorii, musi to być pewnego rodzaju reprezentacja kanoniczna (obiekt początkowy w kategorii kategorii? Może niewłaściwie używam terminologii). W każdym razie dokładnie przeczytam twoją odpowiedź. Wielkie dzięki.

— Giorgio

@Giorgio ups, nie zauważyłem, ile to było haha. Po prostu pojawił się w „pytaniach bez odpowiedzi”. Nie jestem pewien, co rozumiesz przez „reprezentację kanoniczną”. O ile mi wiadomo (i mogę się tutaj mylić), nie ma związku między funktorami a obiektami początkowymi / końcowymi.

— ogrodnik

Mam na myśli to: en.wikipedia.org/wiki/Initial_algebra (patrz Zastosowanie w informatyce). W Haskell (większość) funktory są zdefiniowane w algebraicznych typach danych. Obiektem docelowym takiego funktora jest początkowa algebra. Początkowa algebra jest izomorficzna w stosunku do zestawu terminów zbudowanych przy użyciu konstruktorów wartości. Np. Dla list []i :. Miałem na myśli kanoniczną reprezentację.

— Giorgio

Tak, wiem, czym jest obiekt początkowy i że typy danych indukcyjnych są obiektami początkowymi w algebrze F kategorii. Masz rację, że wiele konstruktorów typów jest zdefiniowanych indukcyjnie. Ale nie jest to absolutnie konieczne. Na przykład, funktor (_, int), który zajmuje rodzaju ado rodzaju produktu (a, int)oraz funkcję f : 'a -> 'bdo g : 'a * int -> 'a * intnie jest indukcyjne.

— ogrodnik

Czy chodziło Ci o: „trwa ... funkcję f : 'a -> 'bdo g : 'a * int -> 'b * int?

— Giorgio