我可以使用DataKinds编写一个返回参数编码类型的值的函数吗？

否，但是有解决方法。如您所见，您需要编写的类型类似于moneyOf :: (c :: Currency) -> Int -> Money c，在c类型和函数实现本身（moneyOf _ amt = Money amt）中都受约束。这不是我们在Haskell中可以做的事情。那我们该怎么办呢？有两种选择，具体取决于您的实际需求。

选项1：代理。定义多类型

data Proxy (t :: k) = Proxy

这种类型背后的想法是，您可以使用Proxy :: Proxy t一种绕过类型t的术语化表示形式的方式。因此，例如，我们可以定义：

moneyOf :: Proxy c -> Int -> Money c
moneyOf _ = Money

然后，我们可以称其moneyOf (Proxy :: Proxy USD) 10为get Money 10 :: Money USD。您可以使用的技巧是改用给函数指定类型proxy k -> Int -> Money c（请注意小写proxy！），这样proxy可以与任意函数类型统一。¹这对于将参数传递给函数以修复其返回类型非常有用，但实际上并没有。真的不让您做任何其他事情。

正如您所描述的那样，我认为代理可能最适合解决它。（假设普通的类型签名（例如）Money 10 :: Money USD不起作用，也就是说，当您可以使用它们时，它们甚至更简单！）

选项2：单例类型。但是，如果发现您需要更多的通用性（或者您只是好奇），那么另一种方法是创建一个单例类型，如下所示：

data SingCurrency (c :: Currency) where
  SUSD :: SingCurrency USD
  SEUR :: SingCurrency EUR
  SYEN :: SingCurrency YEN

之所以称为“单一类型”，是因为每个SingCurrency c成员只有一个成员（例如，SUSD是type的唯一值SingCurrency USD）。现在，您可以写

moneyOf :: SingCurrency c -> Int -> Money c
moneyOf _ = Money

在这里，moneyOf SUSD 10计算为Money 10 :: Money USD。但是，仅此一项就不会为您带来任何好处（除了打字少了一点）。当您想要生产单例时，它们会特别有趣：

class SingCurrencyI (c :: Currency) where
  sing :: SingCurrency c

instance SingCurrencyI USD where scur = SUSD
instance SingCurrencyI EUR where scur = SEUR
instance SingCurrencyI YEN where scur = SYEN

现在，如果有SingCurrencyI c约束，则可以使用来自动生成相应的SingCurrency c值sing，从而使您可以从类型级别移至术语级别。（请注意，尽管Currencys都是的实例SingCurrencyI，但如果需要，则需要显式指定约束。²）我想不出有什么好的例子来使用它。我认为我的建议是仅在发现自己无法完成所需的情况时使用单例，并且意识到单例的额外类型值同步将对您有帮助（并且在您无法做到的情况下）根据情况重新设计自己）。

如果你发现自己使用的单身，机械是所有设置为你的singletons包，在更一般的情况：有一个数据系列Sing :: k -> *是需要的地方SingCurrency; 并且有一个类型类SingI :: k -> Constraint可以代替SingCurrencyI，它具有单个member sing :: SingI a => Sing a。还有一个功能withSingI :: Sing n -> (SingI n => r) -> r，可让您自由地从Sing n转换为SingI n（另一个方向就是sing）。（这些全部在中提供Data.Singletons。）其中也有一些Template Haskell Data.Singletons.TH，可让您编写

singletons [d|data Currency = USD | EUR | YEN|]

在程序的顶层，以便定义Currency类型以及相应的Sing和SingI实例。（您需要以下语言扩展启用，也：KindSignatures，DataKinds，TypeFamilies，GADTs或ExistentialQuantification，ScopedTypeVariables和TemplateHaskell）。

这真的很强大–如果斜视它，几乎就像依赖类型一样–但是使用起来可能会非常麻烦。的确，如果您想了解更多信息，则有一篇论文在谈论这一话题： Sam Lindley和Conor McBride撰写的“ Hasochism：依赖类型的Haskell编程的乐趣和痛苦”。任何已经在考虑这些想法的人都可以读懂，尽管材料本质上是棘手的。请注意，它们的符号略有不同。不幸的是，我不知道关于这些东西的任何不错的博客文章或教程风格的介绍。

¹不过，我不确定该类型统一规则在类型族中的地位。

²否则，包含的运行时词典sing将不会传入，因此该值在运行时将不可用。