Patrick Browne wrote:

Thank you for your clear an detailed reply, the work on dependent types seems to address my needs. However it is beyond my current research question, which is quite narrow(see[1]). I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification*. I do not wish to address any perceived weakness, I merely wish to identify them (if there are ant). Of course my question may be ill conceived, in that type classes were intended to specify interfaces and not algebraic types.

Oh, now I get what you really want. You want to specify not only the captured operations, but also assumptions about them. This is not impossible in Haskell, but in most cases you will need at least some form of lightweight dependent types. However, this can only prove certain properties, which are not dependent on the functions themselves, but only their types. Here is a variant of Stacklike that does static length checks (GHC 7.4 required): {-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes #-} data Nat = Z | S Nat data Stack :: Nat -> * -> * where Empty :: Stack Z a Push :: a -> Stack n a -> Stack (S n) a class Stacklike (s :: Nat -> * -> *) where emptyStack :: s Z a pop :: s (S n) a -> (a, s n a) push :: a -> s n a -> s (S n) a size :: s n a -> Nat toList :: s n a -> [a] fromList :: [a] -> (forall n. s n a -> b) -> b fromList [] k = k emptyStack fromList (x:xs) k = fromList xs (k . push x) instance Stacklike Stack where emptyStack = Empty pop (Push x xs) = (x, xs) push = Push size Empty = Z size (Push _ xs) = S (size xs) toList Empty = [] toList (Push x xs) = x : toList xs Here it is statically proven by Stacklike that the following length preserving property holds: snd . pop . push x :: (Stacklike s) => s n a -> s n a The way Stack is defined makes sure that the following holds: (snd . pop . push x) emptyStack = emptyStack These are the things you can prove. What you can't prove is properties that require lifting the class's functions to the type level. This requires real dependent types. You can replicate the functions on the type level, but this is not lifting and can introduce errors. Also for real proofs your language must be total. Haskell isn't, so you can always cheat by providing bottom as a proof. You may want to check out Agda. Greets, Ertugrul -- Not to be or to be and (not to be or to be and (not to be or to be and (not to be or to be and ... that is the list monad.