1

I'm trying to use DataKinds along with type-level literals to make a type safe currency conversion library. So far I have defined these data types:

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

Along with a function that allows me to convert between them:

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)

Here, I have used ScopedTypeVariables to supply the constraint KnownSymbol a to symbolVal SProxy. This works fine, however, I would like to be able to make the conversion rates update from an external source, perhaps a text file or an API such as fixer.

Obviously, I could just wrap the return type in IO, forming

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

but I would like to be able to keep a pure API. My first thought was to have the conversion rate map be obtained using unsafePerformIO, but this is unsafe so I instead thought I could use another function getConvert with a type to the effect of

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

(i.e an IO action returning a convert type function) so that it could be used like this:

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

However, I have been unable to get this to type check - GHC complains that it:

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’

When I had GHC infer the type of return convert, it did not infer the type I wanted but instead moved the forall a b to the prenex position, which type checks, until I try to use convert' <- getConvert, at which point it fails saying that there is No instance for (KnownSymbol n0)

My question is why does this not type check, and what would be the correct type for the function getConvert?

First I thought that it may be the fact both ScopedTypeVariables and RankNTypes use the forall quantifier in different ways, but toggling RankNTypes has had no effect. I also tried moving the quantifier to the front as GHC suggested but this does not give me the rank-2 type that I need.

4

1 回答 1

3

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)
于 2016-08-03T23:27:13.543 回答