我正在尝试在 Haskell 中为固定长度的列表定义一种类型。当我使用标准方法将自然数编码为一元类型时,一切正常。然而,当我尝试在 GHC 的类型文字上构建所有内容时,我遇到了很多问题。
我对所需列表类型的第一枪是
data List (n :: Nat) a where
Nil :: List 0 a
(:>) :: a -> List n a -> List (n+1) a
不幸的是,它不允许使用类型编写 zip 函数
zip :: List n a -> List n b -> List n (a,b)
我可以通过从类型变量
n
中减去 1 来解决这个问题。类型为 (:>)
:data List (n :: Nat) a where
Nil :: List 0 a
(:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's
接下来,我尝试定义一个附加函数:
append :: List n1 a -> List n2 a -> List (n1 + n2) a
append Nil ys = ys
append (x :> xs) ys = x :> (append xs ys)
不幸的是,GHC 告诉我
Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’
添加约束
((n1 + n2) - 1) ~ ((n1 - 1) + n2)
签名并不能解决问题,因为 GHC 提示Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1))
from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2))
现在,我显然陷入了某种无限循环。
所以,我想知道是否可以使用类型文字为固定长度的列表定义一个类型。我是否可能正是为了这个目的而监督图书馆?基本上,唯一的要求是我想写
List 3 a
之类的东西。而不是 List (S (S (S Z))) a
.
最佳答案
这不是一个真正的答案。
使用 https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2 , 这个
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
import GHC.TypeLits
data List (n :: Nat) a where
Nil :: List 0 a
(:>) :: a -> List n a -> List (n+1) a
append :: List n1 a -> List n2 a -> List (n1 + n2) a
append Nil ys = ys
append (x :> xs) ys = x :> (append xs ys)
...编译,所以显然它是正确的。
关于haskell - 固定长度和类型文字的列表,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/29823345/