W pracy miałem za zadanie wnioskować o pewnych typach informacji o dynamicznym języku. Przepisuję sekwencje instrukcji na letwyrażenia zagnieżdżone , tak jak poniżej:
return x; Z => x
var x; Z => let x = undefined in Z
x = y; Z => let x = y in Z
if x then T else F; Z => if x then { T; Z } else { F; Z }
Ponieważ zaczynam od ogólnych informacji o typie i staram się wydedukować bardziej szczegółowe typy, naturalnym wyborem są typy wyrafinowania. Na przykład operator warunkowy zwraca sumę typów jego prawdziwych i fałszywych gałęzi. W prostych przypadkach działa bardzo dobrze.
Jednak wpadłem na przeszkodę, próbując wywnioskować, co następuje:
function g(f) {
var x;
x = f(3);
return f(x);
}
Który jest przepisany na:
\f.
let x = undefined in
let x = f 3 in
f x
HM wywnioskuje a w konsekwencji . Rzeczywisty typ, który chcę móc wywnioskować, to:
Już używam zależności funkcjonalnych do rozwiązania typu przeciążonego +operatora, więc doszedłem do wniosku, że naturalnym rozwiązaniem było użycie ich do rozwiązania typu fwewnątrz g. Oznacza to, że typy fwszystkich jego aplikacji razem jednoznacznie określają typ g. Jednak, jak się okazuje, fundeps nie nadają się zbyt dobrze do zmiennej liczby typów źródeł.
W każdym razie wzajemne oddziaływanie polimorfizmu i typowania udoskonalonego jest problematyczne. Czy brakuje mi lepszego podejścia? Obecnie trawię „Typy wyrafinowania dla ML” i doceniłbym więcej literatury lub innych wskazówek.
źródło