## Type classes and type generator restrictions

Hello LtU. I've been lurking for a while, but this is my first post. I'm not really sure where it ranks on the scale from "how did you get through undergrad without reading X" to "do your own research, dude". I've tried googling everything I can think of, and reading breadth first from Glynn, Stuckey, and Sulzmann's paper "Type classes and constraint
handling rules", but I haven't gotten anywhere. Here goes:

In a Haskell-esque language with Haskell type classes, imagine a type generator, Set. This type generator requires that its argument be an instance of the Equality type class (because otherwise, how could it ensure that its elements are distinct). Set is also an instance of the Haskell Functor type class, because we can map over sets.

With theSet having type Set integer, and a map function with the usual type (namely, (Functor f) => (a -> b) -> F a -> F b), everything seems good. But here's my problem:

map (+) theSet

appears to have the type Set (integer -> integer).

KA-BOOM! Functions aren't in the Equality type class, and so we can't specialize Set at integer -> integer.

Does anyone know how to build a type inference / type checking algorithm that reports this error (statically)? If so, could you point me in the right direction?

## Comment viewing options

### In theory you just need to

In theory you just need to allow class constraints on the type's parameters. From there you propagate those constraints around everywhere. Slight problem: you then need a way to write Functor such that it doesn't mind those constraints. That looks somewhat more like a can of worms.

### These new constraints?

What if I changed the type of map from

map :: (Functor f) => (a -> b) -> f a -> f b

to

map :: ((Functor f) AND (Applicable f a) AND (Applicable f b)) => (a -> b) -> f a -> f b

where Applicable f a means that the type generator f can be applied to the type a.

The only problem I see is that these constraints aren't like the others (Applicable isn't really a multi-parameter type class because its first argument has a higher kind.) Still, it gives an idea of where to go in trying to write CHRs to check it, because rules like:

applicable(set, T) <=> equality(T)

would seem to make lots of sense and have all the normal termination properties.

Thanks.

### No new constraints

I didn't mean a new kind of constraint, the existing variety should work fine!

You'd allow type definitions like this:

data Set (Eq a) => a where ...

With the consequence that you never see Set a without an Eq a constraint (naturally this affects the constructor types too).

Functor's kind effectively changes from the current * -> * to... call it *? -> *, where the ? signifies that the type parameter in question can be constrained (as with Eq a above, for example). If you have rank-n types then the difference between * and *? will crop up elsewhere as well. More generally you're starting to record class 'variances' in kinds, with * as invariant.

An alternative might be to investigate constraint polymorphism instead of constraint subtyping.

### Just when I thought I was getting somewhere

I'm fairly sure I am missing something. The proposed *? kind seems strange, since nothing has that kind. Or are you saying that it decorates the arrow, like * ->? * ?

If I understand the definition properly, at the moment I only have rank-2 types, because the product type generator and the function arrow are the highest kinded things I've decided to care about yet.

Under this idea, what would the type of the map function end up being?

### Apologies to Philippa if I'm off base here, but...

I think the idea is that *? is a kind variable. Consider the kind of Set. It's not * -> *, but EQ -> *, where EQ is the subkind of types that implement equality. As a variable I think it might be better to give it a name, so I'll use *A (imagining *B, *C, etc):

 
class Functor (f :: *A -> *) where
fmap :: ((a :: *A) -> (b :: *A)) -> f a -> f b


The kinds of types a and b in the signature of fmap should probably be inferred from the use of f, so the signature of fmap could be the usual one.

This feels like a can of worms, but I think Philippa's suggestion to restrict the construction of Sets to the appropriate kind of type sounds like "the right way" to proceed.

I'm not sure I understand the question. Here's an example Haskell program:

import Data.Set as S

theSet = S.insert 1 (S.insert 2 (S.insert 3 S.empty))

foo = S.map (+) theSet


...that fails with the following compiler error message in GHC...

setfun.hs:5:6:
No instance for (Ord (a -> a))
arising from use of map' at setfun.hs:5:6-21
Possible fix: add an instance declaration for (Ord (a -> a))
In the expression: map (+) theSet
In the definition of foo': foo = map (+) theSet


...what differences from Haskell are you looking for?

My problem, in Haskell-speak, is that I would like to unify the definition of Prelude.fmap with that of Data.Set.map, and in so doing to make (Functor Data.Set) a valid instance.

*Main> Prelude.fmap (+) theSet

<interactive>:1:0:
No instance for (Functor Set)
arising from use of fmap' at :1:0-22
Possible fix: add an instance declaration for (Functor Set)
In the expression: fmap (+) theSet
In the definition of it': it = fmap (+) theSet


Data.Set doesn't define this instance because (as I understand it) it isn't possible, because there isn't a way to carry the constraint that making a set requires equality (or in the case of Data.Set, ordering) along with the type of fmap.

### No place to put context

Ah, so you want something like this to work...

instance Functor Set where
fmap :: (Ord a, Ord b) => (a -> b) -> (Set a) -> (Set b)
fmap = S.map


Yup.

### Restricted data types

It seems you might want for so-called `Restricted datatypes'

which usually arise in the discussion of how to make Data.Set a
do-notation for them, so using restricted monads is just as convenient
as ordinary ones...

### Thanks! This looks like a

Thanks! This looks like a very promising approach.

### Exactly on topic

That page links to http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps, which as it turns out is exactly on topic.

This forum is amazing, thanks everyone.

### As another functor

Another view would be to say that Set is a functor from the category of Haskell types and Ord-preserving functions between them, so that Setfmap : Ord A, Ord B => (A -> B) -> Set A -> Set B can really be implemented as an homomorphism. I wonder, does Set's map function assume that its functional argument is Ord-respecting (ie, forall x y : A, x <= y -> f x <= f y) ?