注目★★★★★Lobsters
Haskell の dependent types 実装、GADT で見える forall に対応
30秒で把握
- 1GHC 9.14 で RequiredTypeArguments により GADT 内の forall a -> ty 構文をサポート
- 2型引数と値引数をコンストラクタで明示的に混在・AST 改造と型チェッカー更新で実現
- 3namespace-specified imports (type .., data ..) で型名/値名の曖昧性を解消・dependent types の基盤整備進行中
要約
Serokell の GHC チームが Dependent Haskell の実装進捗を報告した。GADT で forall a -> ty (visible dependent quantification) を GHC 9.14 の RequiredTypeArguments 拡張で実装し、型引数と値引数を明示的に混在させられるようになった。実装には AST 構造の変更、型チェッカーの更新、Core 表現の拡張が必要だったが、これにより型と項を自由に混在させる基盤が整備された。さらに namespace-specified imports により、型名と値名が重複する場合の曖昧さを解消するための文法 (type.., data..) も導入された。複数の補助機能 (Tuple 型族、pun 検出、HsType/HsExpr の統一進捗) も同時に整備され、practical dependent types へ一歩近づいた。
あなたへの影響
dependent types の実装は Haskell の型安全性を大きく拡張する可能性を持つが、本報告は中間的な段階 (erasable な visible forall) に過ぎません。
推奨：実用 dependent types (foreach a -> ty) はまだ先で、今後の複雑さが増す実装過程を注視する価値があります。