Programming in Haskell by Hutton says:
A type that contains one or more type variables is called polymorphic.
Which is a polymorphic type: a type or a set of types?
Is a polymorphic type with a concrete type substituting its type variable a type?
Is a polymorphic type with different concrete types substituting its type variable considered the same or different types?
A function that can evaluate to or be applied to values of different types is known as a polymorphic function. A data type that can appear to be of a generalized type (e.g. a list with elements of arbitrary type) is designated polymorphic data type like the generalized type from which such specializations are made.
Different types of polymorphism Java supports 2 types of polymorphism: static or compile-time. dynamic.
Inclusion polymorphism, also known as subtyping, is when a single name refers to many instances of different classes as long as they share the same superclass.
A type that contains one or more type variables is called polymorphic.
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 Gen
eralization 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 forall
s 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.
There is some nuance in the word "type" here. Values have concrete types, which cannot be polymorphic. Expressions, on the other hand, have general types, which can be polymorphic. If you're thinking of types for values, then a polymorphic type can be thought of loosely as defining sets of possible concrete types. (At least first-order polymorphic types! Higher-order polymorphism breaks this intuition.) But that's not always a particularly useful way of thinking, and it's not a sufficient definition. It doesn't capture which sets of types can be described in this way (and related notions like parametricity.)
It's a good observation, though, that the same word, "type", is used in these two related, but different, ways.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With