mono-traversable 包对MinLen. 我可以使用链式Succs 构造它们：
toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ Zero)) [Int])
但这很快就会失控：
toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ (Succ (Succ (Succ Zero))))) [Int])
有没有一种方便的方法来构造更大的 Peano 数？我看到 GHC 有一个 TypeLiterals 扩展，但我不确定我是否可以在这里使用它。或者，我可以制作同义词，例如：
type One = Succ Zero
type Two = Succ One
等等; 类似的东西是否已经存在于某个地方？
TypeLits非常适合类型级数字。此外，它很容易仅用于语法糖，并且保持底层特定于库的实现不变。
{-# LANGUAGE
UndecidableInstances, TypeFamilies,
DataKinds, TypeOperators #-}
import qualified GHC.TypeLits as TL
data Nat = Zero | Succ Nat
newtype MinLen (n :: Nat) a = MinLen a
我们必须定义一个将文字转换为数字类型的类型族：
type family Lit (n :: TL.Nat) :: Nat where
Lit 0 = Zero
Lit n = Succ (Lit (n TL.- 1))
现在，您可以Lit n在需要Nat文字时使用。在 GHCi 中：
>:kind! MinLen (Lit 3)
MinLen (Lit 3) :: * -> *
= MinLen ('Succ ('Succ ('Succ 'Zero)))
这种事情有一个包：type-level。这有点吓人，我还没有真正探索过。但是你不应该需要那么大的力量，所以你可以滚动你自己的简单位。
如果你愿意使用UndecidableInstances，事情就很简单了。大约像这样的东西（我不确切知道该库中的 naturals 是如何定义的；如果它不使用DataKinds，您可能必须使用*kind 而不是Natkind，并且您可能必须编写'Succand'Zero而不是Succand Zero- - 我在这方面不太清楚）：
{-# LANGUAGE UndecidableInstances, TypeFamilies, DataKinds, TypeOperators #-}
module TAR where
-- You wouldn't actually use this line, because the library
-- provides the naturals
data Nat = Zero | Succ Nat
-- Digits and Ten to get things started
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
type Six = Succ Five
type Seven = Succ Six
type Eight = Succ Seven
type Nine = Succ Eight
type Ten = Succ Nine
type family Plus (a::Nat) (b::Nat) where
Plus Zero n = n
Plus (Succ m) n = Plus m (Succ n)
type family Times (a::Nat) (b::Nat) where
Times Zero n = Zero
Times (Succ m) n = Plus n (Times m n)
type Decimal (a::[Nat]) = Decimal' a Zero
type family Decimal' (a::[Nat]) (n::Nat) where
Decimal' '[] n = n
Decimal' (a ': bs) n = Decimal' bs (Plus a (Times Ten n))
然后你可以写类似
Decimal '[One, Two, Five]
表示 125。