Typeclass dla (co wydaje się być) kontrawariantny funktor realizacji funkcji inwersji

Question

Powiedzmy mam następujące

import Control.Category (Category, (.), id) 

data Invertible a b = Invertible (a -> b) (b -> a) 

instance Category Invertible where 
    id = Invertible Prelude.id Prelude.id 
    (Invertible f f') . (Invertible g g') = 
    Invertible (f Prelude.. g) (g' Prelude.. f') 

invert (Invertible x y) = Invertible y x 

Należy pamiętać, że prawdziwe są następujące:

invert (g . f) == invert f . invert g 

Struktura ta wydaje się bardzo podobna do contravariant functor (wikipedia), jak wynika z tego samego aksjomat:

F(g . f) = F(f) . F(g) 

w moim przypadku, F to po prostu invert.

Spojrzałem na Data.Functor.Contravariant.contramap, który posiada funkcję typu:

(a -> b) -> f b -> f a 

Ale ja nie wiem, skąd będę realizować, że w mojej sytuacji. Na przykład nie mogę wymyślić rozsądnego wyboru dla f, aw mojej sytuacji nie ma funkcji a -> b, tylko invert.

Mimo to, invert mimo to pasuje do aksjomatu matematycznego przeciwwariantnego funktora, więc myślę, że mogę go dopasować do istniejącej klasy, ale po prostu nie mogę znaleźć tego i jak to zrobić. Każda pomoc lub wskazówki będą mile widziane.

Answer 1

Kategoria ma dwie kolekcje: obiekty i morfizmy.

Zazwyczaj Haskell preludium, a wydaje się, że zajęcia w Data.Functor.Contravariant, działają tylko na bardzo wąskiej kategorii, czyli kategoria gdzie typy są obiekty i funkcje są morfizmami, zwykle oznaczany Hask. Standardowa klasa Functor jest również bardzo wąska: reprezentują tylko endofunktury na Hask: muszą przyjmować typy do typów i funkcji dla funkcji.

Weźmy na przykład funktora Maybe. Sposób, w jaki działa Maybe, polega na tym, że przyjmuje typy od a do Maybe a. Maybe map Int do Maybe Int i tak dalej (wiem, że to brzmi trochę trywialnie). Co robi się morfizmów jest kodowana przez fmap: fmap trwa f :: (a -> b), morfizmem pomiędzy dwoma obiektami w Hask i mapuje je do fmap f :: (Maybe a -> Maybe b) kolejna morfizmem w Hask pomiędzy obiektami że mapy funktor do. W Haskell nie mogliśmy zdefiniować Functor, która zajmuje np. Int do Char - wszystkie Haskell Functor s muszą być typami konstruktorów - ale w ogólnej teorii kategorii moglibyśmy.

Control.Category uogólnia trochę: obiekty o Control.Category kategorii C nadal są rodzaje [1], tak jak w HASK, ale jego morfizmów są rzeczy typu C a b. Tak więc w twoim przykładzie obiekty są nadal arbitralnymi typami, ale twoje morfizmy są rzeczy typu Invertible a b. Ponieważ twoje morfizmy nie są funkcjami, nie będziesz w stanie korzystać ze standardowych klas Functor.

Jednakże, jest to zabawa ćwiczenie w budowanie swojej teorii kategorii know-how, aby zdefiniować klasę funktor, który działa między Category kategoriach zamiast zakładając HASK, które uchwycić przykład. Pamiętaj, że funktor działa na morfizmy obiektów (typów) i.

Zostawię was z tym - zachęcamy do komentowania, jeśli chcieliby Państwo uzyskać więcej wskazówek.

---

[1] Ignorowanie numeru PolyKinds, co czyni go bardziej ogólnym.