haskell - 使用 kindsignatures 和 typeoperators 的类型级算术？

Question

我在 ghc 7.6 中搞乱了数据类型，但它并没有像我认为的那样工作。

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
import GHC.TypeLits

data Array (i :: Nat) a = Array {
  num :: Int,
  elems :: [a]
} deriving (Eq, Show)

arr10 :: Array 10 Int
arr10 = arrn 10

arr20 :: Array 20 Int
arr20 = arrn 20

arrn :: Int -> Array a Int
arrn n = Array n (replicate n 0)

arrconcat :: Array a e -> Array b e -> Array (a+b) e
arrconcat (Array a as) (Array b bs) = Array (a+b) (as ++ bs)

在 ghci 中：

*Main> arr10 
Array {num = 10, elems = [0,0,0,0,0,0,0,0,0,0]}

*Main> arr10 == arr10
True

*Main> arr20
Array {num = 20, elems = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]}

*Main> arr10 `arrconcat` arr20
Array {num = 30, elems = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]}

*Main> :t arr10 `arrconcat` arr20
arr10 `arrconcat` arr20 :: Array (10 + 20) Int

*Main> :t arr10 `arrconcat` arr10 == arr20
<interactive>:1:1:
    Couldn't match type `10 + 10' with `20'
    Expected type: Array 20 Int
      Actual type: Array (10 + 10) Int
    In the first argument of `(==)', namely `arr10 `arrconcat` arr10'
    In the expression: arr10 `arrconcat` arr10 == arr20

有没有办法做我正在尝试用这种类型级别的数字做的事情，或者它是否计划最终工作？

Answer 1

如果你像这样定义类型级别的 Peano 数，类型族和数据类型实际上已经足够强大了：

{-# LANGUAGE DataKinds, TypeFamilies #-}

data Array (i :: Nat) a = Array {
  num :: Int,
  elems :: [a]
} deriving (Eq, Show)

arrn :: Int -> Array a Int
arrn n = Array n (replicate n 0)

data Nat = Zero | Succ Nat

type family Add (n :: Nat) (m :: Nat) :: Nat
type instance Add Zero m = m
type instance Add (Succ n) m = Succ (Add n m)

type Ten = Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))
type Twenty = Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))

arr10 :: Array Ten Int
arr10 = arrn 10

arr20 :: Array Twenty Int
arr20 = arrn 20

arrconcat :: Array a e -> Array b e -> Array (Add a b) e
arrconcat (Array a as) (Array b bs) = Array (a+b) (as ++ bs)

这如您所料：

*Main> :t arr10 `arrconcat` arr10 == arr20
arr10 `arrconcat` arr10 == arr20 :: Bool
*Main> arr10 `arrconcat` arr10 == arr20
True

不幸的TypeLits是，目前有点未煮熟。但正如 Nathan Howell 已经评论的那样，它们正在开发中，在 GHC 7.8 中应该会更好。会很棒的！