[解決済み] Haskellの[]と':'とは何ですか？

質問

こんなの見たことある '[] と ': のようなヘテロジニアスリストパッケージを中心に、いくつかの場所で構文が使用されています。 HList または HVect .

例えば、ヘテロジニアスベクトル HVect は次のように定義されます。

data HVect (ts :: [*]) where
    HNil :: HVect '[]
    (:&:) :: !t -> !(HVect ts) -> HVect (t ': ts)

GHCiでは、拡張子 TemplateHaskell または DataKinds このようになります。

> :t '[]
'[] :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name
> :t '(:)
'(:) :: template-haskell-2.13.0.0:Language.Haskell.TH.Syntax.Name

テンプレートhaskellではなく、依存型や種類などに関係する印象がありました。

検索エンジンで、しかも フーグル を、そして ハユー でクエリを処理します。 '[] または ': という質問がありました。 これらの名称は何ですか？ '[] と ': のこと？ ドキュメントやチュートリアルの紹介は大歓迎です。

どのように解決するのですか？

DataKinds は、項レベルのコンストラクタを型レベルで使用できるようにします。

その後

data T = A | B | C

の値でインデックスされた型を書くことができます。 T

data U (t :: T) = ...
foo :: U A -> U B -> ...

ところが、ここで A と B は値としてではなく型として使用されます。従って、それらは引用符を使用して "promoted"する必要があります。

data U (t :: T) = ...
foo :: U 'A -> U 'B -> ...

おなじみのリスト構文でも同じことが言えます。 '[] は型レベルで昇格した空リストです。 '[a,b,c] と同じです。 a ': b ': c ': '[] のように、型レベルで昇格するリストです。

type           :: kind
'[]            :: [k]   -- polykinded! works for any kind k
'[ 'A, 'B, 'C] :: [T]   -- mind the spaces, we do not want the char '['
'A ': '[]      :: [T]
'[ Int, Bool ] :: [*]   -- a list of types
'[ Int ]       :: [*]   -- a list of types with only one element
[Int]          :: *     -- a type "list of Int"

最後の2つのケースは、引用符によって構文が曖昧になることに注意してください。