Rozróżnienie fazy

Rozróżnienie fazowe jest właściwością języków programowania, które przestrzegają ścisłego podziału na typy i terminy . Zwięzłą regułę określania, czy rozróżnienie faz jest zachowane w języku, czy nie, zaproponował Luca Cardelli - Jeśli A jest terminem kompilacji, a B jest terminem podrzędnym A, to B musi być również terminem kompilacji.

Większość języków o typie statycznym jest zgodna z zasadą rozróżnienia faz. Jednak niektóre języki ze szczególnie elastycznymi i ekspresyjnymi systemami typów (zwłaszcza języki programowania o typie zależnym ) umożliwiają manipulowanie typami w taki sam sposób, jak zwykłymi terminami. Mogą być przekazywane do funkcji lub zwracane jako wyniki.

Język z rozróżnieniem faz może mieć oddzielne przestrzenie nazw dla typów i zmiennych czasu wykonywania. W kompilatorze optymalizującym rozróżnienie faz wyznacza granicę między wyrażeniami, które można bezpiecznie wymazać .

Teoria

Rozróżnienie faz jest używane w połączeniu ze sprawdzaniem statycznym. Korzystając z systemu opartego na rachunku różniczkowym, rozróżnienie faz eliminuje potrzebę wymuszania logiki liniowej między różnymi typami i warunkami programowania.

Wstęp

Phase Distinction rozróżnia przetwarzanie wykonywane w czasie kompilacji od przetwarzania wykonywanego w czasie wykonywania.

Rozważ prosty język z terminami:

t ::= prawda | fałsz | x | Xx : T . t | tt | jeśli t to t inaczej t

i rodzaje:

T ::= Bool | T -> T

Zwróć uwagę, jak różnią się typy i terminy. W czasie kompilacji typy są używane do sprawdzania poprawności warunków. Jednak typy nie odgrywają żadnej roli w czasie wykonywania.