时间戳

首页 > 解决方案 > 迭代具有不同输入和输出类型的函数

haskell - 迭代具有不同输入和输出类型的函数

问题描述

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

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

解决方案

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

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

另请参阅Justin Le 的博客系列介绍 Singletons 。

推荐阅读