haskell - 使用种类签名和类型运算符进行类型级算术？

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

如果您像这样定义类型级皮亚诺数，那么类型族和数据类型实际上足够强大来做到这一点:

{-# 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 中应该会更好。这将会很棒!