我想要一個張量資料結構
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
-- | A list of type a and of length n
data ListN a (dim :: Nat) where
Nil :: ListN a Zero
Cons :: a -> ListN a n -> ListN a (Succ n)
data Tensor a where
Dense :: ListN a n -> ListN Int Nat -> Tensor a
張量由元素串列和表示張量維度的整數串列表示。例如 ListN 中的 [3,4,5,6] 意味著您有 4 個維度，每個維度分別是 3、4、5 和 6 個元素長。但是現在我希望第一個 ListN 中的 n 取決于存盤在第二個 ListN 中的所有整數的乘積，因為這是我可以在第一個 ListN 中擁有的元素數量。但是我該怎么做呢？
uj5u.com熱心網友回復：
為此，您需要為您的Tensor型別提供一個型別級別的維度向量，而不僅僅是一個ListN Int Nat值，因此最好Tensor使用dims型別引數進行定義。您可能還會發現首先使用尺寸，然后使用元素型別更方便，例如：
data ListN (dim :: Nat) a where
Nil :: ListN Zero a
Cons :: a -> ListN n a -> ListN (Succ n) a
infixr 5 `Cons`
data Tensor (dims :: [Nat]) a where
Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
這里缺少的Product是一個型別級別的函式來乘以維度。多個 Peano naturals 有點乏味，但以下作業：
type family Plus m n where
Plus (Succ m) n = Plus m (Succ n)
Plus Zero n = n
type family Times m n where
Times (Succ m) n = Plus n (Times m n)
Times Zero n = Zero
type family Product (dims) where
Product '[] = Succ Zero
Product (m : ns) = Times m (Product ns)
之后，進行以下型別檢查。請注意，我在上面創建了Cons一個infixr運算子以避免大量括號：
t1 :: Tensor '[Succ Zero, Succ (Succ Zero), Succ (Succ (Succ Zero))] Int
t1 = Dense (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` 5 `Cons` 6 `Cons` Nil)
如果元素個數不對，則約束失敗，所以下面不做型別檢查：
t2 :: Tensor '[Succ Zero, Succ (Succ Zero), Succ (Succ (Succ Zero))] Int
t2 = Dense (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` 5 `Cons` Nil)
完整的例子：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
data ListN (dim :: Nat) a where
Nil :: ListN Zero a
Cons :: a -> ListN n a -> ListN (Succ n) a
infixr 5 `Cons`
data Tensor (dims :: [Nat]) a where
Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
type family Plus m n where
Plus (Succ m) n = Plus m (Succ n)
Plus Zero n = n
type family Times m n where
Times (Succ m) n = Plus n (Times m n)
Times Zero n = Zero
type family Product (dims) where
Product '[] = Succ Zero
Product (m : ns) = Times m (Product ns)
-- type checks
t1 :: Tensor '[Succ Zero, Succ (Succ Zero), Succ (Succ (Succ Zero))] Int
t1 = Dense (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` 5 `Cons` 6 `Cons` Nil)
-- won't type check
t2 :: Tensor '[Succ Zero, Succ (Succ Zero), Succ (Succ (Succ Zero))] Int
t2 = Dense (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` 5 `Cons` Nil)
如評論中所述，有一個內置的非 PeanoNat型別，您可能會發現它更易于使用。重寫為使用它，代碼如下所示：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
data ListN (dim :: Nat) a where
Nil :: ListN 0 a
Cons :: a -> ListN n a -> ListN (1 n) a
infixr 5 `Cons`
data Tensor (dims :: [Nat]) a where
Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
type family Product dims where
Product '[] = 1
Product (m : ns) = m * Product ns
-- type checks
t1 :: Tensor '[1,2,3] Int
t1 = Dense (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` 5 `Cons` 6 `Cons` Nil)
-- won't type check
t2 :: Tensor '[1,2,3] Int
t2 = Dense (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` 5 `Cons` Nil)
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/452948.html