Search code examples
haskelltypesghcforall

ScopedTypeVariables and RankNTypes with GHC.TypeLits

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.

Solution

  • ImpredicativeTypes don't can't really work right; avoid them. Instead of using IO (forall a. b. ...) you can wrap the exchange rate conversion table in a data type that preserves its polymorphic type.

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

    and return an IO ExchangeRates instead

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

    And use it almost as you expected. Notice the parenthesis to group the :: USD type signature with the converted value.

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