Alejandro,
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.
Regards,
Pat
I think you are confusing ADTs, type classes and default declarations in type classes. In Haskell, values are truly created only via abstract data types. That would be a specific instance of your class:data Stack a = Empty | Top a (Stack a)Then you can write the implementation with respect to this concrete example.What I was proposing, if you only need constructs, is that instead of thinking of constructors, you may think of a "factory" pattern, similar to that pattern in OOP: a function that creates the element for you. That would be the "newStack" in your type class: every instance of a Stack must provide a way to create new objects. However, this is just a function, so you cannot pattern match there.What type classes do allow you to do is to provide default implementations of some function in you type class. But this must be a complete implementation (I mean, executable code), not merely a specification of some properties. For example, say you have functions in your class for testing emptiness and poping elements. Then you may write a default implementation of length:class Stack s a | s -> a whereisEmpty :: s a -> Boolpop :: s a -> (a, s a) -- Returns the top element and the rest of the stacklength :: s a -> Intlength stack = if isEmpty stack then 0 else (length (snd (pop stack))) + 1However, I think that what you are trying to do is to encode some properties of data types into the type system. This is better done using "dependent typing", which in a very broad sense allows you to use value functions into types. For example, you may encode the number of elements of a stack in its type (so the type would be Stack <ElementType> <NumberOfElements>) and then you may only pop when the Stack is not empty, which could be encoded aspop :: Stack a (n + 1) -> (a, Stack a n)Haskell allows this way of encoding properties up to some extent (in particular, this example with numbers could be programmed in Haskell), but for the full power (and in my opinion, for a clearer view of what's happening) I recommend you to look at Idris (http://idris-lang.org/) or Agda2 (http://wiki.portal.chalmers.se/agda/pmwiki.php). A very good tutorial for the first is http://www.cs.st-andrews.ac.uk/~eb/writings/idris-tutorial.pdfHope this helps!2012/7/23 Patrick Browne <patrick.browne@dit.ie <patrick.browne@dit.ie>>Yes. I tried that, but due to my lack of Haskell expertise I cannot write the constructor insertC1 below:
class QUEUE_SPEC_CLASS1 q where
newC1 :: q a
isEmptyC1 :: q a -> Bool
insertC1 :: q a -> a -> q a
sizeC1 :: q a -> Int
restC1 :: q a -> q a
-- I do not know how to specify constructor insertC1 ?? = ??
insertC1 newC1 a = newC1
isEmptyC1 newC1 = True
-- isEmpty (insertC1 newC1 a) = False
On 23/07/12, Alejandro Serrano Mena <trupill@gmail.com <trupill@gmail.com>> wrote:I don't know whether this is really applicable but: isn't emptyStack in Ertugrul last message some kind of constructor? You can add any kind of special constructors as functions in the type class which return a new queue. For example:class Stack s wherenewEmptyStack :: s anewSingletonStack :: a -> s a...Why doesn't this fulfill you needs of specifying ways to construct new elements?2012/7/23 Patrick Browne <patrick.browne@dit.ie <patrick.browne@dit.ie> <patrick.browne@dit.ie <patrick.browne@dit.ie>>>
Haskell-Cafe@haskell.org <Haskell-Cafe@haskell.org> <Haskell-Cafe@haskell.org <Haskell-Cafe@haskell.org>>
On 22/07/12, Ertugrul Söylemez <es@ertes.de <es@ertes.de> <es@ertes.de <es@ertes.de>>> wrote:No really. I am investigating the strengths and weaknesses of type classes as a *unit of specification*.
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:
I am aware that their primarily intended to act as interface description, which I suppose is a form of specification.
To what degree could the QUEUE_SPEC (repeated below) from my first posting be expressed as a type class?
>From the feedback, I get the impression that an abstract specification such as QUEUE_SPEC cannot be expressed as a type class (as an instance yes).
The stumbling block seems to be the abstract representation of constructors.
In [1] the classes Moveable and Named are combined, but again each of these classes are pure signatures.
Regards,
Pat
[1]Haskell: The Craft of Functional Programming (Second Edition) Simon Thompson, page 270
module QUEUE_SPEC where
data Queue e = New | Insert (Queue e) e deriving Show
isEmpty :: Queue e -> Bool
isEmpty New = True
isEmpty (Insert q e) = False
first :: Queue e -> e
first (Insert q e) = if (isEmpty q) then e else (first q)
rest :: Queue e -> Queue e
rest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)
size :: Queue e -> Int
size New = 0
size (Insert q e) = succ (size q)
{-
some tests of above code
size (Insert (Insert (Insert New 5) 6) 3)
rest (Insert (Insert (Insert New 5) 6) 3)
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie
_______________________________________________
Haskell-Cafe mailing list
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie