Wnioskowanie typu dla instrukcji rozkazujących innych niż przypisanie

W poszukiwaniu artykułów naukowych na temat systemów typów dla języków imperatywnych znajduję rozwiązania tylko dla języka ze zmiennymi odnośnikami, ale bez prawdziwych struktur kontroli imperatywnej, takich jak operatory złożone, pętle lub warunki warunkowe.

Nie jest więc jasne, w jaki sposób można wdrożyć imperatywny język z częściowym wnioskiem o typie, taki jak http://rust-lang.org .

W artykułach nie wspomniano o typach sparametryzowanych, List of aponieważ typy sparametryzowane są trywialnym rozszerzeniem systemu typów Hindleya-Milnera - należy rozszerzyć tylko algorytm unifikacji, a reszta wnioskowania działa bez zmian. Jednak zadań nie można dodawać w trywialny sposób, ponieważ powstają paradoksy, dlatego należy zastosować specjalne techniki, takie jak ograniczenie wartości ML.

Czy możesz polecić jakieś artykuły lub książki opisujące system pisma dla języka z imperatywnymi pętlami, warunkami warunkowymi, IO i instrukcjami złożonymi?

Jeśli szukasz zgrabnego, funkcjonalnego odniesienia do wnioskowania o typie, jestem trochę stronnikiem Gundry, McBride i McKinny z „ Inferencji typów w kontekście ”, choć może to nie być dobrym przewodnikiem po istniejących istniejących implementacjach .

Myślę, że częścią odpowiedzi jest to, że poza ograniczeniem wartości naprawdę nie ma tak dużych trudności w dostosowaniu wnioskowania typu Hindley-Milner do języków imperatywnych: jeśli zdefiniujesz e1; e2jako cukier składniowy (fn _ => e2) e1i zdefiniujesz while e1 do e2jako cukier syntaktyczny dla whiledo e1 (fn () => e2), gdzie whiledojest regularny funkcja rekurencyjna

fun whiledo g f = if g then (f (); whiledo g f) else ();

wtedy wszystko będzie działać poprawnie, w tym wnioskowanie typu.

Jeśli chodzi o ograniczenie wartości będące specjalną techniką, podoba mi się następująca historia; Jestem prawie pewien, że odebrałem go od Karla Crary'ego. Rozważ następujący kod, którego ograniczenie wartości nie pozwoli Ci pisać w ML:

let
   val x: 'a option ref = ref NONE
in
   (x := SOME 5; x := SOME "Hello")  
end

Porównaj go z następującym kodem, który jest całkowicie bezproblemowy:

let
   val x: unit -> 'a option ref = fn () => ref NONE
in
   (x () := SOME 5; x () := SOME "Hello")  
end

Wiemy, co robi drugi przykład: tworzy dwie nowe komórki ref zawierające NONE, następnie wstawia SOME 5pierwszą (an int option ref), a następnie wstawia SOME "Hello"drugą (a string option ref).

xx$\forall \alpha. \mbox{ref}(\mbox{option}(\alpha))$x$\Lambda \alpha. \mbox{ref}[\alpha](\mbox{NONE})$

Sugerowałoby to, że jednym „dobrym” zachowaniem w pierwszym przykładzie jest zachowanie dokładnie tak samo, jak w drugim przykładzie - utworzenie wystąpienia lambda na poziomie typu dwa razy. Za pierwszym razem instancję xz int, który spowoduje, że x [int]do oceny do gospodarstwa komórek odniesienia NONE, a następnie SOME 5. Po raz drugi wystąpienia xz string, które będą rozróżniane x [string]ocenić na ( inaczej! Gospodarstwie) komórek odniesienia NONE, a następnie SOME "Hello". To zachowanie jest „poprawne” (bezpieczne dla typu), ale zdecydowanie nie jest to, czego programista by się spodziewał, i dlatego mamy ograniczenie wartości w ML, aby uniknąć programistów radzących sobie z tym nieoczekiwanym zachowaniem.

Rozprawa doktorska Xaviera Leroya to dobry początek.

Przepraszam, że muszę odpowiedzieć na własne pytanie, ale jest to odniesienie

Propozycja dotycząca standardowego ML , Milner, 1983

Część 6 „Standardowe formy pochodne” obejmuje dość obszerne rozwiązywanie konstrukcji imperatywnych. I jak dotąd jest to najwcześniejsza wzmianka o tych w dużej mierze oczywistych przemianach, jakie udało mi się znaleźć.