固定长度列表

发表于 分类于 ，

假设有个函数只能处理列表长度为10列表，通常都是在程序运行期间进行判断，
haskell能够实现固定长度的列表类型，使得长度在编译期间就能确定。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
{-# LANGUAGE GADTs, DataKinds #-}

module Lib
    ( someFunc
    ) where

-- 定义一个类型级别的自然数，用来表示栈的大小
data Nat = Z | S Nat  -- Z表示0，S表示后继

-- 定义固定长度的列表类型
data Vec a n where
  VNil  :: Vec a Z            -- 空列表，长度为 0
  VCons :: a -> Vec a n -> Vec a (S n)  -- 非空列表，长度为 n+1

-- 显示固定长度列表
instance Show a => Show (Vec a n) where
  show VNil = "[]"
  show (VCons x xs) = "[" ++ showElem x ++ showRest xs ++ "]"
    where
      showElem :: Show a => a -> String
      showElem = show
      
      showRest :: Show a => Vec a n -> String
      showRest VNil = ""
      showRest (VCons x xs) = ", " ++ showElem x ++ showRest xs

-- 测试用例
someFunc :: IO ()
someFunc = do
  let vec1 :: Vec Int (S (S Z))  -- 长度为2的列表
      vec1 = VCons 1 (VCons 2 VNil)
  print vec1
  
  let vec2 :: Vec Int (S (S (S Z)))  -- 长度为3的列表
      vec2 = VCons 3 (VCons 2 (VCons 1 VNil))
  print vec2

输出结果

1
2
[1, 2]
[3, 2, 1]

嵌套类型

Z和S都是Nat的构造子，S Nat表示一个嵌套结构，列表的长度将通过嵌套的层数表示。

编译器通过判断两个列表的Nat嵌套层数判断是否相同类型，从而实现列表的长度大小判断，而数字类型Int因为是相同类型所以只能是运行期间判断。

1
data Nat = Z | S Nat  -- Z表示0，S表示后继

定义列表

1
2
3
4
-- 定义固定长度的列表类型
data Vec a n where
  VNil  :: Vec a Z            -- 空列表，长度为 0
  VCons :: a -> Vec a n -> Vec a (S n)  -- 非空列表，长度为 n+1

Vec的参数

  • a：列表存储的类型
  • n：长度类型，因为两个构造子VNil和VCons都是返回的Nat类型，所以使用的时候只能构建出Vec a Nat的类型

Vec的两个构造子

  • VNil：生成一个空列表
  • VCons：将a放入Vec a n得到Vec a (S n)，结果的长度类型增加了一层嵌套

语言拓展

因为VNil和VCons都使用了Nat的构造子S和Z而不是Nat类型，所以需要开启DataKinds。

同时因为和VCons需要使用多个参数，需要开启GADT构造更灵活的构造子。