许多静态类型语言具有参数多态性。例如在 C# 中可以定义:
T Foo<T>(T x){ return x; }
在调用站点中,您可以执行以下操作:
int y = Foo<int>(3);
这些类型有时也写成这样:
Foo :: forall T. T -> T
我听说有人说“forall 就像类型级别的 lambda 抽象”。所以 Foo 是一个函数,它接受一个类型(例如 int)并产生一个值(例如一个 int -> int 类型的函数)。很多语言推断类型参数,所以可以写成
Foo(3)
而不是 Foo<int>(3)
.假设我们有一个对象
f
类型 forall T. T -> T
.我们可以对这个对象做的首先是传递一个类型Q
。通过写 f<Q>
.然后我们返回一个类型为 Q -> Q
的值.但是,某些 f
是无效的。例如这个 f
:f<int> = (x => x+1)
f<T> = (x => x)
所以如果我们“打电话”
f<int>
然后我们返回一个类型为 int -> int
的值,一般来说,如果我们“调用”f<Q>
然后我们返回一个类型为 Q -> Q
的值,所以这很好。不过一般的理解是这个f
不是 forall T. T -> T
类型的有效事物,因为它会根据你传递的类型做不同的事情。 forall 的想法是明确不允许这样做。另外,如果 forall 是类型级别的 lambda,那么存在什么? (即存在量化)。由于这些原因,似乎 forall 和 exists 并不是真正的“类型级别的 lambda”。但那它们是什么?我意识到这个问题相当模糊,但有人可以帮我解决这个问题吗?A possible explanation is the following:
If we look at logic, quantifiers and lambda are two different things. An example of a quantified expression is:
forall n in Integers: P(n)
So there are two parts to forall: a set to quantify over (e.g. Integers), and a predicate (e.g. P). Forall can be viewed as a higher order function:
forall n in Integers: P(n) == forall(Integers,P)
With type:
forall :: Set<T> -> (T -> bool) -> bool
Exists has the same type. Forall is like an infinite conjunction, where S[n] is the n-th elemen to of the set S:
forall(S,P) = P(S[0]) ∧ P(S[1]) ∧ P(S[2]) ...
Exists is like an infinite disjunction:
exists(S,P) = P(S[0]) ∨ P(S[1]) ∨ P(S[2]) ...
If we do an analogy with types, we could say that the type analogue of ∧ is computing the intersection type ∩, and the type analogue of ∨ computing the union type ∪. We could then define forall and exists on types as follows:
forall(S,P) = P(S[0]) ∩ P(S[1]) ∩ P(S[2]) ... exists(S,P) = P(S[0]) ∪ P(S[1]) ∪ P(S[2]) ...
So forall is an infinite intersection, and exists is an infinite union. Their types would be:
forall, exists :: Set<T> -> (T -> Type) -> Type
For example the type of the polymorphic identity function. Here
Types
is the set of all types, and->
is the type constructor for functions and=>
is lambda abstraction:forall(Types, t => (t -> t))
Now a thing of type
forall T:Type. T -> T
is a value, not a function from types to values. It is a value whose type is the intersection of all types T -> T where T ranges over all types. When we use such a value, we do not have to apply it to a type. Instead, we use a subtype judgement:id :: forall T:Type. T -> T id = (x => x) id2 = id :: int -> int
This downcasts
id
to have typeint -> int
. This is valid becauseint -> int
also appears in the infinite intersection.This works out nicely I think, and it clearly explains what forall is and how it is different from lambda, but this model is incompatible with what I have seen in languages like ML, F#, C#, etc. For example in F# you do
id<int>
to get the identity function on ints, which does not make sense in this model: id is a function on values, not a function on types that returns a function on values.
有类型理论知识的人可以解释一下到底什么是 forall 和存在的吗? “forall 在类型级别上是 lambda”在多大程度上是真的?
最佳答案
让我分别解决你的问题。
pack (Int, (λx. x, λx. x)) : ∃ T. (Int → T) × (T → Int)
这是一个简单的 ADT,其表示为 Int,并且仅提供两个操作(作为嵌套元组),用于将 int 转换为抽象类型 T 的进出。例如,这是模块类型理论的基础。
关于haskell - 什么是类型量词?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/10062253/