Haskell PolyKinds extension and type families

Question

I working on type families in Haskell to get deeper inside this topic, and trying to use polymorphic kinds and type families at the same time.

For example, the beginning of the file has the following language extensions (there is more in the file later than will be shown here):

{-# LANGUAGE TypeFamilies,
StandaloneKindSignatures,
RankNTypes,
PolyKinds,
DataKinds,
TypeOperators,
TypeApplications,
KindSignatures,
ScopedTypeVariables,
UndecidableInstances,
MultiParamTypeClasses,
AllowAmbiguousTypes #-}

Then I'm using polymorphic kinds in type declaration:

data Proxy (a :: k) = Proxy

which works well. But at the time I'm trying to use them inside type families with richer definition:

type family PK (a :: k) :: Type where
  PK Int = Char

GHC throws an error:

• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘PK’, namely ‘Int’
  In the type family declaration for ‘PK’.

Is there a fix for that? The GHC version is 8.10.7. Thanks for any idea and help in advance.

Iceland_jack · Accepted Answer · 2021-12-05T15:45:03.200

I recommend you use StandaloneKindSignatures:

..
{-# Language StandaloneKindSignatures #-}

type Id :: k -> k
type Id a = a

type Proxy :: k -> Type
data Proxy a = Proxy

type
  PK :: k -> Type
type family
  PK a where
  PK Int = Char

The kind argument is invisible but you can write it explicitly in the type family PK @Type Int = Char (requires TypeApplications).

With GADTs you can write Proxy

type Proxy :: k -> Type
data Proxy a where
  Proxy :: Proxy @k a

There are proposals to allow visible (kind) applications in the declaration heads:

type Id :: k -> k
type Id @k a = a

type Proxy :: k -> Type
data Proxy @k a = Proxy

type
  PK :: k -> Type
type family
  PK @k    a where
  PK @Type Int = Char

And we can use "visible dependent quantification" in kinds with forall-> instead of (implicit) invisible forall.


type Id :: forall k -> k -> k
type Id k a = a

type Proxy :: forall k -> k -> Type
data Proxy k a = Proxy

type
  PK :: forall k -> k -> Type
type family
  PK k    a where
  PK Type Int = Char

Difference between Proxy, defined as a uniform datatype (non-GADT or tongue-in-cheek: 'legacy' syntax) or a GADT. They are equivalent (tested on an old GHC 8.10) apart from k being

(forall.) specified = can be specified with TypeApplications, but is automatically inferred if not specified
(forall{}.) inferred = TypeApplications skips it, cannot be specified directly

This applies both to the type constructor Proxy and the data constructor named P for disambiguation since both are polymorphic. Proxy can be specified Proxy @Nat 42 or inferred Proxy 42 depending on the quantification of k:

Proxy :: forall (k :: Type). k -> Type
-- or
Proxy :: forall {k :: Type}. k -> Type

And depending on the quantification in P, k can be specified P @Nat @42 or inferred P @42:

P :: forall {k :: Type} (a :: k). Proxy @k a
P :: forall {k :: Type} (a :: k). Proxy    a
-- or
P :: forall (k :: Type) (a :: k). Proxy @k a
P :: forall (k :: Type) (a :: k). Proxy    a

This gives several outcomes

k inferred in both: P @42 :: Proxy 42 (P @42 :: Proxy 42)

data Proxy a = P
--
data Proxy a where
 P :: Proxy a

k specified in Proxy but inferred in P (P @42 :: Proxy @Nat 42)

data Proxy (a :: k) where
 P :: Proxy a
--
type Proxy :: k -> Type
data Proxy a where
  P :: Proxy a

k specified in both Proxy and P (P @Nat @42 :: Proxy @Nat 42)

data Proxy (a :: k) = P
--
type Proxy :: k -> Type
data Proxy a = P
--
type Proxy :: forall k. k -> Type
data Proxy a = P
--
type Proxy :: forall k. k -> Type
data Proxy (a :: k) = P
--
type Proxy :: k -> Type
data Proxy a where
 P :: Proxy @k a

I am waiting for the dust to settle on many of the new and coming changes to quantification and scoping, this may already be out of date.

That's a nice solution to consider writing type families and data types in the same fashion, it has more control over implicit details. And GADs extension appeared to be quite useful as well. And one more thing: Can ```Id``` type synonym be transformed equivalently to type family? — A. G, Dec 04 '21 at 10:30
You can write it as `type family Id a where Id a = a` with the same kind signature, I believe it is equivalent but take it with a grain of salt because type families can be nuanced (see [On the arity of type families](https://ryanglscott.github.io/2019/05/26/on-the-arity-of-type-families/)) — Iceland_jack, Dec 04 '21 at 15:31
By the way, is the written ```Proxy``` data type (the one with ```GADTs``` extension) equivalent to the one simple written as (without defining previously its kind): ```data Proxy a = Proxy```? — A. G, Dec 05 '21 at 11:53
I tried different variations of it, see the end of the answer. — Iceland_jack, Dec 05 '21 at 15:45
There have been rather confusing changes in what implicitly bound kind variables do. I'm a bit lost. — dfeuer, Dec 06 '21 at 05:21
@Iceland_jack, that was quite clear explanation of the problem regarding implicit and explicit kinds, because I had a problem with specifying them in a program, but didn't see reasons of errors. — A. G, Dec 06 '21 at 14:21

score 1 · Answer 2 · answered Dec 03 '21 at 18:28

1

You were one language extension away. If you enable the CUSKs extension too, then what you wrote will do what you want.

answered Dec 03 '21 at 18:28

Joseph Sible-Reinstate Monica

45,431
5
48
98

Haskell PolyKinds extension and type families

2 Answers2