haskell - 我怎样才能从值到类型？

Question

想象一下，我有以下数据类型和类型类(带有适当的语言扩展):

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 提示无法推断出洗牌的类型。

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

直觉上我觉得应该提到列表的长度。我可以通过 HLength 获取特定 HList 类型的长度类型函数，并通过一些精心选择的约束重写 shuffle 使其听起来不错(至少我认为)。

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

Answer 1

要回答您最初的问题，您不能写这样的 f来自 Int到没有完全依赖类型系统(Haskell 没有)的整数的类型级归纳表示。但是，您在“上下文”中描述的问题在 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 的递归结构由类型类实例中约束的递归结构完全反射(reflect)。

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