迭代具有不同输入和输出类型的函数答案

【问题标题】：Iterate a function with different input and output types迭代具有不同输入和输出类型的函数
【发布时间】：2020-05-27 17:57:18
【问题描述】：

我有两个函数可以将异构列表向右/向左旋转：

hRotateRight :: (HInit xs, HLast xs) => HList xs -> HList (HLastR xs ': HInitR xs)
hRotateRight xs = hLast xs `HCons` hInit xs

hRotateLeft :: HSnoc xs x => HList (x ': xs) -> HList (HSnocR xs x)
hRotateLeft (x `HCons` xs) = hSnoc xs x

显然，这两个函数都有不同的输入和输出类型（输入是单例时除外）。但是，它们确实具有函数的任何输出也可以是输入的特性，即函数可以被迭代。

我正在 Haskell 中寻找一种类型安全的方法来做到这一点（我不确定这是否可能）。谢谢！

【问题讨论】：

标签： haskell

【解决方案1】：

这是可能的，但通常需要注意的是，Haskell 中的依赖类型编程一旦开始就会充满漏洞。

要多次迭代一个函数，我们首先需要一个数字的概念。最简单的表示是 Peano naturals，具有关联的单例类型，它提供与类型级别 Nats 链接的术语级别值，而仅使用术语级别 Nat 是无法获得的链接。

data Nat = Z | S Nat
data SNat n where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

在类型级别定义迭代旋转。

-- Note: some renaming happened, dropping type classes and reusing the simpler names for type families.

type Rotate1 xs = HLast xs ': HInit xs

type family RotateN n xs where
  RotateN 'Z xs = xs
  RotateN ('S n) xs = RotateN n (Rotate1 xs)

使用它，在术语级别定义迭代旋转，确保遵循与类型级别定义相同的“结构”。

hRotateN :: SNat n -> HList xs -> HList (RotateN n xs)
hRotateN SZ xs = xs
hRotateN (SS n) xs = hRotateN n (hRotateRight xs)

完整要点：https://gist.github.com/Lysxia/fabbf6636f212577e89d507b5380f54d

另请参阅 Introduction to Singletons，Justin Le 的博客系列。

【讨论】：