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

Question

假设我有一个货币类型:

data Currency = USD | EUR | YEN

和存储 int 的 Money 类型，并由给定的货币参数化(货币被提升为具有 DataKinds 扩展的种类)。

data Money :: Currency -> * where
    Money :: Int -> Money c

能不能写个函数， moneyOf ，它以一个货币值作为其参数，并返回一个由货币值的相应类型参数化的货币值？如 moneyOf :: Currency -> Money c ，但我们得到了编译时间保证 c是从货币值生成的类型吗？

Answer 1

不，但有解决方法。如您所见，您需要编写的类型类似于 moneyOf :: (c :: Currency) -> Int -> Money c ，其中 c 绑定(bind)在类型和函数实现本身( moneyOf _ amt = Money amt )中。这不是我们在 Haskell 中可以做到的。那么我们能做些什么呢？有两种选择，取决于您真正想要的程度。

选项 1:代理。 定义一个poly-kinded类型

data Proxy (t :: k) = Proxy

这种类型背后的想法是，您可以使用 Proxy :: Proxy t 作为传递类型 t 的具体术语级别表示的一种方式。因此，例如，我们可以定义:

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

然后，我们可以像 moneyOf (Proxy :: Proxy USD) 10 一样调用它来获得 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 是类型 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 值，从而允许您从类型级别移动到术语级别。 (请注意，虽然所有 Currency 都是 SingCurrencyI 的实例，但如果需要，您需要明确指定约束。²)我想不出任何使用它的好例子；我认为我的建议是 仅当您发现自己处于无法完成所需的情况时才使用单例，并且意识到单例的额外类型值同步将帮助您 (以及您可以在哪里不要重新设计自己的情况)。

如果您确实发现自己在使用单例，那么机器已经为您设置好了 in the singletons package ，更一般地说:有 a data family Sing :: k -> * 代替了 SingCurrency ；并且有 a type class SingI :: k -> Constraint 代替了 SingCurrencyI ，它具有单个成员 sing :: SingI a => Sing a 。还有 a function withSingI :: Sing n -> (SingI n => r) -> r 允许您从 Sing n 自由转换为 SingI n (另一个方向只是 sing )。 (这些都在 Data.Singletons 中提供。)在 Data.Singletons.TH 中还有一些模板 Haskell 允许您编写

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

在程序的顶层定义 Currency 类型以及适当的 Sing 和 SingI 实例。 (您还需要启用以下语言扩展: KindSignatures 、 DataKinds 、 TypeFamilies 、 GADTs 或 ExistentialQuantification 、 ScopedTypeVariables 和 67)

这真的很强大——如果你眯着眼，它几乎就像依赖类型——但使用起来可能会很痛苦。事实上，如果你想了解更多信息，有一篇论文就是在谈论这个: "Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming" ，作者是 Sam Lindley 和 Conor McBride 。任何已经考虑过这些想法的人绝对可以阅读它，尽管 Material 本质上有点棘手；但是请注意，它们的符号略有不同。不幸的是，我不知道有什么好的博客文章或教程式的介绍来介绍这些东西。

¹不过，我不确定该类型统一规则与类型家族的地位……。

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