安全地從一個矩陣

Question

我已經寫了一個簡單的類型安全的線性代數庫

data Natural where 
    Zero :: Natural 
    Succ :: Natural -> Natural 

type One = Succ Zero 
type Two = Succ One 
type Three = Succ Two 
type Four = Succ Three 

data Vector n e where 
    EmptyVector :: Vector Zero e 
    (:>)  :: e -> Vector n e -> Vector (Succ n) e 

deriving instance Eq e => Eq (Vector n e) 
deriving instance Show e => Show (Vector n e) 

infixr :> 

data Matrix r c e where 
    EmptyMatrix :: Matrix Zero c e 
    (:/)  :: Vector c e -> Matrix r c e -> Matrix (Succ r) c e 

deriving instance Eq e => Eq (Matrix r c e) 
deriving instance Show e => Show (Matrix r c e) 

infixr :/ 

我現在試圖實現的功能如下

dropRow :: Int -> Matrix r c e -> Matrix r c e 

但是，刪除一行，而我的當矩陣的返回值具有不同行數時，部分實現開始拋出錯誤

dropRow i m | i <= 0 = m 
dropRow _ EmptyMatrix = EmptyMatrix 

有沒有辦法保持我的類型，仍然實現這個功能？我會怎麼做？

Answer 1

您給出的dropRow的類型如果應該從矩陣中移除一行，並沒有什麼意義。這一次似乎更好：

dropRow :: Int -> Matrix (Succ r) c e -> Matrix r c e 

鑑於這種情況，你不能真正有離開矩陣不變的情況下，讓我們作出這樣的錯誤，而不是：

dropRow i m | i < 0 = error "invalid row number" 

然後0情況下是相當易：

dropRow 0 (_ :/ m) = m 

的n+1情況下是有點困難，因爲沒有保證的非空矩陣的「尾巴」也是非空的，所以我們需要打出情況下，從其中它有兩個或更多的行的情況下的單排矩陣的：

dropRow i (v :/ EmptyMatrix) = error "invalid row number" 
dropRow i (v :/ m@(_ :/ _)) = v :/ dropRow (i-1) m 

注意dropRow是靜態無法採取一個空矩陣。