如何编写仅接受长度大于/小于2的长度索引向量的Haskell函数？

你已经实现了接受长度恰好为2的Vec的函数，要实现接受长度大于或小于2的Vec，核心是在类型层面定义自然数的大小关系约束，让编译器在编译期就检查向量长度是否符合要求。

步骤1：定义大小关系的类型类 #

我们可以通过归纳的方式定义Gt（大于）和Lt（小于）类型类，用类型实例来描述自然数的大小规则：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
module Main where 

data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One
type Three = S Two

-- 长度索引向量定义
data Vec :: Nat -> * -> * where
  Nil  :: Vec Z a
  (:>) :: a -> Vec n a -> Vec (S n) a 

-- 定义"大于"关系的类型类
class Gt (n :: Nat) (m :: Nat)
-- 规则1：任何非零自然数都大于零
instance Gt (S n) Z
-- 规则2：若n > m，则S n > S m
instance Gt n m => Gt (S n) (S m)

-- 定义"小于"关系的类型类
class Lt (n :: Nat) (m :: Nat)
-- 规则1：零小于任何非零自然数
instance Lt Z (S m)
-- 规则2：若n < m，则S n < S m
instance Lt n m => Lt (S n) (S m)

步骤2：实现带长度约束的函数 #

基于上面的类型类，就可以写出你期望的带Gt l Two约束的函数，因为编译器会确保传入的向量长度一定大于2，所以模式匹配是安全的：

-- 接受长度大于2的Vec，返回第一个元素
f :: Gt l Two => Vec l a -> a
f (e :> _ :> _) = e  -- 长度>2意味着至少有3个元素，匹配不会失败

-- 接受长度小于2的Vec，返回第一个元素的Maybe值（处理长度为0的情况）
g :: Lt l Two => Vec l a -> Maybe a
g Nil = Nothing
g (e :> Nil) = Just e

验证示例 #

你可以用以下代码测试：

test1 :: Int
test1 = f (1 :> 2 :> 3 :> Nil)  -- 长度为3，符合Gt Two约束，编译通过

test2 :: Maybe Int
test2 = g (5 :> Nil)  -- 长度为1，符合Lt Two约束，编译通过

-- test3 = f (1 :> 2 :> Nil)  -- 长度为2，不符合Gt Two约束，编译报错
-- test4 = g (1 :> 2 :> 3 :> Nil)  -- 长度为3，不符合Lt Two约束，编译报错

补充说明 #

如果你不想手动定义大小关系，也可以使用Haskell标准库Data.Type.Natural中的CmpNat类型家族，通过CmpNat l Two ~ 'GT来表示l > Two，效果是一样的，但手动定义类型类更直观，适合理解类型级编程的逻辑。

内容的提问来源于stack exchange，提问作者Evg