Menu
I've read a lot of interesting things about type kinds, higher-kinded types and so on. By default Haskell supports two sorts of kind:
* * → * Latest GHC's language extensions ConstraintKinds adds a new kind:
Constraint Also after reading this mailing list it becomes clear that another type of kind may exists, but it is not supported by GHC (but such support is implemented in .NET):
# I've learned about polymorphic kinds and I think I understand the idea. Also Haskell supports explicitly-kinded quantification.
So my questions are:
subkinding mean? Where is it implemented/useful?kinds, like kinds are a type system on top of types? (just interested)
956
In type theory, every term has a type. A term and its type are often written together as "term : type". A common type to include in a type theory is the Natural numbers, often written as " " or "nat". Another is Boolean logic values.
Church's type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory.
A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be scientific, belong to a non-scientific discipline, or no discipline at all.
Sheldon's Theory of Personality (Type Theory): In the 1940s, William Herbert Sheldon associated body types with human temperament types. He claimed that a body type could be linked with the personality of that person.
Yes, other kinds exist. The page Intermediate Types describes other kinds used in GHC (including both unboxed types and some more complicated kinds as well). The Ωmega language takes higher-kinded types to the maximum logical extension, allowing for user-definable kinds (and sorts, and higher). This page proposes a kind system extension for GHC which would allow for user-definable kinds in Haskell, as well as a good example of why they would be useful.
As a short excerpt, suppose you wanted a list type which had a type-level annotation of the length of the list, like this:
data Zero data Succ n data List :: * -> * -> * where Nil :: List a Zero Cons :: a -> List a n -> List a (Succ n) The intention is that the last type argument should only be Zero or Succ n, where n is again only Zero or Succ n. In short, you need to introduce a new kind, called Nat which contains only the two types Zero and Succ n. Then the List datatype could express that the last argument is not a *, but a Nat, like
data List :: * -> Nat -> * where Nil :: List a Zero Cons :: a -> List a n -> List a (Succ n) This would allow the type checker to be much more discriminative in what it accepts, as well as making type-level programming much more expressive.
142
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
