使用种类和类型操作符的类型级别算术？ [英] Type level arithmetic using kindsignatures and typeoperators?

问题描述

  
 
 { - ＃LANGUAGE DataKinds，KindSignatures，TypeOperators＃ - } 
 import GHC.TypeLits 
 
数组Array（i :: Nat）a = Array {
 num :: Int，
 elems :: [a] 
}派生（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  - >阵列b e  - > Array（a + b）e 
 arrconcat（Array a as）（Array b bs）= Array（a + b）（as ++ bs）
  

in 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]} 
 
 *主要> 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：
无法将'10 + 10'与'20'匹配
预期类型：数组20 Int 
实际类型：Array（10 + 10）Int 
在'（==）'的第一个参数中，即`arr10`arrconcat` arr10'
在表达式中：arr10`arrconcat `arr10 == arr20 
  

有没有办法做我想用这种方法做的事情类型级别的数字，还是计划最终工作？

解决方案

如果您定义类型级别的Peano数字，类型族和数据类型实际上足够强大： （b ::

$ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $' Array {
num :: Int，
elems :: [a]
}派生（Eq，Show）

arrn :: Int - > Array a Int
arrn n = Array n（replicate n 0）

data Nat = Zero | Succ Nat

类型实例添加（n :: Nat）（m :: Nat）:: Nat
类型实例Add Zero m = m
类型实例Add（Succ n） m = Succ（Add nm）

type Ten = Succ（Succ（Succ（Succ（Succ（Succ（Succ（Succ（Succ（Succ Zero）））））））））
型Twenty = Succ（Succ（Succ（Succ（Succ（Succ（Succ（Succ（Succ Succ Succ Succ Succ Succ Succ Succ Succ Succ Succ Zero））））） ）））））））））））））

arr10 :: Array十个Int
arr10 = arrn 10

arr20 :: Array Twenty Int
arr20 = arrn 20

arrconcat :: Array ae - >阵列b e - > Array（Add ab）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>不幸的是， TypeLits 目前有点不足。但正如内森豪威尔已经评论的那样，他们正在努力，在GHC 7.8中应该会更好。这将是伟大的！
 
I was messing around with datakinds in ghc 7.6 and it didn't quite work the way I thought it should.
{-# 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)
in 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
Is there a way to do what I'm trying to do with this sort of type level numeric or is it planned to work eventually? 
解决方案
Type families and data kinds are actually powerful enough to do this if you define type-level Peano numbers like so:
{-# 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)
This works as you'd expect:
*Main> :t arr10 `arrconcat` arr10 == arr20
arr10 `arrconcat` arr10 == arr20 :: Bool
*Main> arr10 `arrconcat` arr10 == arr20
True
Unfortunately the TypeLits are a bit undercooked at the moment. But as Nathan Howell already commented, they are being worked on and should be much better in GHC 7.8. It's going to be great!

                        
这篇关于使用种类和类型操作符的类型级别算术？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！