What is '[] and ': in Haskell?

Question

I've seen this '[] and ': syntax in a few places, most notably in heterogeneous lists packages like HList or HVect.

For example, the heterogeneous vector HVect is defined as

data HVect (ts :: [*]) where
    HNil :: HVect '[]
    (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)

In GHCi, with extension TemplateHaskell or DataKinds, I get this

> :t '[]
'[] :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name
> :t '(:)
'(:) :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name

I had the impression that this has to do with dependent types and kinds, etc., not with template haskell.

The search engines, and hoogle, and hayoo, handle queries with '[] or ': rather badly, hence the question: What is the name of these '[] and ': things? Pointers to documentation or tutorials would be most welcome.

Answer 1

DataKinds allows one to use term-level constructors at the type level.

After

data T = A | B | C

one can write types indexed by a value of T

data U (t :: T) = ...
foo :: U A -> U B -> ...

Here, however, A and B are used as types, not as values. Hence, they have to be "promoted" using a quote:

data U (t :: T) = ...
foo :: U 'A -> U 'B -> ...

The same happens with the familiar list syntax. '[] is an empty list, promoted at the type level. '[a,b,c] is the same as a ': b ': c ': '[], a list promoted at the type level.

type           :: kind
'[]            :: [k]   -- polykinded! works for any kind k
'[ 'A, 'B, 'C] :: [T]   -- mind the spaces, we do not want the char '['
'A ': '[]      :: [T]
'[ Int, Bool ] :: [*]   -- a list of types
'[ Int ]       :: [*]   -- a list of types with only one element
[Int]          :: *     -- a type "list of Int"

Note the last two cases, where the quote disambiguates the syntax.

Answer 2

The book

Thinking with Types by Sandy Maguire (http://thinkingwithtypes.com)

could be a good resource on topic of type-level programming in Haskell in general. The chapter "Lifting Restrictions" deals with DataKinds and promoted constructors.

(Disclaimer: No affiliation.)