Co to jest pisanie zależne?

Czy ktoś może mi wyjaśnić pisanie na klawiaturze zależnej? Mam niewielkie doświadczenie w języku Haskell, Cayenne, Epigram lub innych językach funkcjonalnych, więc im prostszych terminów użyjesz, tym bardziej to docenię!

Rozważ to: we wszystkich przyzwoitych językach programowania możesz pisać funkcje, np

def f(arg) = result

Tutaj fprzyjmuje wartość argi oblicza wartość result. Jest to funkcja od wartości do wartości.

Teraz niektóre języki umożliwiają definiowanie wartości polimorficznych (czyli ogólnych):

def empty<T> = new List<T>()

Tutaj emptyprzyjmuje typ Ti oblicza wartość. Jest to funkcja od typów do wartości.

Zwykle możesz również mieć definicje typów ogólnych:

type Matrix<T> = List<List<T>>

Ta definicja przyjmuje typ i zwraca typ. Można go postrzegać jako funkcję od typów do typów.

To tyle, jeśli chodzi o to, co oferują zwykłe języki. Język nazywany jest typem zależnym, jeśli oferuje również czwartą możliwość, mianowicie definiowanie funkcji od wartości do typów. Innymi słowy, parametryzacja definicji typu względem wartości:

type BoundedInt(n) = {i:Int | i<=n}

Niektóre języki głównego nurtu mają jakąś fałszywą formę, której nie należy mylić. Np. W C ++ szablony mogą przyjmować wartości jako parametry, ale po zastosowaniu muszą być stałymi czasu kompilacji. Inaczej jest w przypadku prawdziwie zależnego języka. Na przykład mógłbym użyć powyższego typu w ten sposób:

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

W tym przypadku typ wyniku funkcji zależy od rzeczywistej wartości argumentu j, a więc od terminologii.

Zależne typy umożliwiają wyeliminowanie większego zestawu błędów logicznych w czasie kompilacji . Aby to zilustrować, rozważ następującą specyfikację funkcji f:

Funkcja fmusi przyjmować tylko parzyste liczby całkowite jako dane wejściowe.

Bez typów zależnych możesz zrobić coś takiego:

def f(n: Integer) := {
  if  n mod 2 != 0 then 
    throw RuntimeException
  else
    // do something with n
}

W tym przypadku kompilator nie może wykryć, czy nrzeczywiście jest parzysty, to znaczy z punktu widzenia kompilatora następujące wyrażenie jest w porządku:

f(1)    // compiles OK despite being a logic error!

Ten program uruchomi się, a następnie zgłosi wyjątek w czasie wykonywania, co oznacza, że ​​program ma błąd logiczny.

Teraz typy zależne pozwalają na znacznie większą ekspresję i pozwolą napisać coś takiego:

def f(n: {n: Integer | n mod 2 == 0}) := {
  // do something with n
}

Tutaj njest zależny typ {n: Integer | n mod 2 == 0}. Pomocne może być przeczytanie tego na głos jako

n jest członkiem zbioru liczb całkowitych, tak że każda liczba całkowita jest podzielna przez 2.

W tym przypadku kompilator wykryłby w czasie kompilacji błąd logiczny, do którego przekazałeś nieparzystą liczbę fi uniemożliwiłby wykonanie programu w pierwszej kolejności:

f(1)    // compiler error

Oto ilustrujący przykład wykorzystujący typy zależne od ścieżki Scala, w jaki sposób możemy próbować zaimplementować funkcję fspełniającą takie wymaganie:

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

Kluczem jest zwrócenie uwagi na to, jak wartość npojawia się w typie wartości, proofa mianowicie n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

Mówimy, że typ n.IsEven.type zależy od wartości, n stąd termin typy zależne .

Jeśli znasz C ++, możesz łatwo podać motywujący przykład:

Powiedzmy, że mamy jakiś typ kontenera i jego dwie instancje

typedef std::map<int,int> IIMap;
IIMap foo;
IIMap bar;

i rozważ ten fragment kodu (możesz założyć, że foo nie jest puste):

IIMap::iterator i = foo.begin();
bar.erase(i);

Jest to oczywiste śmieci (i prawdopodobnie psuje struktury danych), ale sprawdzanie typu będzie dobre, ponieważ „iterator do foo” i „iterator do baru” są tego samego typu IIMap::iterator, nawet jeśli są całkowicie niekompatybilne semantycznie.

Problem w tym, że typ iteratora nie powinien zależeć tylko od typu kontenera, ale w rzeczywistości od obiektu kontenera , czyli powinien być „niestatycznym typem składowym”:

foo.iterator i = foo.begin();
bar.erase(i);  // ERROR: bar.iterator argument expected

Taka cecha, możliwość wyrażenia typu (foo.iterator) zależnego od terminu (foo), jest dokładnie tym, co oznacza typ zależny.

Powodem, dla którego rzadko widzisz tę funkcję, jest to, że otwiera ona dużą puszkę robaków: nagle kończysz w sytuacjach, w których, aby sprawdzić w czasie kompilacji, czy dwa typy są takie same, musisz udowodnić dwa wyrażenia są równoważne (zawsze dają tę samą wartość w czasie wykonywania). W rezultacie, jeśli porównasz listę języków zależnie wpisywanych w Wikipedii z listą potwierdzających twierdzenia , możesz zauważyć podejrzane podobieństwo. ;-)

Cytując książkę Typy i języki programowania (30.5):

Znaczna część tej książki poświęcona była formalizowaniu różnego rodzaju mechanizmów abstrakcji. W prostym typie rachunku lambda sformalizowaliśmy operację przyjęcia terminu i wyodrębnienia podterminu, uzyskując funkcję, która może być później utworzona przez zastosowanie jej do różnych terminów. W System Frozważaliśmy operację pobrania terminu i wyodrębnienia typu, uzyskując termin, który można utworzyć, stosując go do różnych typów. Wλω, podsumowaliśmy mechanizmy prostego rachunku lambda „jeden poziom wyżej”, pobierając typ i wyodrębniając podwyrażenie w celu uzyskania operatora typu, który można później utworzyć, stosując go do różnych typów. Dogodnym sposobem myślenia o wszystkich tych formach abstrakcji są rodziny wyrażeń indeksowane innymi wyrażeniami. Zwykła abstrakcja lambda λx:T1.t2to rodzina terminów [x -> s]t1indeksowanych według terminów s. Podobnie abstrakcja typu λX::K1.t2to rodzina terminów indeksowanych według typów, a operator typu to rodzina typów indeksowanych według typów.

• λx:T1.t2 rodzina terminów indeksowanych według terminów

• λX::K1.t2 rodzina terminów indeksowanych według typów

• λX::K1.T2 rodzina typów indeksowana według typów

Patrząc na tę listę, widać wyraźnie, że istnieje jedna możliwość, której jeszcze nie rozważaliśmy: rodziny typów indeksowanych według terminów. Ta forma abstrakcji była również obszernie badana w rubryce typów zależnych.