Typ wyjątkowości
| Systemy typów |
|---|
| Pojęcia ogólne |
| Główne kategorie |
| Kategorie drugorzędne |
W informatyce unikalny typ gwarantuje, że obiekt jest używany w sposób jednowątkowy , z co najwyżej jednym odwołaniem do niego. Jeśli wartość ma unikalny typ, zastosowaną do niej funkcję można zoptymalizować , aby aktualizowała wartość na miejscu w kodzie obiektowym . Takie aktualizacje na miejscu poprawiają wydajność języków funkcjonalnych przy jednoczesnym zachowaniu przejrzystości referencyjnej . Unikalne typy mogą być również używane do integracji programowania funkcjonalnego i imperatywnego.
Wstęp
Typowanie unikalności najlepiej wyjaśnić na przykładzie. Rozważmy funkcję readLine , która odczytuje następny wiersz tekstu z podanego pliku:
funkcja readLine(File f) zwraca wiersz zwrotny String gdzie String line = doImperativeReadLineSystemCall(f) end end Teraz doImperativeReadLineSystemCall odczytuje następny wiersz z pliku przy użyciu wywołania systemowego na poziomie systemu operacyjnego , którego efektem ubocznym jest zmiana bieżącej pozycji w pliku. Ale to narusza przejrzystość referencyjną, ponieważ wywołanie go wiele razy z tym samym argumentem zwróci różne wyniki za każdym razem, gdy bieżąca pozycja w pliku zostanie przesunięta. To z kolei powoduje, że readLine narusza przezroczystość referencyjną, ponieważ wywołuje funkcję doImperativeReadLineSystemCall .
Jednak używając unikalności typowania, możemy skonstruować nową wersję readLine , która jest przezroczysta referencyjnie, mimo że jest zbudowana na funkcji, która nie jest przezroczysta referencyjnie:
funkcja readLine2(unique File f) zwraca (unique File, String) return (różneF, line) gdzie String line = doImperativeReadLineSystemCall(f) File differentF = newFileFromExistingFile(f) end end Deklaracja unique określa, że typ f jest unikalny; to znaczy, że osoba wywołująca readLine2 po powrocie readLine2 nie może już nigdy więcej odwołać się do f , a to ograniczenie jest wymuszane przez typ system . A ponieważ readLine2 nie zwraca f samo w sobie, ale raczej nowy, inny obiekt pliku differentF , oznacza to, że nie można wywołać readLine2 z f ponownie jako argument, zachowując w ten sposób przejrzystość referencyjną, jednocześnie pozwalając na wystąpienie skutków ubocznych.
Języki programowania
Typy unikalności są implementowane w funkcjonalnych językach programowania, takich jak Clean , Mercury , SAC i Idris . Są czasami używane do wykonywania we/wy w językach funkcjonalnych zamiast monad .
Opracowano rozszerzenie kompilatora dla języka programowania Scala , które wykorzystuje adnotacje do obsługi wyjątkowości w kontekście przekazywania komunikatów między aktorami.
Związek z pisaniem liniowym
Unikalny typ jest bardzo podobny do typu liniowego , do tego stopnia, że terminy te są często używane zamiennie, ale w rzeczywistości istnieje różnica: rzeczywiste typowanie liniowe pozwala na przekształcenie wartości nieliniowej w postać liniową, przy jednoczesnym zachowaniu liczne odniesienia do niego. Unikalność gwarantuje, że wartość nie ma innych odniesień do niej, podczas gdy liniowość gwarantuje, że nie można już poczynić żadnych odniesień do wartości.
Liniowość i niepowtarzalność można postrzegać jako szczególnie różne w odniesieniu do modalności nieliniowości i niejednoznaczności, ale można je również ujednolicić w jednym systemie typów.