What is a fully understandable language? and the limitations of such a language?

Question

As far as I know, any programming language that does not require writing type annotations in the source when writing a function or module, and if this piece of code is "correct for input", the compiler will output the types and compilation code. is there even more?

is (is) such language (s)? if so, are there any restrictions on his type system?

Update 1: Just to be really understandable, I am asking about a statically typed, fully printed language, and not a dynamically typed programming language.

Answer 1

The limitation of the full type inference is that it does not work with many functions of the extended type system. As an example, consider Haskell and OCaml. Both of these languages ​​are almost completely inferred by type, but have some functions that can interfere with type inference.

---

In Haskell, he introduces classes in conjunction with polymorphic return types:

readAndPrint str = print (read "asd") 

Here, read is a function of type Read a => String -> a , which means "for any type a that supports a class of type read , the read function can take a String and return a Therefore, if f is a method that accepts int, I can write f (read "123") and it will convert "123" to Int 123 and call f with it. He knows that he must convert the string to Int because f takes Int. If f took the list of ints, he would try to convert the string Ints. No problem.

But for the readAndPrint function above, this approach does not work. The problem here is that print can accept an argument of any type that can be printed (it is any type that supports the Show class). Thus, the compiler does not know if you want to convert the string to int, or the list of ints, or anything else that can be printed. Therefore, in such cases, you need to add type annotations.

---

In OCaml, a problematic function is polymorphic functions in classes: if you define a function that takes an object as an argument and calls a method for that object, the compiler will infer a monomorphic type for this method. For example:

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

Here, the compiler concludes that obj must be an instance of a class that has a method called meth type int -> int , that is, a method that accepts Int and returns Int. Now you can define a group of classes that have such a method and pass instances of this class as arguments to f . No problems.

The problem arises if you define a class with a method of type 'a. 'a -> int 'a. 'a -> int , that is, a method that can take an argument of any type and return int. You cannot pass an object of this class as an argument to f because it does not match the inferred type. If you want f take such an object as its argument, the only way is to add type annotation to f .

---

Thus, these were examples of languages ​​that are almost completely inferred by type, and cases when they are not. If you remove problematic features from these languages, they will be fully printed.

Therefore, the basic dialects of ML without such advanced features are completely inferred in type. For example, I assume that Caml Light is completely out of order, since it is mostly OCaml without classes (however, in fact, I don’t know the language, so it’s just a guess).

Answer 2

What is type inference?

Historically, type inference (or type reconstruction) has meant that all types in a program can be inferred without requiring mainly annotations of an explicit type. However, in recent years, the main thesis in the programming language has become the designation of even the most trivial forms of type inference from bottom to top as "type inference" (for example, new auto declarations in C ++ 11). So people started adding “full” to refer to the “real” thing.

What is full type inference?

There is a wide range to what extent a language can output types, and in practice, almost no language supports the "full" type of output in the strict sense (basic ML is the only example). But the main distinguishing factor is whether types can be obtained for bindings that do not have a “definition” attached to them; in particular, function parameters. If you can write, say

 f(x) = x + 1 

and the type system determines that f eg is of type Int → Int, then it makes sense to call this type of output. Moreover, we are talking about the conclusion of the polymorphic type, when, for example,

 g(x) = x 

assigned the generic type & forall; (t) t → t automatically.

Type inference was invented in the context of simply typed lambda calculus, and polymorphic type inference (the so-called inference of the Hindley / Milner type, invented in the 1970s) is a claim to the glory of the ML language family (Standard ML, OCaml, and possibly Haskell )

What are the limits of full type inference?

Core ML has the luxury of a "complete" polymorphic type output. But it depends on certain limitations of polymorphism in its type system. In particular, only definitions can be general, not function arguments. I.e

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

works just fine because id can be given by a polymorphic type when the definition is known. But

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

does not set validation in ML, because id cannot be polymorphic as an argument to a function. In other words, the type system allows polymorphic types, such as & forall; (t) t → t, but not the so-called polymorphic types of a higher rank, such as (? forall; (t) t → t) → Bool, where the polymorphic values ​​are used in a first-class manner (which, to be understood, allows even very few explicitly typed languages).

The polymorphic lambda calculus (also called "System F"), which is explicitly introduced, allows the latter to be used. But the standard result of type theory is that type reconstruction for the complete system F is unsolvable. Hindley / Milner falls into the sweet spot of a slightly less expressive type system for which type reconstruction is still solvable.

There are more advanced type system functions that also make complete type reconstruction impossible. And there are others who keep it solvable, but still make it impracticable, for example. the presence of ad-hoc overload or subtyping, as this leads to a combinatorial explosion.

Answer 3

Another limitation is higher rated types. For example, the following program does not check type in languages ​​with outputs of type ML:

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

The type controller can assign f the type [Char] → [Char] or [Int] → [Int], but not for all a. [a] → [a]. There is no way to fix this in ML, Ocaml, and F #, since you can't even write higher rank types.

But Haskell (via the GHC extension) and Frege support higher rank types. But since only checking the type of a higher rank is possible (as opposed to outputting a higher rank), the programmer must give a type annotation, although, for example:

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