6

假设我有一个货币类型：

data Currency = USD | EUR | YEN

以及存储 int 的 Money 类型，并由给定的 Currency 参数化（Currency 被提升为具有 DataKinds 扩展名的种类）。

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

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

4

2 回答 2

9

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

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

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是 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，它具有单个成员sing :: SingI a => Sing a。还有一个功能withSingI :: Sing n -> (SingI n => r) -> r可以让您自由转换 from Sing ninto SingI n（另一个方向是 just sing）。（这些都在 中提供Data.Singletons。）还有一些 Template HaskellData.Singletons.TH允许您编写

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

在程序的顶层，以便定义Currency类型以及适当的Sing和SingI实例。（您还需要启用以下语言扩展：KindSignatures、、、或DataKinds、、TypeFamilies和。）GADTsExistentialQuantificationScopedTypeVariablesTemplateHaskell

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

¹我不确定该类型统一规则与类型族的状态，但是……。

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

于 2015-02-02T19:13:09.187 回答
1

Antal SZ 答案的选项 2 的替代方案如下。

你保留Currency单例SingCurrency。

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

SingCurrencyI但是，您可以使用存在的 GADT，而不是使用单例实例类 ( )。

data AnyCurrency where
    AnyCurrency :: SingCurrency sc -> AnyCurrency

具有代替SingCurrencyI实例的辅助功能。

anyCurrency :: Currency -> AnyCurrency
anyCurrency EUR = AnyCurrency SEUR
anyCurrency USD = AnyCurrency SUSD
anyCurrency YEN = AnyCurrency SYEN

使用

money :: SingCurrency c -> Int -> Money c
money = const Money

和存在主义Money

data AnyMoney where
    AnyMoney :: Money c -> AnyMoney

你可以实施

moneyOf :: Currency -> Int -> AnyMoney
moneyOf c v = case anyCurrency c of
                AnyCurrency sc -> AnyMoney $ money sc v

模式匹配AnyMoney将允许您使用带有类型参数的函数Money c，即

useMoney :: Money c -> IO ()
useMoney = undefined

最终会得到你

useUseMoney :: Currency -> Int -> IO ()
useUseMoney c v = case moneyOf c v of
                    AnyMoney m -> useMoney m
于 2015-02-02T20:32:22.733 回答