Związek między umowami a pisaniem zależnym

Czytałem kilka artykułów na temat typów zależnych i umów programowych. Z większości tego, co przeczytałem, wydaje się, że kontrakty są sprawdzane dynamicznie, a typy zależne sprawdzane statycznie.

Było kilka dokumentów, które skłoniły mnie do myślenia, że ​​możliwe są kontrakty częściowo sprawdzane statycznie:

• Hybrid Type Checking (C. Flanagan - 2006)
• Unifying Hybrid Typs and Contracts (J. Groński, C. Flanagan - 2007)

W związku z tym wydaje się, że nakładają się na siebie znaczne zakresy, a moja kategoryzacja kontraktów względem rodzajów zależnych zaczyna znikać.

Czy w obu koncepcjach brakuje czegoś głębszego? Czy te naprawdę rozmyte kategorie reprezentują tę samą koncepcję?

Na poziomie praktycznym umowy są twierdzeniami. Pozwalają sprawdzić (bez kwantyfikatora) właściwości poszczególnych wykonań programu. Kluczową ideą leżącą u podstaw sprawdzania umowy jest idea winy - w zasadzie chcesz wiedzieć, kto ponosi winę za naruszenie umowy. Może to być implementacja (która nie oblicza obiecanej wartości) lub obiekt wywołujący (który przekazał funkcji niewłaściwy rodzaj wartości).

Kluczowym wnioskiem jest to, że można śledzić winę za pomocą tej samej maszynerii, co pary osadzania i projekcji w konstrukcji odwrotnego limitu teorii domen. Zasadniczo przełączasz się z pracy z asercjami na pracę z parami asercji, z których jedna obwinia kontekst programu, a druga obwinia program. Następnie pozwala to zawijać funkcje wyższego rzędu kontraktami, ponieważ można modelować kontrawariancję przestrzeni funkcji, zamieniając parę asercji. (Zobacz na przykład artykuł Nicka Bentona „Cofanie pisania dynamicznego” ).

Typy zależne to typy. Typy określają zasady stwierdzania, czy niektóre programy są dopuszczalne, czy nie. W rezultacie nie obejmują one pojęcia winy, ponieważ ich funkcją jest przede wszystkim zapobieganie istnieniu źle działających programów. Nie można winić za to, że tylko dobrze sformułowane programy są nawet wypowiedziami gramatycznymi. Pragmatycznie oznacza to, że bardzo łatwo jest używać typów zależnych, aby mówić o właściwościach terminów z kwantyfikatorami (np. Że funkcja działa dla wszystkich danych wejściowych).

Te dwa widoki nie są takie same, ale są ze sobą powiązane. Zasadniczo chodzi o to, że w umowach zaczynamy od uniwersalnej dziedziny wartości i używamy kontraktów do obniżania wartości. Ale kiedy używamy typów, staramy się z góry określić mniejsze domeny wartości (z pożądaną właściwością). Możemy więc połączyć te dwa za pomocą rodzin relacji ukierunkowanych na typ (tj. Relacji logicznych). Na przykład zobacz najnowszą „Winy za wszystkich” Ahmeda, Findlera, Siek i Wadlera lub „Znaczenie typów: od wewnętrznej do zewnętrznej semantyki” Reynoldsa .

(Dość abstrakcyjny) problem, jaki atakują zarówno typy, jak i kontrakty, brzmi „Jak zapewnić, aby programy miały określone właściwości?”. Istnieje nieodłączne napięcie między zdolnością wyrażania szerszej klasy właściwości a możliwością sprawdzania, czy program ma właściwość, czy nie. Systemy typów zazwyczaj zapewniają bardzo specyficzną właściwość (program nigdy nie ulega awarii w określony sposób) i mają algorytm sprawdzania typu. Z drugiej strony, kontrakty pozwalają na określenie bardzo szerokiego zakresu właściwości (powiedzmy, wynik tego programu jest liczbą pierwszą), ale nie zawierają algorytmu sprawdzającego.

Niemniej jednak fakt, że nie ma algorytmu sprawdzania kontraktów (który zawsze działa) nie oznacza, że ​​nie ma algorytmów sprawdzania prawie kontraktów (które zwykle działają w praktyce). Polecam zajrzeć do Spec # i wtyczki Jessie Frama-C . Oba działają, wyrażając „ten program przestrzega tej umowy” jako oświadczenie w logice pierwszego rzędu poprzez wygenerowanie warunków weryfikacji , a następnie pytając SMTsolver, aby przejść, spróbuj znaleźć dowód. Jeśli solver nie znajdzie dowodu, to albo program jest zły, albo, cóż, solver nie znalazł dowodu, który istnieje. (Dlatego jest to algorytm „prawie” sprawdzania kontraktu.) Istnieją również narzędzia oparte na symbolicznym wykonywaniu, co oznacza z grubsza, że ​​„ten program przestrzega tej umowy” jest wyrażony jako wiązka zdań (w pewnej logice). Zobacz na przykład jStar .

Praca Flanagana stara się czerpać to, co najlepsze z obu światów, abyś mógł szybko sprawdzić właściwości podobne do typu, a następnie zająć się resztą. Nie znam się na typach hybrydowych, ale pamiętam, jak autor powiedział, że jego motywacją było wymyślenie rozwiązania, które wymaga mniej adnotacji (niż poprzednia praca nad ESC / Java). W pewnym sensie istnieje jednak pewna luźna integracja między typami i umowami w ESC / Java (i Spec #): podczas sprawdzania umów solver otrzymuje informację, że sprawdzenie typu powiodło się, aby mógł zobaczyć te informacje.

Kontrakty można sprawdzać statycznie. Jeśli spojrzysz na starą pracę Dany Xu nad ESC / Haskell , była ona w stanie wdrożyć pełne sprawdzanie kontraktu w czasie kompilacji, opierając się tylko na twierdzeniu o arytmetyki. Zakończenie jest rozwiązywane przez prosty limit głębokości, jeśli dobrze pamiętam:

Zarówno kontrakty, jak i typy pozwalają reprezentować specyfikacje funkcji w stylu Hoare'a (warunek przed / po). Oba można sprawdzić statycznie w czasie kompilacji lub dynamicznie w czasie wykonywania.

Zależne typy pozwalają zakodować bardzo szeroki zakres właściwości w systemie typów, rodzaj właściwości, których oczekują programiści. Wynika to z faktu, że mogą zależeć od wartości typu. Typy zależne mają tendencję do sprawdzania statycznego, chociaż uważam, że cytowane artykuły dotyczą alternatywnych podejść.

Ostatecznie różnica jest niewielka. Myślę, że bardziej zależne typy są logiką, w której można wyrażać specyfikacje, podczas gdy kontrakty są metodologią programowania, w której wyrażasz specyfikacje.