Am I thinking about and using singleton types in Haskell correctly?

Question

I want to create several incompatible, but otherwise equal, datatypes. That is, I'd like to have a parameterized type Foo a, and functions such as

bar :: (Foo a) -> (Foo a) -> (Foo a) 

without actually caring about what a is. To clarify further, I'd like the type system to stop me from doing

x :: Foo Int
y :: Foo Char
bar x y

while I at the same time don't really care about Int and Char (I only care that they're not the same).

In my actual code I have a type for polynomials over a given ring. I don't actually care what the indeterminates are, as long as the type system stops me from adding a polynomial in t with a polynomial in s. So far I've solved this by creating a typeclass Indeterminate, and parameterizing my polynomial type as

data (Ring a, Indeterminate b) => Polynomial a b

This approach feels perfectly natural for the Ring part because I do care about which particular ring a given polynomial is over. It feels very contrived for the Indeterminate part, as detailed below.

The above approach works fine, but feels contrived. Especially so this part:

class Indeterminate a where
    indeterminate :: a

data T = T

instance Indeterminate T where
    indeterminate = T

data S = S

instance Indeterminate S where
    indeterminate = S

(and so on for perhaps a few more indeterminates). It feels weird and wrong. Essentially I'm trying to demand that instances of Indeterminate be singletons (in this sense). The feeling of weirdness is one indicator that I might be attacking this wrongly. Another is the fact that I end up having to annotate a lot of my Polynomial a bs since the actual type b often cannot be inferred (that's not strange, but is annoying nevertheless).

Any suggestions? Should I just keep on doing it like this, or am I missing something?

PS: Don't feel offended if I don't upvote or accept answers immediately. I'll be unable to check back in for a few days.

Answer 1

First of all, I'm not sure this:

data (Ring a, Indeterminate b) => Polynomial a b

...is doing what you expect it to. Contexts on data definitions are not terribly useful--see the discussion here for some reasons why, most of which amount to them forcing you to add extra annotations without actually providing many additional type guarantees.

Second, do you actually care about the "indeterminate" parameter other than to ensure that the types are kept distinct? A pretty standard way of doing that sort of thing is what's called phantom types--essentially, parameters in the type constructor that aren't used in the data constructor. You'll never use or need a value of the phantom type, so functions can be as polymorphic as you want, e.g.:

data Foo a b = Foo b

foo :: Foo a b -> Foo a b
foo (Foo x) = Foo x

bar :: Foo a c -> Foo b c
bar (Foo x) = Foo x

baz :: Foo Int Int -> Foo Char Int -> Foo () Int
baz (Foo x) (Foo y) = Foo $ x + y

Obviously this does require annotations, but only in places where you're deliberately adding restrictions. Otherwise, inference will work normally for the phantom type parameter.

It seems to me that the above approach should be sufficient for what you're doing here--the business with singleton types is mostly about bridging the gap between more complicated type-level stuff and regular value-level computations by creating type proxies for values. This could be useful for, say, marking vectors with types that indicate their basis, or marking numeric values with physical units--both cases where the annotation has more meaning than just "an indeterminate called X".