Matematyczny (kategoryczny) opis klas typów

Język funkcjonalny można postrzegać jako kategorię, w której jego obiektami są typy, a między nimi funkcjonują morfizmy.

Jak pasują klasy w tym modelu?

Zakładam, że powinniśmy brać pod uwagę tylko te implementacje, które spełniają ograniczenie większości klas typów, ale które nie są wyrażone w języku Haskell. Na przykład powinniśmy brać pod uwagę tylko te wdrożenia, Functordla których fmap id ≡ idi fmap f . fmap g ≡ fmap (f . g).

Czy istnieją jakieś inne teoretyczne podstawy dla klas typów (na przykład oparte na typowych obliczeniach lambda)?

Jak pasują klasy w tym modelu?

Krótka odpowiedź brzmi: nie.

Ilekroć wprowadzasz w języku przymus, klasy typów lub inne mechanizmy polimorfizmu ad hoc, głównym problemem projektowym, z którym się stykasz, jest spójność .

Zasadniczo musisz upewnić się, że rozdzielczość klasy jest deterministyczna, aby dobrze napisany program miał jedną interpretację. Na przykład, jeśli możesz podać wiele instancji dla tego samego typu w tym samym zakresie, możesz potencjalnie napisać niejednoznaczne programy, takie jak to:

class Blah a where
   blah : a -> String 

instance Blah T where
   blah _ = "Hello"

instance Blah T where
   blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?

W zależności od wyboru przykład kompilator sprawia, blah vmógłby dorównać albo "Hello"albo "Goodbye". Dlatego znaczenie programu nie byłoby całkowicie zdeterminowane przez składnię programu, ale raczej mogło na niego wpływać arbitralne wybory dokonywane przez kompilator.

Rozwiązaniem tego problemu Haskell jest wymaganie, aby każdy typ miał co najwyżej jedną instancję dla każdej klasy. Aby to zapewnić, zezwala na deklaracje instancji tylko na najwyższym poziomie, a ponadto sprawia, że ​​wszystkie deklaracje są globalnie widoczne. W ten sposób kompilator może zawsze zasygnalizować błąd, jeśli zostanie złożona niejednoznaczna instancja.

Jednak uczynienie deklaracji widocznymi na całym świecie przełamuje złożoność semantyki. Aby odzyskać, należy podać semantykę opracowania dla języka programowania - to znaczy, jak pokazać, jak tłumaczyć programy Haskell na lepiej zachowujący się, bardziej kompozycyjny język.

To faktycznie pozwala ci również na kompilację klas - nazywa się to zwykle „tłumaczeniem dowodów” lub „transformacją słownikową” w kręgach Haskella i jest jednym z pierwszych etapów większości kompilatorów Haskell.

Klasy typów są również dobrym przykładem tego, w jaki sposób projektowanie języka programowania różni się od czystej teorii typów. Klasy typów są naprawdę niesamowitą funkcją językową, ale są dość źle wychowane z teoretycznego punktu widzenia. (Właśnie dlatego Agda w ogóle nie ma klas i dlatego Coq włącza je do infrastruktury heurystycznej wnioskowania).