Can I write a function using DataKinds that returns a value of type encoded by the parameter?

Question

Let's say I have a Currency type:

data Currency = USD | EUR | YEN

and a Money type that stores an int, and is parameterized by a given Currency (Currency is promoted to a kind with the DataKinds extension).

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

Is it possible to write a function, moneyOf, that takes as its parameter, a Currency value, and returns a Money value which is parameterized by the corresponding type of the Currency value? Such as moneyOf :: Currency -> Money c, but we get a compile time guarantee that c is the type generated from the Currency value?

Answer 1

No, but there are workarounds. As you saw, the type you'd need to write is something like moneyOf :: (c :: Currency) -> Int -> Money c, where c is bound both in the type and in the function implementation itself (moneyOf _ amt = Money amt). This isn't something we can do in Haskell. So what can we do instead? There are two options, depending on how much you really want.

Option 1: Proxies. Define a poly-kinded type

data Proxy (t :: k) = Proxy

The idea behind this type is that you can use Proxy :: Proxy t as a way of passing around a reified term-level representation of the type t. So, for instance, we can define:

moneyOf :: Proxy c -> Int -> Money c
moneyOf _ = Money

Then, we can call it like moneyOf (Proxy :: Proxy USD) 10 to get Money 10 :: Money USD. A trick you can use is to instead give the function the type proxy k -> Int -> Money c instead (note the lowercase proxy!), so that proxy will unify with arbitrary function types.¹ This is great for passing arguments to functions in order to fix their return types, but it doesn't really let you do anything beyond that.

As you've described your problem, I think proxies are probably the best fit for solving it. (Assuming that plain type signatures, like Money 10 :: Money USD, don't work, that is – those are even simpler when you can use them!)

Option 2: Singleton types. However, if you find that you need more generality (or if you're just curious), then another approach is to create a singleton type like the following:

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

This is called a "singleton type" because each SingCurrency c has only one member (e.g., SUSD is the unique value of type SingCurrency USD). Now, you can write

moneyOf :: SingCurrency c -> Int -> Money c
moneyOf _ = Money

Here, moneyOf SUSD 10 evaluates to Money 10 :: Money USD. But this alone doesn't buy you anything beyond using (except a bit less typing). Singletons get particularly fun when you want to produce them:

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

Now, if you have a SingCurrencyI c constraint, you can automatically produce the corresponding SingCurrency c value with sing, thus allowing you to move from the type level to the term level. (Note that, although all Currencys are instances of SingCurrencyI, you need to specify the constraint explicitly if you want it.²) I can't think of any good examples of using this off the top of my head; I think my suggestion would be to use singletons only if you find yourself in a situation where you realize you can't accomplish what you need, and realize that the extra type-value synchronization of singletons would help you (and where you can't redesign yourself out of the situation).

If you do find yourself using singletons, the machinery is all set up for you in the singletons package, in more generality: there's a data family Sing :: k -> * that takes the place of SingCurrency; and there's have a type class SingI :: k -> Constraint that takes the place of SingCurrencyI, which has the single member sing :: SingI a => Sing a. There's also a function withSingI :: Sing n -> (SingI n => r) -> r which allows you to convert freely from Sing n into SingI n (the other direction is just sing). (These are all provided in Data.Singletons.) There's also some Template Haskell in Data.Singletons.TH that allows you to write

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

at the top level of your program in order to define the Currency type along with the appropriate Sing and SingI instances. (You need the following language extensions enabled, too: KindSignatures, DataKinds, TypeFamilies, GADTs or ExistentialQuantification, ScopedTypeVariables, and TemplateHaskell.)

This is really powerful – it's almost like dependent types, if you squint – but it can be a massive pain to use. Indeed, if you want more information, there's a paper talking about exactly that: "Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming", by Sam Lindley and Conor McBride. It's definitely readable by anybody who's thinking about these ideas already, although the material is sort of intrinsically tricky; be warned that their notation is slightly different, though. I don't, unfortunately, know of any good blogpost or tutorial-style introductions to this stuff.

---

¹ I'm uncertain about the status of that type unification rule with type families, though….

² Otherwise, the run-time dictionary containing sing won't be passed in, so the value wouldn't be available at run-time.

Answer 2

An alternative to option 2 of Antal S-Z's answer is the following.

You keep the Currency singletons SingCurrency.

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

But instead of using a singleton instance class (SingCurrencyI) you can use an existential GADT.

data AnyCurrency where
    AnyCurrency :: SingCurrency sc -> AnyCurrency

with an auxiliary function that takes the place of the SingCurrencyI instances.

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

Using

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

and an existential Money

data AnyMoney where
    AnyMoney :: Money c -> AnyMoney

you can implement

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

Pattern matching on AnyMoney will let you use functions taking an argument of type Money c, i.e.

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

will finally get you

useUseMoney :: Currency -> Int -> IO ()
useUseMoney c v = case moneyOf c v of
                    AnyMoney m -> useMoney m