ScopedTypeVariables 和 RankNTypes 与 GHC.TypeLits

Posted 2023-03-28

【中文标题】ScopedTypeVariables 和 RankNTypes 与 GHC.TypeLits

【英文标题】：ScopedTypeVariables and RankNTypes with GHC.TypeLits

【发布时间】：2016-08-03 22:38:40

【问题描述】：

我正在尝试将DataKinds 与类型级文字一起使用来创建一个类型安全的货币转换库。到目前为止，我已经定义了这些数据类型：

data Currency (s :: Symbol) = Currency Double
    deriving Show

type USD = Currency "usd"
type GBP = Currency "gbp"

usd :: Double -> USD
usd = Currency

gbp :: Double -> GBP
gbp = Currency

data SProxy (s :: Symbol) = SProxy

还有一个允许我在它们之间进行转换的功能：

convert :: forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> Currency b
convert (Currency a) = case (symbolVal (SProxy :: SProxy a), 
                             symbolVal (SProxy :: SProxy b)) of
          ("usd", "gbp") -> Currency (a * 0.75)
          ("gbp", "usd") -> Currency (a * 1.33)

在这里，我使用ScopedTypeVariables 将约束KnownSymbol a 提供给symbolVal SProxy。这很好用，但是，我希望能够从外部源更新转换率，可能是文本文件或 API，例如 fixer。

显然，我可以将返回类型包装在 IO 中，形成

convert :: forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> IO (Currency b)

但我希望能够保留一个纯 API。我的第一个想法是使用unsafePerformIO 获得转换率图，但这是不安全的，所以我认为我可以使用另一个函数getConvert，其类型为

getConvert :: IO (forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> Currency b)

（即返回 convert 类型函数的 IO 操作）以便它可以像这样使用：

do
    convert <- getConvert
    print $ convert (gbp 10) :: USD

但是，我无法进行类型检查 - GHC 抱怨它：

Couldn't match expected type ‘forall (a :: Symbol) (b :: Symbol). 
                              (KnownSymbol a, KnownSymbol b) => 
                              Currency a -> Currency b’ 
with actual type ‘Currency a0 -> Currency b0’

当我让 GHC 推断 return convert 的类型时，它并没有推断出我想要的类型，而是将 forall a b 移动到了类型检查的 prenex 位置，直到我尝试使用 convert' <- getConvert，在该位置指出它没有说有No instance for (KnownSymbol n0)

我的问题是为什么不进行类型检查，函数getConvert 的正确类型是什么？

首先我认为ScopedTypeVariables 和RankNTypes 使用forall 量词的方式可能不同，但切换RankNTypes 没有效果。我还尝试按照 GHC 的建议将量词移到前面，但这并没有给我所需的 rank-2 类型。

【问题讨论】：

可能相关：***.com/a/38653526/3234959

对了，你看过reflection这个包吗？这闻起来可能有好处。

【参考方案1】：

ImpredicativeTypes 不要 不能真的可以正常工作；避免他们。除了使用IO (forall a. b. ...)，您可以将汇率转换表包装在保留其多态类型的data 类型中。

data ExchangeRates = ExchangeRates 
    getER :: forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> Currency b

并返回IO ExchangeRates

-- getConvert :: IO (forall a b. (KnownSymbol a, KnownSymbol b) => Currency a -> Currency b)
getConvert    :: IO ExchangeRates
getConvert = return (ExchangeRates convert)

几乎按照您的预期使用它。请注意括号将:: USD 类型签名与转换后的值组合在一起。

main = do
    convert <- getER <$> getConvert
    print $ (convert (gbp 10) :: USD)

【讨论】：

IIRC，这使得convert 成为单态：你不能同时在英镑和美元上使用它。要获得完整的多型，需要do c <- getConvert ; let convert :: forall ... ; convert = getEr c ; print (convert ...)

@chi 使用NoMonomorphismRestriction 你可以做到let convert = getER c