Haskell PolyKinds extension and type families

user_14644255 0
Viewed 228

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.

polykinds data-kinds functional-programming haskell types
2 Answers

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.

user_1658060

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

user_75090650
Related