小编313*_*13H的帖子

我已经定义了一个向量:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}
data Nat = Z | S Nat

type family (+) (n :: Nat) (m :: Nat) :: Nat
type instance Z     + m = m
type instance (S n) + m = S (n + m)

type family (*) (n :: Nat) (m :: Nat) :: Nat
type instance Z * m = Z
type instance (S n) * m = n * m + m

data Vec (n :: Nat) …