Расширение Haskell PolyKinds и семейства типов

Question

Я работал над семействами типов в Haskell, чтобы глубже проникнуть в эту тему, и пытался одновременно использовать полиморфные типы и семейства типов.

Например, начало файла имеет следующие языковые расширения (в файле их больше, чем показано здесь):

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

Затем я использую полиморфные виды в объявлении типа:

      data Proxy (a :: k) = Proxy

который хорошо работает. Но в то время я пытаюсь использовать их внутри семейств типов с более богатым определением:

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

GHC выдает ошибку:

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

Есть ли исправление для этого? Версия GHC - 8.10.7. Заранее благодарим за любую идею и помощь.

Answer 1

Я рекомендую вам использовать 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

Аргумент kind невидим, но вы можете указать его явно в семействе типов PK @Type Int = Char(требует TypeApplications).

С помощью GADT вы можете писать Proxy

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

Есть предложения разрешить видимые (видовые) приложения в заголовках объявлений:

      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

И мы можем использовать «видимую зависимую количественную оценку» в видах с forall->вместо (неявного) невидимого 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

Answer 2

Вы были на расстоянии одного языкового расширения. Если вы включите CUSKsрасширение тоже, то то, что вы написали, будет делать то, что вы хотите.