PolyKinds

高階多相型をするためのGHC拡張

自動的にKindSignaturesも付随する

PolyKindsを有効にすることでkindを多相にすることができる

defaultでは、kindは*または->の2種類である

*は、いわば具体kindなので、そこへ*->*などを代入することはできない

例えば、data App f a = App (f a)という型は、

App :: (* -> *) -> * -> *と推論されるが、

App :: (ココ -> *) -> ココ -> *のココの部分は別に具体型じゃなくても矛盾は生じないはず

つまり、defaultでは無駄に制限が強い

そこで、PolyKindsを有効にすると、多相にできる箇所は多相で推論してくれる

App :: (k -> *) -> k -> *

kには、*でも*->*でも、*->*->*でも何でも取れるようになっている

安全な範囲で制限が緩まった感じmrsekut.icon

有効にする前後で、ghciの:kの結果が変わっている

KindSignaturesと併用することが多い

だから自動でKindSignaturesも有効になる

簡単な例

PolyKindsを有効にする前では、

code:hs

{-# LANGUAGE DataKinds #-}

data N (n :: *) = N -- data N n = N　と同じ

type A1 = N Int -- ok

type A2 = N (Int -> String) -- ok

type A3 = N Maybe -- error

型引数nのkindは、無駄に*へと具体化されてしまうので、Maybeのような*->*な型は代入できない

有効にすると、

code:hs

-- {-# LANGUAGE DataKinds #-} 不要

{-# LANGUAGE PolyKinds #-}

data P (n :: k) = P

type A1 = P Int -- ok

type A2 = P (Int -> String) -- ok

type A3 = P Maybe -- ok

使用例

ServantのVerb型の定義の意味を理解する

Proxy型

実際の定義はもう少し複雑だがノリはこんなん

code:hs

data Proxy (t :: k) = Proxy

任意のkindの型を引数に取る幽霊型

もし、PolyKindsがなかったら*->*のレベルごとに定義しないといけない

code:hs

{-# LANGUAGE KindSignatures #-}

data Proxy1 (a :: *) = Proxy1 -- Proxy1 Maybeはerrorになる

data Proxy2 (a :: * -> *) = Proxy2

data Proxy3 (a :: * -> * -> *) = Proxy3

purs

pursはv0.14.0からはいった

だから、dataやclassで型変数を用いた定義をしたい場合は記述方法が以前と異なる

https://github.com/purescript/purescript/releases/tag/v0.14.0

pursuitの型表記が2021/7/4現在古いままになってる

issueは出てる

classの場合はこんな感じになる

classの返り値をConstraintにしないといけないのはちょっと覚えづらい

型の文脈でのTypeみたいな感じかmrsekut.icon

code:purs(hs)

class Cons :: forall k. Symbol -> k -> Row k -> Row k -> Constraint

class Cons label a tail row | label a tail -> row, label row -> a tail

参考

About kind system of Haskell (Part 1) - Haskell-jp

わかりやすい