co to jest w pełni sformułowany język? i ograniczenia takiego języka?

Question

O ile mi wiadomo, każdy język programowania, który nie wymaga, aby napisać typu adnotacji w źródle podczas pisania funkcji lub moduł i jeśli ten fragment kodu jest „typu poprawne”, kompilator będzie wnioskować typy i kompiluje kod. czy jest w tym coś więcej?

jest (są) istnieje taki język (s)? jeśli tak, czy istnieją jakiekolwiek ograniczenia dotyczące jego systemu typu?

Aktualizacja 1: Wystarczy być naprawdę jasne, pytam o statycznie wpisane, w pełni wpisać-wywnioskować języka programowania nie dynamicznie wpisywanych języka programowania.

Answer 1

Ograniczenie pełnego typu wnioskowania jest to, że nie działa z wielu zaawansowanych funkcji systemowych typu. Jako przykład rozważ Haskella i OCamla. Oba te języki są w pełni typu wywnioskowane, ale mają pewne funkcje, które mogą zakłócać wnioskowanie o typie.

---

Haskell IT klasy typu w połączeniu z polimorficznych typów obie:

readAndPrint str = print (read "asd") 

tutaj read jest funkcją typu Read a => String -> a, co oznacza „dla każdego typu a obsługującej klasy typu Read wyboru funkcji read można wziąć String i zwracają a. Więc jeśli f jest metodą, która zajmuje int, mogę napisać f (read "123") i będzie konwertować „123” do Int 123 i wezwać f z to. Wie, że powinien przekonwertować ciąg na Int, ponieważ f przyjmuje wartość Int. Jeśli f wziął listę int, spróbowałby zamiast tego przekonwertować ciąg na listę Ints. Nie ma problemu.

Ale funkcja readAndPrint powyżej tego podejścia nie działa. Problem polega na tym, że print może argument dowolnego typu, które można wydrukować (czyli każdy typ, który wspiera Show typeclass). Kompilator nie ma więc możliwości sprawdzenia, czy chcesz przekonwertować ciąg znaków na int, czy listę int, lub cokolwiek innego, co można wydrukować. W takich przypadkach należy dodać adnotacje typu.

---

W SML problematyczne cechą jest polimorficzne funkcje w klasach: Jeśli zdefiniować funkcję, która pobiera jako argument obiekt i wywołuje metodę na tym obiekcie, kompilator będzie wyprowadzić jednokształtnym typ dla tej metody. Na przykład:

let f obj = obj#meth 23 + obj#meth 42 

Tutaj kompilator będzie wywnioskować, że obj musi być instancją klasy, która ma metodę nazwie meth typu int -> int, czyli metodę, która zajmuje int i zwraca int. Możesz teraz zdefiniować grupę klas, które mają taką metodę i przekazać instancje tej klasy jako argumenty do f. Nie ma problemu.

Problem występuje, jeśli zdefiniujesz klasę metodą typu 'a. 'a -> int, tj. Metodą, która może przyjmować argument dowolnego typu i zwracać wartość int. Nie można przekazać obiektu tej klasy jako argumentu do f, ponieważ nie pasuje on do wywnioskowanego typu. Jeśli chcesz, aby f wziął taki obiekt jako jego argument, jedynym sposobem jest dodanie adnotacji typu do f.

---

Tak więc były to przykłady języków, które są w pełni typu wywnioskować i przypadków, w których nie są. Jeśli usuniesz problematyczne funkcje z tych języków, zostaną one w pełni sprecyzowane.

W konsekwencji podstawowe dialekty ML bez takich zaawansowanych funkcji są w pełni typu wywnioskowane. Na przykład zakładam, że Caml Light jest w pełni typu wywnioskować, ponieważ jest to w zasadzie OCaml bez klas (jednak tak naprawdę nie znam języka, więc to tylko założenie).

Answer 2

Co to jest wnioskowanie typu?

Historycznie wnioskowanie typu (lub typu rekonstrukcji) oznacza, że ​​wszystkie typów w programie może być uzyskane bez konieczności zasadniczo dowolnego wyraźny typu opisów. Jednak w ostatnich latach w głównym nurcie języka programowania stało się modne, aby oznaczyć nawet najbardziej banalne formy dedukcji typu "od dołu do dołu" jako "wnioskowanie typu" (np. Nowe deklaracje C++ 11). Więc ludzie zaczęli dodawać "pełne", aby odnieść się do "prawdziwej" rzeczy.

Co to jest pełna propozycja typu?

Istnieje szerokie spektrum tego, w jakim stopniu język może wnioskować o typach, aw praktyce prawie żaden język nie obsługuje "pełnego" typu wnioskowania typu w ścisłym tego słowa znaczeniu (rdzeń ML jest jedynym przykładem). Ale głównym czynnikiem wyróżniającym jest to, czy można uzyskać typy dla powiązań, które nie mają do nich "definicji", w szczególności parametrów funkcji. Jeśli możesz napisać, powiedzmy,

f(x) = x + 1 

i system typów odczytuje, że np. ma typ Int → Int, wtedy sensowne jest wywoływanie tego typu wnioskowania. Ponadto, mówimy o polimorficzne typu wywnioskować kiedy, na przykład,

g(x) = x 

przypisany jest ogólny typ i Forall; (t) t → t automatycznie.

Wnioskowanie o typ zostało wymyślone w kontekście prosto napisanego rachunku lambda, a wnioskowanie o typie polimorficznym (zwane również wnioskiem typu Hindley/Milner, wynalezione w latach 70. XX wieku) jest pretekstem do uznania rodziny języków ML (Standard ML , OCaml i prawdopodobnie Haskell).

Jakie są ograniczenia pełnego wnioskowania typu?

Core ML ma luksus "pełnego" polimorficznego typu wnioskowania. Ale zależy to od pewnych ograniczeń polimorfizmu w jego systemie typów. W szczególności tylko definicje mogą być ogólne, a nie argumenty funkcyjne. Oznacza to, że

id(x) = x; 
id(5); 
id(True) 

działa dobrze, ponieważ id można podać rodzaj polimorficzny gdy definicja jest znana. Ale

f(id) = (id(5); id(True)) 

nie typ kontroli w ML, ponieważ id nie może być polimorficzny jako argument funkcji.Innymi słowy, system typów dopuszcza typy polimorficzne, jak i wszystkie, ale nie tak zwane wyższego rzędu typy polimorficzne, takie jak (i ​​all (t) t → t) → Bool, gdzie stosuje się wartości polimorficzne w sposób pierwszorzędny (który, by to wyjaśnić, pozwala na to nawet bardzo niewiele języków jawnie wpisanych).

Polimorficzny współczynnik lambda (zwany również "Systemem F"), który jest jawnie wpisany, pozwala na to ostatnie. Ale jest to standardowy wynik w teorii typu, że rekonstrukcja typu dla pełnego Systemu F jest nierozstrzygalna. Hindley/Milner uderza słodką plamę o nieco mniej ekspresyjnym systemie typu, dla którego rekonstrukcja typu jest wciąż rozstrzygająca.

Istnieją bardziej zaawansowane funkcje systemowe, które powodują, że pełna rekonstrukcja typu jest nierozstrzygalna. Są też inne, które decydują o tym, ale wciąż są niewykonalne, np. obecność przeciążenia lub podporządkowania ad-hoc, ponieważ prowadzi to do kombinatorycznej eksplozji.

Answer 3

Kolejnym ograniczeniem są wyższe typy w rankingu. Na przykład, następujący program robi nie typecheck w językach z ML typu styl wnioskowania:

foo = let bar f = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse 

Kontrolujący typu można przypisać do f rodzaj [Char] -> [Char] lub [Int] -> [Int], ale nie całkiem. [A] -> [a]. W ML, Ocaml i F # nie ma sposobu, aby to naprawić, ponieważ nie można nawet pisać o wyższych typach rang.

Ale Haskell (przez rozszerzenie GHC) i Frege obsługują typy wyższego rzędu. Ale ponieważ tylko wyższy stopień kontroli typu (w przeciwieństwie do wyższej rangi typu wnioskowanie) jest możliwe, programista ma obowiązek podać typ adnotacji, choć na przykład:

foo = let bar (f :: forall a.[a]->[a]) = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse