Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,265
    • Issues 4,265
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 419
    • Merge Requests 419
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Wiki
    • Commentary
    • Compiler
  • kinds

Last edited by Takenobu Tani Jun 20, 2020
Page history New page

kinds

TODO This page is somewhat old. It needs to be updated with recent information. The followings are the latest related information.

GHC User's Guide:

  • Levity polymorphism
  • The kind *

GHC Proposals:

  • Revise Levity Polymorphism
  • Embrace Type :: Type
  • Remove the * kind syntax

Papers:

  • System FC with Explicit Kind Equality
  • Levity Polymorphism (extended version)

Kinds

Kinds classify types. So for example:

   Int :: *
   Int -> Int :: *
   Maybe :: * -> *
   Int# :: #
   (# Int, Int #) :: #

The base kinds are these:

  • "*" is the kind of lifted, boxed values. Things like Int and Maybe Float have kind *.
  • "#" is the kind of unlifted values. Things like Int# have kind #.
  • With the advent of data type promotion and kind polymorphism we can have a lot more kinds.
  • Kinds are in flux with levity polymorphism. See LevityPolymorphism. See also TypeType.

(Unboxed tuples used to have a distinct kind, but in 2012 we combined unboxed tuples with other unboxed values in a single kind "#".)

Representing kinds

Kinds are represented by the data type Type (see Commentary/Compiler/TypeType):

type Kind = Type

Basic kinds are represented using type constructors, e.g. the kind * is represented as

liftedTypeKind :: Kind
liftedTypeKind = TyConApp liftedTypeKindTyCon []

where liftedTypeKindTyCon is a built-in PrimTyCon. The arrow type constructor is used as the arrow kind constructor, e.g. the kind * -> * is represented internally as

FunTy liftedTypeKind liftedTypeKind

It's easy to extract the kind of a type, or the sort of a kind:

typeKind :: Type -> Kind

The "sort" of a kind is always one of the sorts: TY (for kinds that classify normal types) or CO (for kinds that classify coercion evidence). The coercion kind, T1 :=: T2, is represented by PredTy (EqPred T1 T2).

Kind subtyping

There is a small amount of sub-typing in kinds. Suppose you see (t1 -> t2). What kind must t1 and t2 have? It could be * or #. So we have a single kind OpenKind, which is a super-kind of both, with this simple lattice:

(You can edit this picture here.)

Clone repository

GHC Home
GHC User's Guide

Joining In

Newcomers info
Mailing Lists & IRC
The GHC Team

Documentation

GHC Status Info
Working conventions
Building Guide
Debugging
Commentary

Wiki

Title Index
Recent Changes