> Takové jazyky rozhodně neexistují, už proto, že stoprocentně statická typová kontrola je ekvivalentní problému zastavení (a je tedy nerozhodnutelná) :-)
Ale já nikde nepsal, že ten jazyk bude ekvivalentní částečně rekurzivním funkcím :-) Ono to často ani není potřeba a stačí obecně rekurzivní funkce.
Podívejte se třeba na jazyk Epigram nebo Agda, to jsou staticky typované jazyky (a existují i další). Navíc je typový systém tak silný, že umožňuje kódovat libovolné výroky z predikátové logiky, takže když vhodně zapíšete typy, tak vám kompilace zaručí parciálně korektní program (vzhledem k typům). Epigram dovolí jen obecně rek. funkce a Agda zase umí kontrolovat to, že program skončí (resp. když to nevidí, tak vás varuje abyste program mohl přepsat tak, že to bude vidět; je pravda, že tam se ta konečnost nevynucuje).
> Takže staticky typované jazyky samozřejmě mají dynamickou typovou kontrolu, a označují se za staticky typované právě proto, že mají i tu statickou.
Tahle definice je dost častá, ale přijde mi divná. Představte si, že budu v jazyce provádět drobnou statickou kontrolu, že když uvidím dvě konstanty a mezi nimi operátor +, tak zahlásím chybu pokud oboje nejsou čísla, tedy už provádím statickou kontrolu typů. Znamená to, že jazyk je staticky typovaný?
