Tim*_*Tim 8 polymorphism haskell types parametric-polymorphism
Hutton在Haskell中编程说：
包含一个或多个类型变量的类型称为多态。
哪个是多态类型：一个类型或一组类型？
用具体类型替换其类型变量的多态类型是类型吗？
用不同具体类型替换其类型变量的多态类型是否被视为相同或不同类型？
HTN*_*TNW 13
Is a polymorphic type with a concrete type substituting its type variable a type?
That's the point, yes. However, you need to be careful. Consider:
id :: a -> a
That's polymorphic. You can substitute a := Int and get Int -> Int, and a := Float -> Float and get (Float -> Float) -> Float -> Float. However, you cannot say a := Maybe and get id :: Maybe -> Maybe. That just doesn't make sense. Instead, we have to require that you can only substitute concrete types like Int and Maybe Float for a, not abstract ones like Maybe. This is handled with the kind system. This is not too important for your question, so I'll just summarize. Int and Float and Maybe Float are all concrete types (that is, they have values), so we say that they have type Type (the type of a type is often called its kind). Maybe is a function that takes a concrete type as an argument and returns a new concrete type, so we say Maybe :: Type -> Type. In the type a -> a, we say the type variable a must have type Type, so now the substitutions a := Int, a := String, etc. are allowed, while stuff like a := Maybe isn't.
Is a polymorphic type with different concrete types substituting its type variable considered the same or different types?
No. Back to a -> a: a := Int gives Int -> Int, but a := Float gives Float -> Float. Not the same.
Which is a polymorphic type: a type or a set of types?
Now that's a loaded question. You can skip to the TL;DR at the end, but the question of "what is a polymorphic type" is actually really confusing in Haskell, so here's a wall of text.
There are two ways to see it. Haskell started with one, then moved to the other, and now we have a ton of old literature referring to the old way, so the syntax of the modern system tries to maintain compatibility. It's a bit of a hot mess. Consider
id x = x
What is the type of id? One point of view is that id :: Int -> Int, and also id :: Float -> Float, and also id :: (Int -> Int) -> Int -> Int, ad infinitum, all simultaneously. This infinite family of types can be summed up with one polymorphic type, id :: a -> a. This point of view gives you the Hindley-Milner type system. This is not how modern GHC Haskell works, but this system is what Haskell was based on at its creation.
In Hindley-Milner, there is a hard line between polymorphic types and monomorphic types, and the union of these two groups gives you "types" in general. It's not really fair to say that, in HM, polymorphic types (in HM jargon, "polytypes") are types. You can't take polytypes as arguments, or return them from functions, or place them in a list. Instead, polytypes are only templates for monotypes. If you squint, in HM, a polymorphic type can be seen as a set of those monotypes that fit the schema.
Modern Haskell is built on System F (plus extensions). In System F,
id = \x -> x -- rewriting the example
is not a complete definition. Therefore we can't even think about giving it a type. Every lambda-bound variable needs a type annotation, but x has no annotation. Worse, we can't even decide on one: \(x :: Int) -> x is just as good as \(x :: Float) -> x. In System F, what we do is we write
id = /\(a :: Type) -> \(x :: a) -> x
using /\ to represent ? (upper-case lambda) much as we use \ to represent ?.
id is a function taking two arguments. The first argument is a Type, named a. The second argument is an a. The result is also an a. The type signature is:
id :: forall (a :: Type). a -> a
forall is a new kind of function arrow, basically. Note that it provides a binder for a. In HM, when we said id :: a -> a, we didn't really define what a was. It was a fresh, global variable. By convention, more than anything else, that variable is not used anywhere else (otherwise the Generalization rule doesn't apply and everything breaks down). If I had written e.g. inject :: a -> Maybe a, afterwards, the textual occurrences of a would be referring to a new global entity, different from the one in id. In System F, the a in forall a. a -> a actually has scope. It's a "local variable" available only for use underneath that forall. The a in inject :: forall a. a -> Maybe a may or may not be the "same" a; it doesn't matter, because we have actual scoping rules that keep everything from falling apart.
Because System F has hygienic scoping rules for type variables, polymorphic types are allowed to do everything other types can do. You can take them as arguments
runCont :: forall (a :: Type). (forall (r :: Type). (a -> r) -> r) -> a
runCons a f = f a (id a) -- omitting type signatures; you can fill them in
You put them in data constructors
newtype Yoneda f a = Yoneda (forall b. (a -> b) -> f b)
You can place them in polymorphic containers:
type Bool = forall a. a -> a -> a
true, false :: Bool
true a t f = t
false a t f = f
thueMorse :: [Bool]
thueMorse = false : true : true : false : _etc
There's an important difference from HM. In HM, if something has polymorphic type, it also has, simultaneously, an infinity of monomorphic types. In System F, a thing can only have one type. id = /\a -> \(x :: a) -> x has type forall a. a -> a, not Int -> Int or Float -> Float. In order to get an Int -> Int out of id, you have to actually give it an argument: id Int :: Int -> Int, and id Float :: Float -> Float.
Haskell is not System F, however. System F is closer to what GHC calls Core, which is an internal language that GHC compiles Haskell to—basically Haskell without any syntax sugar. Haskell is a Hindley-Milner flavored veneer on top of a System F core. In Haskell, nominally a polymorphic type is a type. They do not act like sets of types. However, polymorphic types are still second class. Haskell doesn't let you actually type forall without -XExplicitForalls. It emulates Hindley-Milner's wonky implicit global variable creation by inserting foralls in certain places. The places where it does so are changed by -XScopedTypeVariables. You can't take polymorphic arguments or have polymorphic fields unless you enable -XRankNTypes. You cannot say things like [forall a. a -> a -> a], nor can you say id (forall a. a -> a -> a) :: (forall a. a -> a -> a) -> (forall a. a -> a -> a)—you must define e.g. newtype Bool = Bool { ifThenElse :: forall a. a -> a -> a } to wrap the polymorphism under something monomorphic. You cannot explicitly give type arguments unless you enable -XTypeApplications, and then you can write id @Int :: Int -> Int. You cannot write type lambdas (/\), period; instead, they are inserted implicitly whenever possible. If you define id :: forall a. a -> a, then you cannot even write id in Haskell. It will always be implicitly expanded to an application, id @_.
TL;DR: In Haskell, a polymorphic type is a type. It's not treated as a set of types, or a rule/schema for types, or whatever. However, due to historical reasons, they are treated as second class citizens. By default, it looks like they are treated as mere sets of types, if you squint a bit. Most restrictions on them can be lifted with suitable language extensions, at which point they look more like "just types". The one remaining big restriction (no impredicative instantiations allowed) is rather fundamental and cannot be erased, but that's fine because there's a workaround.
编辑：下面的答案并没有回答这个问题。区别在于术语上的一个微妙错误：像Maybe和 之类的类型[]是高级类型，而像forall a. a -> a和 之类的类型forall a. Maybe a是多态的。下面的答案与更高种类的类型有关，但问题是关于多态类型的。我\xe2\x80\x99m仍然保留这个答案，以防它对其他人有帮助，但我现在意识到它\xe2\x80\x99s并不是真正问题的答案。
我认为多态的高级类型更接近于一组类型。例如，您可以将其视为Maybe集合 { Maybe Int, Maybe Bool, \xe2\x80\xa6}。
然而，严格来说，这有点误导。为了更详细地解决这个问题，我们需要了解种类。与类型描述值的方式类似，我们说种类描述类型。这个想法是：
\n\n*. 示例包括Bool、、和，它们都有Char类型。这表示为例如。请注意，诸如 之类的函数也有 kind ，因为这些是具体类型，可以包含诸如!IntMaybe String*Bool :: *Int -> String*showid :: a -> a，我们可以说Maybe :: * -> *，sinceMaybe接受具体类型作为参数（例如Int），并生成具体类型作为结果（例如Maybe Int）。类似的东西a -> a也有 kind * -> *，因为它有一个类型参数 ( a) 并产生一个具体的结果 ( a -> a) 。您还可以获得更复杂的类型：例如，data Foo f x = FooConstr (f x x)has kind Foo :: (* -> * -> *) -> * -> *。（你能明白为什么吗？）（如果上面的解释\xe2\x80\x99没有意义，《Learn You a Haskell》一书也有关于类型的精彩部分。）
\n\n那么现在我们可以正确地回答您的问题了：
\n\n\n\n\n哪一个是
\n多态的高级类型：一个类型还是一组类型？
两者都不是：多态的高级类型是类型级函数，如其类型中的箭头所示。例如，Maybe :: * -> *是一个类型级函数，可以转换Int\xe2\x86\x92 Maybe Int、Bool\xe2\x86\x92Maybe Bool等。
\n\n\n\n
用具体类型代替其类型变量的多态高级类型是类型吗？
是的，当您的多态高级类型有一种时* -> *（即它有一个类型参数，它接受具体类型）。当您将具体类型应用于Conc :: *type时Poly :: * -> *，它\xe2\x80\x99 只是函数应用程序，如上所述，结果就是Poly Conc :: *具体类型。
\n\n\n用不同的具体类型替换其类型变量的
\n多态高级类型被视为相同类型还是不同类型？
这个问题有点不合时宜，因为它与\xe2\x80\x99t 没有任何关系。答案肯定是否定的Maybe Int：像和一样的两种类型Maybe Bool并不相同。Nothing可能是两种类型的成员，但只有前者包含 value Just 4，并且只有后者包含 value Just False。
另一方面，可以有两种不同的替换，其中结果类型是同构的。（同构是指两种类型不同，但在某些方面等效。例如，(a, b)和(b, a)是同构的，尽管类型相同。形式条件是，当您可以编写两个反函数和时，两种类型p,是同构的。）qp -> qq -> p
其中一个例子是Const：
data Const a b = Const { getConst :: a }\n该类型只是忽略它的第二个类型参数；因此，像Const Int Char和 这样的两种类型Const Int Bool是同构的。但是，它们不是同一类型：如果您创建一个 type 值Const Int Char，但随后将其用作 type 的某个值Const Int Bool，这将导致类型错误。a这种功能非常有用，因为这意味着您可以使用\xe2\x80\x98tag\xe2\x80\x99 类型Const a tag，然后使用tag作为类型级别信息的标记。