我在 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。感謝您提前提供任何想法和幫助。
uj5u.com熱心網友回復：
我建議你使用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
之間的區別Proxy，定義為統一資料型別（非 GADT 或半開玩笑：“傳統”語法）或 GADT。它們是從等效（在一個舊GHC 8.10測驗）隔開?感
- (
forall.) 指定 = 可以用 指定TypeApplications，但如果未指定則自動推斷 - (
forall{}.) inferred =TypeApplications跳過，不能直接指定
這適用于為消歧Proxy命名的型別建構式和資料建構式P，因為它們都是多型的。Proxy可以根據 的量化來指定Proxy @Nat 42或推斷：Proxy 42k
Proxy :: forall (k :: Type). k -> Type
-- or
Proxy :: forall {k :: Type}. k -> Type
并且根據 中的量化P，可以指定或推斷k：P @Nat @42P @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
這給出了幾個結果
- k在兩者中推斷：
P @42 :: Proxy 42(P @42 :: Proxy 42)
data Proxy a = P
--
data Proxy a where
P :: Proxy a
- k
Proxy在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
Proxy和P(P @Nat @42 :: Proxy @Nat 42) 中指定的k
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
我正在等待對量化和范圍界定的許多新的和即將到來的變化塵埃落定，這可能已經過時了。
uj5u.com熱心網友回復：
你是一種語言擴展。如果您也啟用了CUSKs擴展程式，那么您撰寫的內容將滿足您的需求。
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/374161.html
上一篇：如何在純函式中跳過不必要的IO？