在Haskell中将具有已知长度的列表转换为嵌套对的最简单方法是什么？

Question

如何将具有已知长度的列表转换为嵌套对？换句话说,填充下面的类型孔最方便的方法是什么？

_ [1,2]       :: (Int,Int)
_ [1,2,3]     :: ((Int,Int),Int)
_ [1,2,3,4]   :: (((Int,Int),Int),Int)
_ [1,2,3,4,5] :: ((((Int,Int),Int),Int),Int)

---

编辑:请注意,类型孔不必是相同的功能,我正在寻找一个方便的模式(如果存在方便的模式)来填补空洞.

Answer 1

也许是这样的:

step f xs = (f (init xs), last xs)
len1 = head
len2 = step len1
len3 = step len2
len4 = step len3

在ghci:

*Main> len4 [1..4]
(((1,2),3),4)

当然也可以通过模式匹配直接实现这些功能之一:

len4' [a,b,c,d] = (((a,b),c),d)

这也不会像有元素一样遍历列表,这很好.

Answer 2

与依赖类型的版本一起使用.首先,让我们完成样板:

{-# LANGUAGE
  TemplateHaskell, DataKinds, ScopedTypeVariables,
  FlexibleInstances, PolyKinds, TypeOperators,
  TypeFamilies, GADTs, UndecidableInstances #-}

import Data.Singletons.TH
import qualified GHC.TypeLits as Lit

$(singletons [d| data Nat = Z | S Nat deriving (Eq, Show) |])

这里使用TH纯粹是为了减少样板,我们不会在实际代码中使用TH.实际上,上面的内容可以(并且应该)在某个地方的一个包中被考虑(在写这个答案的时候,没有这样的包具有最新的singletons依赖性).

tuplify成为一个函数,其返回类型取决于Nat参数.

type family NTup n a where
  NTup (S (S Z))     a = (a, a)
  NTup (S (S (S n))) a = (NTup (S (S n)) a, a)

tuplify :: Sing n -> [a] -> NTup n a
tuplify n as = go n (reverse as) where
  go :: Sing n -> [a] -> NTup n a
  go (SS (SS SZ))     [a, b] = (b, a)
  go (SS (SS (SS n))) (a:as) = (go (SS (SS n)) as, a)
  go _                _      = error "tuplify: length mismatch"

尝试一下:

tuplify (SS (SS (SS SZ))) [1, 2, 3] -- ((1, 2), 3)

现在写出自然是非常艰巨的,所以让我们介绍一些语法糖:

type family N n where
  N 0 = Z
  N n = S (N (n Lit.- 1))

type SN n = Sing (N n)

现在:

tuplify (sing:: SN 10) [1..10] -- (((((((((1,2),3),4),5),6),7),8),9),10)

作为旁注,如果我们将空列表转换为()(从而也允许单元素嵌套元组),我们的定义会变得更加自然:

type family NTup n a where
  NTup Z     a = ()
  NTup (S n) a = (NTup n a, a)

tuplify :: Sing n -> [a] -> NTup n a
tuplify n = go n . reverse where
  go :: Sing n -> [a] -> NTup n a
  go SZ     []     = ()
  go (SS n) (a:as) = (go n as, a)
  go _      _      = error "tuplify: length mismatch"

tuplify (sing:: SN 5) [1..5] -- ((((((),1),2),3),4),5)