PolyKinds
自動的にKindSignaturesも付随する
PolyKindsを有効にすることでkindを多相にすることができる
defaultでは、kindは
* または -> の2種類である * は、いわば具体kindなので、そこへ *->* などを代入することはできない例えば、
data App f a = App (f a) という型は、 App :: (* -> *) -> * -> * と推論されるが、 App :: (ココ -> *) -> ココ -> * の ココ の部分は別に具体型じゃなくても矛盾は生じないはずつまり、defaultでは無駄に制限が強い
そこで、PolyKindsを有効にすると、多相にできる箇所は多相で推論してくれる
App :: (k -> *) -> k -> * k には、 * でも *->* でも、 *->*->* でも何でも取れるようになっている安全な範囲で制限が緩まった感じ
有効にする前後で、ghciの
:k の結果が変わっているKindSignaturesと併用することが多い
だから自動でKindSignaturesも有効になる
簡単な例
PolyKindsを有効にする前では、
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 のような *->* な型は代入できない有効にすると、
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使用例
実際の定義はもう少し複雑だがノリはこんなん
hsdata Proxy (t :: k) = Proxy任意のkindの型を引数に取る幽霊型
もし、PolyKindsがなかったら
*->* のレベルごとに定義しないといけない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 で型変数を用いた定義をしたい場合は記述方法が以前と異なるpursuitの型表記が2021/7/4現在古いままになってる
issueは出てる
classの場合はこんな感じになる
classの返り値を
Constraint にしないといけないのはちょっと覚えづらい型の文脈での
Type みたいな感じか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参考
わかりやすい