[Haskell] dependent types, type class contexts
John D. Barnett
barnett at MIT.EDU
Tue Apr 6 10:48:43 EDT 2004
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
More information about the Haskell
mailing list