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?

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.

By Philippa Cowderoy at Thu, 2008-07-24 00:55 | login or register to post comments

These new constraints?

What if I changed the type of map from

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

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.

By Douglas McClean at Thu, 2008-07-24 14:35 | login or register to post comments

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.

By Philippa Cowderoy at Thu, 2008-07-24 16:08 | login or register to post comments

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?

By Douglas McClean at Thu, 2008-07-24 17:51 | login or register to post comments

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.

By Matt M at Fri, 2008-07-25 03:06 | login or register to post comments

Different from Haskell?

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
Failed, modules loaded: none.

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

By Greg Buchholz at Thu, 2008-07-24 20:23 | login or register to post comments

(Possible) Differences from Haskell

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.

By Douglas McClean at Thu, 2008-07-24 20:35 | login or register to post comments

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

By Greg Buchholz at Thu, 2008-07-24 22:00 | login or register to post comments

Yup.

By Douglas McClean at Thu, 2008-07-24 22:13 | login or register to post comments

Restricted data types

It seems you might want for so-called `Restricted datatypes'
http://okmij.org/ftp/Haskell/types.html#restricted-datatypes

which usually arise in the discussion of how to make Data.Set a
monad. Your problem (making Set a functor) seems quite similar. The
answer is that Set is not a monad; however, it is a restricted monad
(a generalization of monads: all ordinary monads are restricted
monads). Incidentally, GHC already supports restricted monads and the
do-notation for them, so using restricted monads is just as convenient
as ordinary ones...

By Oleg at Fri, 2008-07-25 08:47 | login or register to post comments

Thanks! This looks like a

Thanks! This looks like a very promising approach.

By Douglas McClean at Fri, 2008-07-25 15:32 | login or register to post comments

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.

By Douglas McClean at Fri, 2008-07-25 16:18 | login or register to post comments

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) ?

By Matthieu Sozeau at Mon, 2008-07-28 09:02 | login or register to post comments

Lambda the Ultimate

User login

Navigation