Dowody stosowania praw dla instancji haskell

Question

Czy wszystkie przykłady Haskella Applicative Typeclass, które otrzymujemy z platformą Haskell, zostały udowodnione, że spełniają wszystkie prawa aplikacyjne? Jeśli tak, gdzie znajdujemy te dowody?

Kod źródłowy Control.Applicative nie zawiera żadnego dowodu na to, że przepisy dotyczące stosowania różnych instancji nie istnieją. To po prostu mówi, że

-- | A functor with application. 
-- 
--Instances should satisfy the following laws: 

to wtedy po prostu stwierdza, przepisy ustawowe w komentarzach.

Znalazłem podobny przypadek dla wystąpień innych czcionek (Alternatywa i Monada).

Czy użytkownicy tych bibliotek mają samodzielnie zweryfikować te prawa?

Ale zastanawiałem się, czy rygorystyczne dowody tych praw zostały podane przez deweloperów gdzie indziej?

Ponownie, zdaję sobie sprawę z tego, że rygorystyczny dowód stosowania prawa (w Monadzie) dla IO Monad, który obejmuje rozmowę ze światem zewnętrznym, może być bardzo złożony.

Dzięki.

Answer 1

Tak, ciężar dowodu spoczywa wyłącznie na autorach bibliotek. Istnieje kilka przykładów implementacji, które naruszają te prawa. Kanonicznym przykładem naruszenia prawa jest ListT, co nie jest zgodne z prawami monady dla większości bazowych monad (zob. examples). Daje to bardzo błędne zachowanie i nikt tak naprawdę nie używa ListT jako wyniku.

Jestem prawie pewien, że większość tego rodzaju dowodów nie została wyryta w kamieniu w standardowym miejscu. Większość dowodów została po prostu powtórzona i sprawdzona na śmierć przez różnych ciekawych członków społeczności, więc po pewnym czasie wiemy, które implementacje nie spełniają ich praw.

Aby podać konkretny przykład, gdy piszę pipes bibliotekę, muszę udowodnić, że mój pipes spełniać Category ustawowe, ale ja po prostu zachować te dowody w pliku tekstowym lub hpaste dla przyszłych rekord jeśli ktoś prosi je. Włączenie ich do źródła nie jest możliwe, ponieważ mogą być bardzo długie, zwłaszcza w przypadku praw zrzeszeniowych.

Uważam jednak, że dobrą praktyką może być, jeśli to możliwe, sprawdzanie sprawdzonych plików w oryginalnych repozytoriach, aby użytkownicy mogli się do nich odwołać w razie potrzeby.

Answer 2

Istnieje doskonała biblioteka checkers, która zapewnia właściwości QuickCheck do sprawdzania przepisów.

Answer 3

Biblioteka eksperymentalny ghc-proofs pozwala na użycie kompilatora do weryfikacji takich ustaw dla Ciebie:

app_law_2 a b (c :: Succs a) = pure (.) <*> a <*> b <*> c 
          === a <*> (b <*> c) 

To działa tylko w nielicznych przypadkach, takich jak ten opisany in my blog post, a najlepiej jest postrzegane jako eksperyment , a nie gotowe narzędzie.