Can I write a product kind for kind product of kinds without polluting the term level namespace ?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}

data Pair a b = Pair a b

type family Proj1 (asd :: Pair a b) where
  Proj1 ('Pair a b) = a

type family Proj2 (asd :: Pair a b) where
  Proj2 ('Pair a b) = b

CodePudding user response：

Well, you can leave out the constructor:

data Pair a b

Now, Pair is both a type-level product:

x :: Pair a b
x = undefined

and a kind-level product:

type family Proj1 (x :: Pair a b)

with no associated term-level Pair.

It ends up being a little hard to do much with it. Since it's uninhabited as a type (no terms) and uninhabited as a kind (no types).

I think that's what @chepner was pointing out in the comment. Since the only way to define a new kind in Haskell is to define a new type and lift it, the only way to define a new kind without affecting the term-level namespace is to define an uninhabited new type and lift it to an uninhabited kind.

Note that, as soon as DataKinds is enabled, the kind-level product (,) automatically springs into existence, so if your worry is about adding to term-level namespace pollution, you can just use that one:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

type family Proj1 (asd :: (a,b)) where
  Proj1 '(a,b) = a

type family Proj2 (asd :: (a,b)) where
  Proj2 '(a,b) = a

and in GHCi:

> :kind! Proj1 '(Int, String)
Proj1 '(Int,String) :: *
= Int