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ę!
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ę!
Odpowiedzi:
Rozważ to: we wszystkich przyzwoitych językach programowania możesz pisać funkcje, np
def f(arg) = result
Tutaj f
przyjmuje wartość arg
i 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 empty
przyjmuje typ T
i 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.
BoundedInt
przykład nie jest w rzeczywistości typem uściślenia? To jest „całkiem blisko”, ale nie jest to dokładnie ten rodzaj „typów zależnych”, o których np. Idris wspomina jako pierwszy w samouczku dotyczącym składania.
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
f
musi 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 n
rzeczywiś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 n
jest 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ę f
i 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ę f
speł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ść n
pojawia się w typie wartości, proof
a 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 .
f(random())
błąd kompilacji?
f
do jakiegoś wyrażenia wymagałoby od kompilatora (z twoją pomocą lub bez) zapewnienia, że wyrażenie jest zawsze parzyste i nie ma takiego dowodu random()
(ponieważ w rzeczywistości może być dziwne), dlatego f(random())
kompilacja nie powiodłaby się.
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
F
rozważ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.t2
to rodzina terminów[x -> s]t1
indeksowanych według terminóws
. Podobnie abstrakcja typuλX::K1.t2
to 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ówPatrzą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.