依賴鍵入'ZipVector'Applicatives

Question

我已經爲有限的Vector創建了一個「ZipVector」風格Applicative，它使用求和類型將有限向量粘合到對「無限」向量建模的Unit。

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 

這大概是足以滿足我的需求，但我懶懶地想「固定尺寸」一個仿照可適用的情況下，你可以依賴輸入「矢量」 S獲得。

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 

其中d幻象參數是一個類型級Nat。我如何（如果可能的話）在Haskell中編寫reifiedDimension？此外，如果再有可能，給予(Point v1) :: Point d1 a和(Point v2) :: Point d2 a我怎樣才能得到length v1 == length v2我能得到d1 ~ d2？

Answer 1

我如何（如果有可能）在Haskell中寫入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？

With Data.Vector，no。你需要一個矢量類型來編碼類型的長度。你可以做的最好的就是自己維護它，並通過不輸出Point構造函數來封裝它。