如何有效地添加存在类型的安全货币值？

Question

我编写了一个玩具库，它使用依赖类型来表示货币及其类型签名中的货币：

data Currency = CHF | EUR | PLN | USD
  deriving stock (Bounded, Enum, Eq, Read, Show)

data CurrencyWitness (c :: Currency) where
  CHFWitness :: CurrencyWitness CHF
  EURWitness :: CurrencyWitness EUR
  PLNWitness :: CurrencyWitness PLN
  USDWitness :: CurrencyWitness USD

deriving stock instance Eq (CurrencyWitness c)
deriving stock instance Show (CurrencyWitness c)


data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(CurrencyWitness currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

现在我怎样才能写出addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)只有当它们是相同的货币时才能安全地加钱呢？您可以想象，在用户提供货币参数的情况下可能需要这样做，因此我们无法在编译时检查他们的货币。

我最好的方法是：

addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c' _)) = case (c, c') of
  (CHFWitness, CHFWitness) -> Just . SomeMoney $ add m m'
  (PLNWitness, PLNWitness) -> Just . SomeMoney $ add m m'
  -- ...
  (_, _) -> Nothing

这种方法的缺点是编写起来很麻烦、重复，并且当我添加新货币时会出现错误，因为编译器不会警告我这种情况未得到处理。

addSomeMoney (SomeMoney m@(Money c _)) (SomeMoney m'@(Money c _)) = _

不起作用。GHC 抱怨重复c：Conlicting definitions of 'c'。

Answer 1

完全“类型安全”的方法是可能的，但我们必须编写一些样板文件。

我们从OP的代码开始，大部分是逐字的。我们只添加一些扩展，启用警告（这应该在其他地方更正确地完成，但让我们保持简单）和import Data.Typeable.

（我还没有检查是否可以删除某些扩展）

{-# LANGUAGE GADTs, DerivingStrategies, KindSignatures,
    StandaloneDeriving, DataKinds, RankNTypes, 
    TypeApplications, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}
   
import Data.Typeable

data Currency = CHF | EUR | PLN | USD
  deriving stock (Bounded, Enum, Eq, Read, Show)

data CurrencyWitness (c :: Currency) where
  CHFWitness :: CurrencyWitness 'CHF
  EURWitness :: CurrencyWitness 'EUR
  PLNWitness :: CurrencyWitness 'PLN
  USDWitness :: CurrencyWitness 'USD

deriving stock instance Eq (CurrencyWitness c)
deriving stock instance Show (CurrencyWitness c)

data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(CurrencyWitness currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

现在是新的部分。

我们首先“证明”任何货币类型都c满足Typeable约束。这很简单，但需要一些样板文件。

重要的是，添加新货币将触发非详尽的模式匹配警告，因此保持同步相当容易。

withTypeableCurrency :: CurrencyWitness c -> (Typeable c => a) -> a
withTypeableCurrency CHFWitness x = x
withTypeableCurrency EURWitness x = x
withTypeableCurrency PLNWitness x = x
withTypeableCurrency USDWitness x = x

然后是加币功能。我们调用在范围内withTypeableCurrency放置两个Typeable约束。然后我们利用杠杆eqT来检查两种货币类型是否相同。在肯定的情况下，我们不会得到一个无聊的True布尔值，而是一个方便的Refl，它允许编译器识别类型。剩下的就很容易了。

addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney (m1@(Money (c1 :: CurrencyWitness tc1) _)))
             (SomeMoney (m2@(Money (c2 :: CurrencyWitness tc2) _))) =
  withTypeableCurrency c1 $
  withTypeableCurrency c2 $
  case eqT @tc1 @tc2 of
    Just Refl -> Just . SomeMoney $ add m1 m2
    Nothing   -> Nothing  -- not the same type of currency

这种方法的优点是样板文件被限制在 中withTypeableCurrency，并且不必在处理SomeMoney诸如addSomeMoney、subtractSomeMoney等的每个函数中重复。

更新：可以利用该包和一些模板 Haskell 删除一些样板文件singletons。

{-# LANGUAGE GADTs, DerivingStrategies, KindSignatures,
    StandaloneDeriving, DataKinds, RankNTypes, TypeApplications,
    ScopedTypeVariables, TemplateHaskell, EmptyCase, TypeFamilies,
    UndecidableInstances, TypeSynonymInstances, InstanceSigs #-}

import Data.Singletons.Decide
import Data.Singletons.TH

$(singletons [d|
  data Currency = CHF | EUR | PLN | USD
    deriving (Eq, Read, Show, Bounded)
  |])
-- This automatically creates the equivalent of
--    data SCurrency :: Currency -> Type where
--       SCHF :: SCurrency 'CHF
--       SEUR :: SCurrency 'EUR
--       SPLN :: SCurrency 'PLN
--       SUSD :: SCurrency 'USD
-- and some helper stuff.

-- singletons does not like deriving Enum, so we move it here.
deriving stock instance Enum Currency

-- singletons does not create this for some reason.
deriving stock instance Eq (SCurrency c)

data Money (currency :: Currency) representation = Money
  { moneyCurrency :: !(SCurrency currency)
  , moneyAmount :: !representation
  }
  deriving stock (Eq, Show)

add :: (Num r) => Money c r -> Money c r -> Money c r
add (Money witness1 amount1) (Money _ amount2) =
  Money witness1 (amount1 + amount2)

data SomeMoney r where
  SomeMoney :: Money c r -> SomeMoney r

关键功能更简单，利用%~.

addSomeMoney :: (Num r) => SomeMoney r -> SomeMoney r -> Maybe (SomeMoney r)
addSomeMoney (SomeMoney m1@(Money c1 _))
             (SomeMoney m2@(Money c2 _)) =
  -- Check for singleton equality.
  case c1 %~ c2 of
    Proved    Refl -> Just . SomeMoney $ add m1 m2
    Disproved _    -> Nothing