Haskell中实现普通列表到类型级定长ListF的转换方法

你编写的toListF :: [a] -> ListF n a无法通过类型检查的核心原因是：
ListF n a中的长度参数n是编译期确定的类型，这个类型签名等价于forall a n. [a] -> ListF n a，承诺函数可以返回调用方指定的任意长度n对应的定长列表，这在逻辑上不可能实现——普通列表的长度是运行时才确定的值，转换函数只能返回和输入列表实际长度匹配的、某个特定n对应的定长列表，无法满足任意n的要求。
你需要的带存在量词的类型[a] -> exists n. ListF n a确实是正确的类型，Haskell没有原生的存在量词语法，但可以通过两种标准方式实现等价效果。

方案1：存在类型包装 #

通过GADT把长度类型参数封装在新类型内部，对外隐藏具体的长度类型，不需要额外新增扩展，直接复用你已开启的DataKinds/GADTs/KindSignatures即可实现。
完整代码如下：

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Nat = Z | S Nat

data ListF (n :: Nat) a where
    Nil :: ListF 'Z a
    Cons :: a -> ListF m a -> ListF ('S m) a

-- 存在类型包装：对外隐藏长度类型n
data SomeListF a where
  SomeListF :: ListF n a -> SomeListF a

toListF :: [a] -> SomeListF a
toListF [] = SomeListF Nil
toListF (x:xs) = case toListF xs of
  SomeListF rest -> SomeListF (Cons x rest)

使用时通过模式匹配拆包即可，只要传入的操作对任意长度的定长列表都成立，就能正常工作，比如计算定长列表长度：

lenF :: ListF n a -> Int
lenF Nil = 0
lenF (Cons _ rest) = 1 + lenF rest

-- 调用示例：case toListF [1,2,3] of SomeListF l -> lenF l
-- 运行结果为3

方案2：续体传递风格（CPS）模拟存在类型 #

如果不想额外定义包装类型，可以开启RankNTypes扩展，用高秩类型通过续体传递实现和存在类型完全等价的效果：

{-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes #-}

-- Nat和ListF定义和之前一致

toListF :: [a] -> (forall n. ListF n a -> r) -> r
toListF [] k = k Nil
toListF (x:xs) k = toListF xs (\rest -> k (Cons x rest))

调用时直接传入对任意长度定长列表适用的处理函数即可，不需要拆包，比如计算长度的调用写法为：

-- toListF [1,2,3] lenF
-- 运行结果为3

永远不可能写出类型为forall n. [a] -> ListF n a的合法实现，这种类型要求函数可以凭空构造出调用方指定任意长度的列表，逻辑上不成立。

内容的提问来源于stack exchange，提问作者Iván Renison