依存型指定された「ZipVector」Applicatives

Question

私は自分自身 Unitのモデル「無限」のベクトルに有限のベクトルを接着するために和タイプを使用して、有限 Vector Sの「 ZipVector」スタイル Applicative作りました

。

data ZipVector a = Unit a | ZipVector (Vector a) 
      deriving (Show, Eq) 

instance Functor ZipVector where 
    fmap f (Unit a) = Unit (f a) 
    fmap f (ZipVector va) = ZipVector (fmap f va) 

instance Applicative ZipVector where 
    pure = Unit 
    Unit f <*> p  = fmap f p 
    pf  <*> Unit x = fmap ($ x) pf 
    ZipVector vf <*> ZipVector vx = ZipVector $ V.zipWith ($) vf vx 

これはおそらく、私のニーズには十分だろうが、私はぼんやりあなたが依存して入力した「ベクトル」ので得ることができますApplicativeのインスタンスをモデルにした「固定次元」ものを望んでいました。 dファントムパラメータがタイプレベルNatある

data Point d a = Point (Vector a) deriving (Show, Eq) 

instance Functor (Point d) where 
    fmap f (Point va) = Point (fmap f va) 

instance Applicative Point where 
    pure = Vector.replicate reifiedDimension 
    Point vf <*> Point vx = Point $ V.zipWith ($) vf vx 

。可能であれば、私はHaskellにreifiedDimensionを書き込むことができますか？さらに、可能であれば、(Point v1) :: Point d1 aと(Point v2) :: Point d2 aを入手するにはどうすればlength v1 == length v2を入手できますか？d1 ~ d2を入手できますか？

Answer 1

ハスケルでどうすればいいですか（可能な場合）reifiedDimension？

GHC.TypeLitsとScopedTypeVariablesの使用：

instance SingI d => Applicative (Point d) where 
    pure = Point . Vector.replicate reifiedDimension 
    where reifiedDimension = fromInteger $ fromSing (sing :: Sing d) 
    ... 

がいっぱい例えばmy answer hereを参照してください。

また、再び可能な場合は、(Point v1) :: Point d1 aと(Point v2) :: Point d2 a与えられたどのように私はlength v1 == length v2は私がd1 ~ d2を得ることができます得ることができますか？

Data.Vectorといいます。型の長さをエンコードするベクトル型が必要です。あなたができることは、これを自分自身で維持し、Pointコンストラクタをエクスポートしないことでカプセル化することです。 `D ::歌う（Vector.length V）を反映>ポイントdがA`` -