Re: [Haskell-cafe] specifying using type class

Hi there Patrick,
Patrick Browne
Thanks for you very clear explanation. Without committing to some concrete representation such as list I do not know how to specify constructors in the class (see below). As you point out a class may not be appropriate for an actual application, but I am investigating the strengths and weaknesses of class as a unit of *specification*. Regards, Pat
-- Class with functional dependency class QUEUE_SPEC_CLASS2 a q | q -> a where newC2 :: q a -- ?? sizeC2 :: q a -> Int restC2 :: q a -> Maybe (q a) insertC2 :: q a -> a -> q a -- Without committing to some concrete representation such as list I do not know how to specify constructor for insertC2 ?? = ?? insertC2 newC2 a = newC2 -- wrong isEmptyC2 :: q a -> Bool isEmptyC2 newC2 = True -- isEmptyC2 (insertC2 newC2 a) = False wrong
You are probably confusing the type class system with something from OOP. A type class captures a pattern in the way a type is used. The corresponding concrete representation of that pattern is then written in the instance definition: class Stacklike s where emptyStack :: s a push :: a -> s a -> s a rest :: s a -> Maybe (s a) top :: s a -> Maybe a pop :: s a -> Maybe (a, s a) pop s = liftA2 (,) (top s) (rest s) instance Stacklike [] where emptyStack = [] push = (:) top = foldr (\x _ -> Just x) Nothing rest [] = Nothing rest (Push _ xs) = Just xs data MyStack a = Empty | Push a (MyStack a) instance Stacklike MyStack where emptyStack = Empty push = Push top Empty = Nothing top (Push x _) = Just x rest Empty = Nothing rest (Push _ xs) = Just xs 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.

Patrick,
-- Class with functional dependency class QUEUE_SPEC_CLASS2 a q | q -> a where newC2 :: q a -- ?? sizeC2 :: q a -> Int restC2 :: q a -> Maybe (q a) insertC2 :: q a -> a -> q a
The above is a reasonable type class definition for what you seem to intend.
-- Without committing to some concrete representation such as list I do not know how to specify constructor for insertC2 ?? = ?? insertC2 newC2 a = newC2 -- wrong isEmptyC2 :: q a -> Bool isEmptyC2 newC2 = True -- isEmptyC2 (insertC2 newC2 a) = False wrong
Correct me if I'm wrong, but what I understand you want to do here is specify axioms on the behaviour of the above interface methods, similar to how the well-known |Monad| class specifies for example "m
= return === m". You seem to want for example an axiom saying
isEmptyC2 newC2 === True and similar for possible other equations. With such axioms you don't need access to actual constructors and you don't want access to them because concrete implementations may use a different representation that does not use such constructors. Anyway, in current Haskell, such type class axioms can not be formally specified or proven but they are typically formulated as part of the documentation of a type class and implementations of the type class are required to satisfy them but this is not automatically verified. Dominique
participants (3)
-
Dominique Devriese
-
Ertugrul Söylemez
-
Patrick Browne