Alejandro,<br _moz_dirty="" />Thank you for your clear an detailed reply, the work on dependent types seems to address my needs.<br _moz_dirty="" />However it is beyond my current research question, which is quite narrow(see[1]).<br _moz_dirty="" />I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification*.<br _moz_dirty="" />I do not wish to address any perceived weakness, I merely wish to identify them (if there are ant).<br _moz_dirty="" />Of course my question may be ill conceived, in that type classes were intended to specify interfaces and not algebraic types.<br _moz_dirty="" /><br _moz_dirty="" />Regards,<br _moz_dirty="" />Pat<br _moz_dirty="" /><br _moz_dirty="" type="_moz" /><div style="font-family: 'Times New Roman'; font-size: 16px;">[1] ftp://ftp.geoinfo.tuwien.ac.at/wilke/BUP_Skriptsammlungen/GeoInfo/%5BPub%5D/2002_%5BKuhn%5D_Modelling_the_Semantics_of_geographic_Categories_through_Conceptual_Integration.pdf<br /><br /><span>On 23/07/12, <b class="name">Alejandro Serrano Mena </b> <trupill@gmail.com> wrote:</span><blockquote cite="mid:CAHnFXOtk+_cy42vDbfL=hGJakys80AcnqkdBUZ2JUjrF79PMLA@mail.gmail.com" class="iwcQuote" style="border-left: 1px solid #00F; padding-left: 13px; margin-left: 0;" type="cite"><div class="mimepart text html">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:<div><br /></div><div>
data Stack a = Empty | Top a (Stack a)</div><div><br /></div><div>Then you can write the implementation with respect to this concrete example.</div><div><br /></div><div>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.</div>
<div><br /></div><div>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:</div>
<div><br /></div><div>class Stack s a | s -> a where</div><div> isEmpty :: s a -> Bool</div><div> pop :: s a -> (a, s a) -- Returns the top element and the rest of the stack</div><div><br /></div><div> length :: s a -> Int</div>
<div> length stack = if isEmpty stack then 0 else (length (snd (pop stack))) + 1</div><div><br /></div><div>However, 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 as</div>
<div><br /></div><div>pop :: Stack a (n + 1) -> (a, Stack a n)</div><div><br /></div><div>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 (<a href="http://idris-lang.org/" target="_blank">http://idris-lang.org/</a>) or Agda2 (<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php</a>). A very good tutorial for the first is <a href="http://www.cs.st-andrews.ac.uk/%7Eeb/writings/idris-tutorial.pdf" target="_blank">http://www.cs.st-andrews.ac.uk/~eb/writings/idris-tutorial.pdf</a></div>
<div><br /></div><div>Hope this helps!</div><div><br /><div class="gmail_quote">2012/7/23 Patrick Browne <span dir="ltr"><patrick.browne@dit.ie <patrick.browne@dit.ie>></span><br /><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Yes. I tried that, but due to my lack of Haskell expertise I cannot write the constructor insertC1 below:<br />
<br />
class QUEUE_SPEC_CLASS1 q where<br />
newC1 :: q a<br />
isEmptyC1 :: q a -> Bool<br />
insertC1 :: q a -> a -> q a<br />
sizeC1 :: q a -> Int<br />
restC1 :: q a -> q a<br />
-- I do not know how to specify constructor insertC1 ?? = ?? <br />
insertC1 newC1 a = newC1<br />
isEmptyC1 newC1 = True<br />
-- isEmpty (insertC1 newC1 a) = False <div style="font-family:'Times New Roman';font-size:16px"><div class="im"><br /><br /><span>On 23/07/12, <b>Alejandro Serrano Mena </b> <trupill@gmail.com <trupill@gmail.com>> wrote:</span></div>
<blockquote style="border-left:1px solid #00f;padding-left:13px;margin-left:0" type="cite"><div><div class="im">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:<div>
<br /></div><div>class Stack s where</div><div> newEmptyStack :: s a</div><div> newSingletonStack :: a -> s a</div><div> ...</div><div><br /></div><div>Why doesn't this fulfill you needs of specifying ways to construct new elements?</div>
</div><div><br /><div class="gmail_quote">2012/7/23 Patrick Browne <span dir="ltr"><patrick.browne@dit.ie <patrick.browne@dit.ie> <patrick.browne@dit.ie <patrick.browne@dit.ie>>></span><br />
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
<div style="font-family:'Times New Roman';font-size:16px"><div><br /><br /><span>On 22/07/12, <b>Ertugrul Söylemez </b> <es@ertes.de <es@ertes.de> <es@ertes.de <es@ertes.de>>> wrote:</span></div>
<div><blockquote style="border-left:1px solid #00f;padding-left:13px;margin-left:0" type="cite"><div><br /><br />You are probably confusing the type class system with something from<br />OOP. A type class captures a pattern in the way a type is used. The<br />
corresponding concrete representation of that pattern is then written in<br />the instance definition:<br /><br /> </div></blockquote></div>No really. I am investigating the strengths and weaknesses of type classes as a *unit of specification*. <br />
I am aware that their primarily intended to act as interface description, which I suppose is a form of specification.<br />To what degree could the QUEUE_SPEC (repeated below) from my first posting be expressed as a type class?<br />