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
_______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
