Haskellで整数を型でパラメータ化する

Question

型ではなく、型の要素、具体的には整数によってパラメータ化されたHaskell型をいくつか作成しようとしています。例えば、R^2の（線形代数）ベクトルとR^3のベクトルは異なる型付きオブジェクトです。具体的には、私はハスケルにK-Dツリーを作成しています.3Dツリーと4Dツリーが異なるタイプになるように、データ構造を正の整数でパラメータ化したいと思います。

私はタプルでツリーをパラメータ化しようとしましたが、どこにも出てこないようです（特にトリプルのようには見えないので、これはやや難しいようです。でもファンクタ（と私のような言うする方法を知らない、インスタンスHomogeneousTuple A =>ファンクタA）私はこのような何かやりたい：。いいだろう、またはこのようなものは次のようになり

data (TupleOfDoubles a) => KDTree a b = ... ---so in a 3DTree a is (Double,Double,Double) 

を同様に良い

data KDTree Int a = ... -- The Int is k, so KDTree has kind Int -> * -> * 

これらのいずれか効果は実行可能か妥当か？

おかげ -Joseph

Answer 1

正確に何をしたいだろうTypeNatsと呼ばれる作業中GHC拡張機能は、あります。しかし、その目標は現在、the ticketによれば7.4.1に設定されているため、少し待っています。

拡張機能が利用できるようになるまでは、タイプを使用して次元をエンコードすることしかできません。例えば、これらの線に沿って何かがうまくいくかもしれない：

{-# LANGUAGE ScopedTypeVariables #-} 
class MyTypeNat a where 
    toInteger :: a -> Integer 

data Zero 
data Succ a 

instance MyTypeNat Zero where 
    toInteger _ = 0 

instance MyTypeNat a => MyTypeNat (Succ a) where 
    toInteger _ = toInteger (undefined :: a) + 1 

data KDTree a b = -- ... 

dimension :: forall a b. MyTypeNat a => KDTree a b -> Integer 
dimension = toInteger (undefined :: a) 

このようなアプローチの欠点は、あなたがKDTree (Succ (Succ (Succ Zero))) Foo代わりのKDTree 3 Fooのようなものを書かなければならないのは勿論です。

Answer 2

sepp2kの答えは、これを行うための基本的なアプローチを示しています。実際、すでに多くの作業が完了しています。

タイプレベル番号パッケージ

• natural-numberとtype-level-natural-number
• numtype
• type-level

自然数のタイプレベルのエンコーディングを使用してスタッフ（例）

• Vec
• Dimensional
• llvm
• ForSyDe

残念ながら

このような何か：

data KDTree Int a = ... 

が実際には不可能です。最終的な型（KDTreeによって構築されます）は、依存型と呼ばれる機能を必要とするIntの値によって異なります。AgdaやEpigramのような言語はこれをサポートしますが、Haskellはサポートしません。