Menu
When I was experimenting with Haskell kinds, and trying to get the kind of ->, and this showed up:
$ ghci ... Prelude> :k (->) (->) :: ?? -> ? -> * Prelude> Instead of the expected * -> * -> *. What are the ?? and ? things? Do they mean concrete types or "kind variables"? Or something else?
881
From HaskellWiki. Wikipedia says, "In type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator.
If you are using an interactive Haskell prompt (like GHCi) you can type :t <expression> and that will give you the type of an expression. e.g. or e.g.
Haskell also incorporates polymorphic types---types that are universally quantified in some way over all types. Polymorphic type expressions essentially describe families of types. For example, (forall a)[a] is the family of types consisting of, for every type a, the type of lists of a.
Functions can also be passed as arguments or returned (as we have seen). Their types are given in the type signature. *Main> :t map map :: (a -> b) -> [a] -> [b] *Main> :t filter filter :: (a -> Bool) -> [a] -> [a] flip_args :: (a -> b -> c) -> b -> a -> c flip_args f x y = f y x.
These are GHC-specific extensions of the Haskell kind system. The Haskell 98 report specifies only a simple kind system:
... type expressions are classified into different kinds, which take one of two possible forms:
The symbol * represents the kind of all nullary type constructors. If k1 and k2 are kinds, then k1->k2 is the kind of types that take a type of kind k1 and return a type of kind k2.
GHC extends this system with a form of kind subtyping, to allow unboxed types, and to allow the function construtor to be polymorphic over kinds. The kind lattice GHC supports is:
? /\ / \ ?? (#) / \ * # Where: * [LiftedTypeKind] means boxed type # [UnliftedTypeKind] means unboxed type (#) [UbxTupleKind] means unboxed tuple ?? [ArgTypeKind] is the lub of {*, #} ? [OpenTypeKind] means any type at all Defined in ghc/compiler/types/Type.lhs
In particular:
> error :: forall a:?. String -> a > (->) :: ?? -> ? -> * > (\\(x::t) -> ...) Where in the last example t :: ?? (i.e. is not an unboxed tuple). So, to quote GHC, "there is a little subtyping at the kind level".
For interested souls, GHC also supports coercion types and kinds ("type-level terms which act as evidence for type equalities", as needed by System Fc) used in GADTs, newtypes and type families.
148
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
