少し前に Haskell 拡張機能の 1 つ (リンクが見つかりません) で、最近 Urで名前 (レコード フィールドなど) が Kind を形成することを発見しました。型の抽象化が十分でない理由を誰か説明できますか?
2 に答える
7
レコードシステムは、値、タイプ、および（多分）種類のルールを定義します。使用されるルールは、設計されている型システムと、設計者が達成したいことによって異なります。
たとえば、Haskellでは、レコードレーベルは次のとおりです。
- 値（アクセサー関数）
- これらの値にはタイプがあります（例
Record -> Int） - それらのタイプには種類があります（
*）
他の記録システムでは、タイプまたは種類のシステムをさまざまな目的に使用できます。
ラベルを別の種類に配置することにより、タイプチェッカーは、自動レンズなどの特別なルール、または汎用機能には当てはまらないレコード構築（おそらく全体）に関連する証明を使用して、ラベルを特別に処理できます。
Haskellでkindシステムを使用する例は、「ボックス化されていない型」の使用です。これらは次のタイプです。
- 通常の値とは異なるランタイム表現
- さまざまなバインディングフォーム（たとえば、ヒープに割り当てることができない）
ボックス化されていない型が通常の型と混ざらないようにするために、それらには異なる種類が与えられます。これにより、コンパイラーはそれらの分離を追跡できます。
したがって、レコードレーベル名には魔法はありません。つまり、レコードレーベルを表すために別の種類を使用する必要があります。これは、言語デザイナーが選択できる選択にすぎません。また、UrやTwelfなどの依存型言語では、次のことができます。便利な区別になります。
于 2012-04-24T11:59:05.627 に答える
7
答えは簡単です: 型に現れるからです。したがって、それらは型レベルで存在する必要があります (そうしないと、依存型が必要になります)。そして、それらはタイプ レベルで生きているため、種類ごとに分類されます。
于 2012-04-24T13:00:06.360 に答える