想在 Haskell 中實作型別安全的矩陣乘法。定義如下：
{-# LANGUAGE TypeFamilies, DataKinds, GADTs #-}
module Vector where
data Nat = Succ Nat | Zero
data Vector (n :: Nat) a where
Nil :: Vector 'Zero a
(:::) :: a -> Vector n a -> Vector (Succ n) a
type Matrix n m a = Vector m (Vector n a)
instance Foldable (Vector n) where
foldr f b (a ::: as) = f a (foldr f b as)
foldr _ b Nil = b
instance Functor (Vector n) where
fmap f (x ::: xs) = f x ::: fmap f xs
fmap _ Nil = Nil
zipV :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipV f (a ::: as) (b ::: bs) = f a b ::: zipV f as bs
zipV f Nil Nil = Nil
最終需要實施
transpose :: Matrix n m a -> Matrix m n a
但我在 Haskell 能做的最好的事情是：
transpose :: Matrix n (Succ m) a -> Matrix (Succ m) n a
transpose (h ::: rest@(_ ::: _)) = zipV (:::) h (transpose rest)
transpose (h ::: Nil) = fmap (::: Nil) h
僅限于 m > 0 因為我無法實作
nils :: {n :: Nat} -> Vector n (Vector Zero a)
切換到 Idris 只是為了練習并且做得更好：
matrix : Nat -> Nat -> Type -> Type
matrix n m a = Vector n (Vector m a)
nils : {n: Nat} -> Vector n (Vector Z a)
nils {n = Z} = Nil
nils {n = S k} = Nil ::: nils
transpose : matrix n m a -> matrix m n a
transpose (h ::: rest) = zipV (:::) h (transpose rest)
transpose Nil = nils
我有實作 nils 的沖動，但是 Haskell 中的型別級編程非常尷尬。我還必須在 Haskell 中對 rest@(_ ::: _) 進行模式匹配，但我在 Idris 中沒有。我怎樣才能實作“零”？
uj5u.com熱心網友回復：
這基本上就是單例的用途。這是一個型別類的價值級別見證，它使您可以訪問這個（概念上冗余的）資訊，每個數字實際上都可以用標準形式來描述。一個最小的實作：
data NatSing n where
ZeroSing :: NatSing Zero
SuccSing :: KnownNat n => NatSing (Succ n)
class KnownNat n where
natSing :: NatSing n
instance KnownNat Zero where natSing = ZeroSing
instance KnownNat n => KnownNat (Succ n) where natSing = SuccSing
現在可以寫了
{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}
nils :: ? n a . KnownNat n => Vector n (Vector Zero a)
nils = case natSing @n of
ZeroSing -> Nil
SuccSing -> Nil ::: nils
轉載請註明出處，本文鏈接：https://www.uj5u.com/shujuku/427242.html