Konwersja dowolnego ograniczenia klasy "C a" na "C a Bool"

Question

Istnieje wiele zalet posiadania typologii w formularzu C a Bool. Głównie dlatego, że pozwalają wykonać dowolną operację logiczną między dwoma wiązaniami, gdy normalny C a po prostu niejawnie AND wszystko.

Jeśli weźmiemy pod uwagę ~ ograniczenie klasy, można to zrobić jak tak

class Equal x y b | x y -> b 
instance Equal x x True 
instance False ~ b => Equal x y b 

ale to, co sprawia, że ​​to przypadek szczególny, jest fakt, że wprowadzenie x x w głowie instancji jest równoważna x ~ y => a następnie x y w głowie. Nie dotyczy to żadnej innej typografii. Więc jeśli staramy się zrobić coś podobnego dla klasy C otrzymujemy coś

class C' x b | x -> b 
instance C x => C' x True 
instance False ~ Bool => C' x b 

Niestety to nie działa, ponieważ tylko jeden z tych przypadków będzie kiedykolwiek podniósł, bo nie dyskryminuje typu x więc każdy typ pasuje do obu głów.

Przeczytałem również https://www.haskell.org/haskellwiki/GHC/AdvancedOverlap, który ponownie nie dotyczy żadnej klasy C, ponieważ wymaga przepisania wszystkich wystąpień oryginalnej klasy. Najlepiej byłoby, gdyby mój kod działał z GHC.Exts.Constraint i KindSignatures, aby C mógł być parametryczny.

Więc dla klasy jak ten

class Match (c :: * -> Constraint) x b | c x -> b 

Jak napisać przypadki tak że Match c x True wtedy i tylko wtedy c x, Match c x False inaczej?

Answer 1

Jest to niemożliwe w Haskell z powodu tak zwanego założenia otwartego świata. Stwierdza, że ​​zestaw wystąpień dla typografii jest otwarty, co oznacza, że ​​możesz tworzyć nowe instancje w dowolnym momencie (w przeciwieństwie do zamkniętego świata, gdzie musi istnieć ustalony zestaw instancji). Na przykład, podczas gdy typ-klaska Functor jest zdefiniowana w Preludium, mogę nadal tworzyć instancje w moim własnym kodzie, którego nie ma w Preludium.

Aby zaimplementować proponowany program, kompilator będzie potrzebował sposobu sprawdzenia, czy typ T jest instancją klasy C. Wymaga to jednak, aby kompilator znał wszystkie możliwe wystąpienia tej klasy i nie jest to możliwe z powodu założenia otwartego świata (podczas kompilowania Prelude, kompilator nie może jeszcze wiedzieć, że później wykonałeś też instancję Functor).

Jedynym sposobem, aby to działało, byłoby uwzględnienie tylko tych wystąpień, które są obecnie widoczne (ponieważ zostały zdefiniowane w bieżącym module lub dowolnym jego imporcie). Ale to doprowadziłoby do dość nieprzewidywalnego zachowania: zestaw widocznych instancji zależy nie tylko od importu modułu, ale także od importu importu, ponieważ nie można ukryć wystąpień. Tak więc zachowanie twojego kodu zależy od szczegółów implementacji twoich zależności.

Jeśli chcesz zamknięty świat, możesz zamiast niego użyć closed type families, które zostały wprowadzone w GHC 7.8. Używając ich, można napisać:

type family Equal a b :: Bool where 
    Equal x x = True 
    Equal x y = False