[Haskell] dependent types, type class contexts

[John D. Barnett]

Hello-

I'm interested in simulating dependent types in haskell, with the aim of 
operating on (as Oleg put it) "stanamically" sized lists: types reflect 
size constraints, but ultimately need to be resolved from dynamic input. 
I have a good handle on how to do this (read on), but I keep running 
into the same problems related to managing type class contexts. 
Ultimately, I think what I might want is a way of _excluding_ types from 
classes, or declaring classes closed. Much of this is a rehash of what 
others have presented; sorry if I don't give appropriate credit (Oleg, 
Okasaki, Hallgren, ...)

Here's what I want to cover:

- types/classes parallel algebraic data types
- rank-2 polymorphic continuation to simulate dependent types
- stanamically sized lists
- (ditto) as a numeric type
- contexts ?#$%#!!!
- exclusion as a possible solution?

The first part is familiar, and is exemplified in "Fun with Functional 
Dependencies"; this is the parallel between types/classes and algebraic 
data types. Just as we can define a type with values (and an example 
function on that type):

 > data Nat = Zero | Succ Nat
 > toInt :: Nat -> Int
 > toInt Zero = 0
 > toInt (Succ x) = 1 + toInt x

We can have a corresponding definition for a class and types:

 > class NatT a where
 >   toIntT :: a -> Int

 > data ZeroT
 > instance NatT ZeroT where
 >   toIntT ZeroT = 0

 > data SuccT a
 > instance (NatT a) => NatT (SuccT a) where
 >   toIntT (SuccT x) = 1 + toIntT x

(Although functional dependencies can be used to essentially define 
functions/relations at the type level, I don't make use of that here.)

So far so good. But what if I want to dynamically convert from Nat to 
NatT? I'd like a function defined as:

< convert Zero = ZeroT
< convert (Succ x) = SuccT (convert x)

But this isn't legitmate; the return type depends on the input value. So 
first, we need an existential type to capture the return value:

 > data Nat' = forall a . NatT a
 > convert :: Nat -> Nat'

A dependent return value isn't allowed, but we can use a rank-2 
polymorphic continuation to simulate it:

 > convert x = convert_ x Nat'
 > convert_ :: Nat -> (forall a . NatT a => a -> b) -> b
 > convert_ Zero k = k ZeroT
 > convert_ (Succ x) k = convert_ x (\x' -> k (SuccT x'))

By the way, although I've seen a few of you use this trick, is there 
proven theory to back this up-- that rank-2 polymorphism can simulate 
any function with a dependent type by using CPS?

This brings me to lists; I'm actually playing around with nested 
datatypes (a la Okasaki's square matrices), but this suffices to make 
the connection:

 > class ListT a where
 >   map0 :: b -> a b
 >   map1 :: (b -> c) -> a b -> a c
 >   map2 :: (b -> c -> d) -> a b -> a c -> a d
 >   toList :: a b -> [b]

 > data NilT b = NilT
 > instance ListT NilT where
 >   map0 _ = NilT
 >   map1 _ _ = NilT
 >   map2 _ _ _ = NilT
 >   toList _ = []

 > data ConsT a b = ConsT b (a b)
 > instance (ListT a) => ListT (ConsT a) where
 >   map0 x = ConsT x (map0 x)
 >   map1 f (ConsT x xs) = ConsT (f x) (map1 f xs)
 >   map2 f (ConsT x xs) (ConsT y ys) = ConsT (f x y) (map2 f xs ys)
 >   toList (ConsT x xs) = x:(toList xs)

So, for instance, we can have a list

(ConsT 1 (ConsT 2 (ConsT 3 NilT)))::((ConsT (ConsT (ConsT NilT))) Int)

i.e., a list of length 3.

Again, dynamic conversion can be supported by an existential type and 
polymorphic recursion (CPS):

 > data List' b = forall a . ListT a => List' (a b)

 > fromList' :: [b] -> List' b
 > fromList' l = fromList_ l List'

 > fromList_ :: [b] -> (forall a . ListT a => a b -> c) -> c
 > fromList_ [] k = k (NilT)
 > fromList_ (x:xs) k = fromList_ xs (\xs' -> ConsT x xs')

Thus, (fromList' [1,2,3]) should yield the existential version of the 
list above.

It's probably worth mentioning that I define another class method, 
fromList:: (ListT a) => [b] -> Maybe (a b), which only succeeds if the 
input is the correct length. This allows me to write two versions of a 
function: static and dynamic, as:

 > myZip :: (ListT a) => (a b) -> (a c) -> (a (b,c))
 > myZip = map2 (,)

 > myZip' :: [b] -> [c] -> Maybe (List' (b,c))
 > myZip' x y = do (List' x') <- return $ fromList' x  -- convert, unwrap
 >                 y' <- fromList y
 >                 result <- myZip x' y'
 >                 return (List' result)

Type inference forces x' and y' to have the same type; this determines 
at which type fromList is applied, which succeeds or fails depending on 
the size of the input.

I've swept some details under the rug-- see what you need to do to make 
appropriate instances of Show, Eq. This becomes more relevant in trying 
to make a Num instance, so I can have automagically derived vector 
operations. Here's my goal:

 > instance (ListT a, Num b) => Num (a b) where
 >   (+) = map2 (+)
 >   (-) = map2 (-)
 >   (*) = map2 (*)
 >   negate = map1 negate
 >   abs = map1 abs
 >   signum = map1 signum
 >   fromInteger = map0 . fromInteger

This is where things start to get tricky. In order for the above to 
type-check (in ghc 6.2; I understand handling contexts may vary), I need 
to add (Show (a b), Eq (a b)) to the context. What I've elided is that I 
have already provided declarations

 > instance (ListT a, Eq b) => Eq (a b)
 > instance (ListT a, Show b) => Show (a b)

which requires -fallow-overlapping-instances, as e.g., Eq (a b) overlaps 
with [b]. As I get deeper into the numeric type heirarchy, the contexts 
required become increasingly cumbersome; these ultimately make the 
existential type List' useless for any numeric types, and instead 
require me to use (IMHO) overly specified existential types.

  This gets at the crux of my questions:

- Why can't the compiler tell that (ListT a, Num b) is enough to figure 
out the additional context it seems to need?

- Would it be possible to _exclude_ a type from a class, to aviod 
overlapping instances? Perhaps what I want is negation in a type class 
declaration:

< forall a . a /= [] => class ListT a

Alternatively, I'd like to state that the _only_ instances of ListT are 
NilT and ConsT.

Are there definitive references on context resolution (aside from the 
compiler source, which I have not looked at)? Has anyone grappled with 
these problems and come up with satisfactory solutions?

Thanks for your help, and I'm happy to go into more detail. I tried to 
be brief, but, well, I didn't succeed.

-John Barnett