什么是完全类型推断的语言？这种语言的限制？ [英] what is a fully type-inferred language? and limitations of such language?

问题描述

据我所知，编写函数或模块时不需要在源代码中写入类型注释的任何编程语言，如果该代码块是类型正确的，编译器将推断类型并编译代码。还有更多吗？

是否有这样的语言？如果是的话，是否有任何限制它的类型系统？

更新1：
只是确实清楚，我问的是一种静态类型的，完全类型推断的编程语言，而不是一种动态类型的编程语言。

解决方案

它不适用于许多高级类型的系统功能。以Haskell和OCaml为例。这两种语言几乎都是完全类型推断，但有一些功能会干扰类型推断。

---

在Haskell中，它的类型类与多态返回类型结合在一起：

  readAndPrint str = print（readasd）
  

这里 read 是类型阅读a =>字符串 - >一个，这意味着对于任何类型 a ，它支持类型类读取函数读取可以接收字符串并返回 a 。如果 f 是一个接受int的方法，我可以写 f（读取123），它会转换123给Int 123并用它调用 f 它知道它应该将字符串转换为Int，因为 f



但是对于 readAndPrint 函数不起作用。这里的问题是 print 可以接受任何类型的参数（这是支持 Show typeclass）的任何类型，所以编译器无法知道您是要将字符串转换为int还是列表ints或其他可以打印的东西，所以在这种情况下，你需要添加t在OCaml中，有问题的特性是类中的多态函数：如果你定义了一个函数，它将一个对象作为一个对象它的参数并在该对象上调用一个方法，编译器会推断该方法的单形类型。例如：



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

这里编译器会推断出 obj 必须是一个具有方法的类的实例命名为 meth 类型为 int - > int ，即采用Int并返回Int的方法。您现在可以定义一堆具有此类方法的类，并将该类的实例作为参数传递给 f 。没问题。



如果您使用类型'a的方法定义类，则会发生此问题。 'a - > int ，即可以接受任何类型参数并返回int的方法。您不能将该类的对象作为参数传递给 f ，因为它与推断的类型不匹配。如果你想让 f 把这样一个对象作为它的参数，唯一的方法就是添加一个类型注释到 f 。



---

所以这些都是几乎完全推断的语言的例子，以及它们不是的例子。如果您从这些语言中删除了有问题的功能，那么它们将被完全推断出来。

因此，没有这些高级功能的ML的基本方言是完全类型推断的。例如，我假设Caml Light是完全类型推断的，因为它基本上是OCaml，没有类（但是我​​实际上并不知道语言，所以这只是一个假设）。

As far as I know,any programming language which doesn't require to write type annotations in the source while writing a function or module and if that chunk of code is "type-correct" , compiler will infer the types and compiles the code. is there more to it?

is(are) there a such language(s)? if yes are there any limitations on it's type system?

Update 1: Just to be really clear , I am asking about a statically typed,fully type-inferred programming language not a dynamically typed programming language.

解决方案

The limitation of full type inference is that it doesn't work with many advanced type system features. As an example consider Haskell and OCaml. Both of these languages are almost fully type inferred, but have some features that can interfere with type inference.

---

In Haskell it's type classes combined 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 the type class Read the function read can take a String and return an a. So if f is a method that takes an int, I can write f (read "123") and it will convert "123" to the Int 123 and call f with it. It knows that it should convert the string to an Int because f takes an Int. If f took a list of ints, it would try to convert the string to a list of Ints instead. No problem.

But for the readAndPrint function above that approach does not work. The problem here is that print can take an argument of any type that can be printed (that is any type that supports the Show typeclass). So there's no way for the compiler to know whether you want to convert the string to an int, or a list of ints, or anything else that can be printed. So in cases like this you need to add type annotations.

---

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

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

Here the compiler will infer that obj must be an instance of a class that has a method named meth of type int -> int, i.e. a method that takes an Int and returns an Int. You can now define a bunch of classes that have such a method and pass instances of that class as arguments to f. No problem.

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

---

So those were examples of languages that are almost fully type inferred and of cases where they're not. If you'd remove the problematic features from those languages, they'd be fully type inferred.

Consequently basic dialects of ML without such advanced features are fully type inferred. For instance I assume that Caml Light is fully type inferred since it's basically OCaml without classes (however I don't actually know the language, so that's just an assumption).

这篇关于什么是完全类型推断的语言？这种语言的限制？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！