[解決済み] レビティ多態性とは

質問

質問のタイトルにあるように、Levity polymorphismとは何か、またその動機は何なのかを知りたいのです。私が知っているのは このページ にはいくつかの詳細がありますが、そこでの説明のほとんどは私の頭の上を通過しています :)

一方 このページ は少し親切になりましたが、私はまだその背後にある動機を理解することができません。

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

注意してください。 この回答はLevityの議論に関するごく最近の観察に基づくものです。Levityポリモーフィズムに関するすべてのことは、現在GHC 8.0のリリース候補にのみ実装されており、そのため変更される可能性があります( #11471 を参照)。

TL;DR : これは通常の関数では不可能な、lifted型とunlifted型に対する関数の多相性を実現する方法です。例えば、以下のコードは通常のポリモーフィズムでは型チェックを行いません、なぜなら Int# は種類 # を持ちますが、型変数が id には種類 * :

{-# LANGUAGE MagicHash #-}

import GHC.Prim

example :: Int# -> Int# 
example = id            -- does not work, since id :: a -> a

Couldn't match kind ‘*’ with ‘#’
When matching types
  a0 :: *
  Int# :: #
Expected type: Int# -> Int#
  Actual type: a0 -> a0
In the expression: id

なお (->) はまだいくつかのマジックを使っていることに注意してください。

この質問に答え始める前に、一歩下がって、最もよく使われる関数の1つに行きたいと思います。 ($) .

何が ($) の型は何でしょうか？Hackageとそのレポートによると、それは

($) :: (a -> b) -> a -> b

しかし、それは100％完全ではありません。それは便利な小さな嘘です。問題は、ポリモーフィック型（例えば a と b を含む)は * . しかし，(ライブラリの)開発者は ($) を持つ型に対してだけでなく * のみならず、種類 # のようなもの、例えば

unwrapInt :: Int -> Int#

一方 Int は種類 * (を持つ（下でもよい）。 Int# は種類 # を持ちます (そして，まったく底になることはできません)。それでも、以下のコードでは型チェックが行われます。

unwrapInt $ 42

これはうまくいかないはずです。の戻り値の型を覚えておいてください。 ($) ? それは多相型であり、多相型は親切な * ではなく # ! では、なぜうまくいったのでしょうか。まず、それは バグ であり、次に ハック (の抜粋）。 ライアン・スコットのメール による ghc-dev メーリングリストでのメール) の抜粋です。

では、なぜこのようなことが起こるのでしょうか？

長い答えは、GHC 8.0より前では、型シグネチャで ($) :: (a -> b) -> a -> b , b 実は親切でなかった * ではなく、むしろ OpenKind . OpenKind はひどいハックで、持ち上げられた（親切な * ) と の両方を可能にします。 # )系が生息するようになり、そのため (unwrapInt $ 42) のタイプチェックを行います。

では、何が ($) の新しい型は何でしょうか？それは

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.

これを理解するために、私たちは Levity :

data Levity = Lifted | Unlifted

さて、ここで考えられるのは ($) には二つの選択肢しかないため、以下のどちらかの型があると考えることができます。 w :

-- pseudo types
($) :: forall a (b :: TYPE   Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b

TYPE は魔法のような定数であり、これは様々な種類の * と # として

type * = TYPE Lifted
type # = TYPE Unlifted

種類に対する数量化 もかなり新しい の一部であり の統合で、Haskell の従属型 .

名前 レビティ多相性 これは，以前のポリモーフィズムの制限では許されなかった，持ち上げられた型と持ち上げられなかった型の両方に対してポリモーフィックな関数を書けるようになったという事実に由来しています．また OpenKind のハックも同時に取り除かれます。この点については、両方の種類を処理することが本当に "just" なのです。

_{ちなみに、この質問はあなただけではありません。偶 Simon Peyton Jones は、Levity の wiki ページが必要だと言っています。 と言っていますし、Richard E. (現在の実装者) も は、wiki ページの更新が必要だと述べ が必要だと述べています。}

リファレンス

• 依存するHaskellのレビティ多相性 Richard A. EisenbergによるICFP 2015に関する講演です。非常におすすめです。
• レビティポリモーフィズム（拡張版） リチャード・A・アイゼンバーグとサイモン・ペイトン・ジョーンズによる
• GHC.Types の一部、つまり ghc-prim ライブラリの一部であり、GHC に同梱されています。
• ディスカッションを行います。
  • のディスカッションは ghc-dev .
  • の議論は ハスケル・カフェ .