9

想象一下，我有以下数据类型和类型类（带有适当的语言扩展）：

data Zero=Zero
data Succ n = Succ n
class Countable t where
      count :: t -> Int
instance Countable Zero where
      count Zero = 0

instance (Countable n) => Countable (Succ n) where
      count (Succ n) = 1 + count n

是否可以编写一个函数，从整数中为我提供正确类型类实例的实例？基本上，一个函数f使得count (f n) = n

我的尝试是以下变体，但这在编译时给了我一些类型错误：

f::(Countable k)=> Int -> k
f 0 = Zero
f n = Succ $ f (n-1)

在寻找解决方案时，我经常讨论依赖类型，但我还没有能够将这些讨论映射到我的用例。

背景：因为我意识到这会得到很多“你为什么要这样做”类型的问题......

我目前正在使用该Data.HList包来处理异构列表。在这个库中，我想构建一个函数shuffle，当给定一个整数时n，它会将n列表的第 th 个元素移到末尾。

例如，如果我有l=1:"Hello":32:500，我想shuffle 1 l给1:32:500:"Hello"。

我已经能够编写专门的函数shuffle0来回答用例shuffle 0：

shuffle0 ::(HAppend rest (HCons fst HNil) l')=>HCons fst rest -> l'
shuffle0 (HCons fst rest) = hAppend rest (HCons fst HNil)

我还编写了这个函数next来“包装”一个函数，例如next (shuffle n) = shuffle (n+1)：

next :: (forall l l'. l -> l') -> (forall e l l'.(HCons e l) -> (HCons e l'))
next f = \(HCons e l)-> HCons e  $ (f l)

我觉得我的类型签名可能无济于事，即没有长度编码（这是可能出现问题的地方）：

shuffle 0=shuffle0
shuffle n= next (shuffle (n-1))

GHC 抱怨无法推断出洗牌的类型。

这并不让我感到惊讶，因为该类型可能不是很有根据。

直觉上我觉得应该提到列表的长度。我可以通过 type 函数获得特定 HList 类型的长度HLength，并通过一些精心选择的约束重写 shuffle 以使其合理（至少我认为）。

问题是我仍然需要获得我选择的长度的类型级别版本，以便我可以在调用中使用它。我什至不确定这是否可行，但我觉得我会有更好的机会。

4

1 回答 1

6

要回答您最初的问题，如果没有完整的依赖类型系统（Haskell 没有），您将无法编写这样的ffrom到整数的类型级归纳表示。Int但是，您在“上下文”中描述的问题在 Haskell 中不需要这样的功能。

我相信以下内容大致是您正在寻找的内容：

 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, FunctionalDependencies, UndecidableInstances #-}

 import Data.HList

 data Z = Z
 data S n = S n

 class Nat t
 instance Nat Z
 instance Nat n => Nat (S n)

 class (Nat n, HList l, HList l') => Shuffle n l l' | n l -> l' where
     shuffle :: n -> l -> l'

 instance Shuffle Z HNil HNil where
     shuffle Z HNil = HNil

 instance (HAppend xs (HCons x HNil) ys, HList xs, HList ys) => Shuffle Z (HCons x xs) ys where
     shuffle Z (HCons x xs) = hAppend xs (HCons x HNil)

 instance (Shuffle n xs ys) => Shuffle (S n) (HCons x xs) (HCons x ys) where
     shuffle (S n) (HCons x xs) = HCons x (shuffle n xs)

例如

 *Main> shuffle (S Z) (HCons 1 (HCons "Hello" (HCons 32 (HCons 500 HNil))))
 HCons 1 (HCons 32 (HCons 500 (HCons "Hello" HNil)))

这个定义背后的一般技术是首先考虑如何编写非依赖类型的版本（例如这里，如何将元素打乱到列表的末尾），然后将其转换为类型级别（约束）版本。请注意，shuffle类型类实例中约束的递归结构完全反映了 的递归结构。

这是否解决了您正在尝试做的事情？

于 2013-01-30T10:08:39.603 回答