[Haskell-cafe] specifying using type class

[Alejandro Serrano Mena]

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 where
  isEmpty :: s a -> Bool
  pop :: s a -> (a, s a)  -- Returns the top element and the rest of the
stack

  length :: s a -> Int
  length stack = if isEmpty stack then 0 else (length (snd (pop stack))) + 1

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

pop :: 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.pdf

Hope this helps!

2012/7/23 Patrick Browne <patrick.browne at 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 at 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 where
>   newEmptyStack :: s a
>   newSingletonStack :: a -> s a
>   ...
>
> Why doesn't this fulfill you needs of specifying ways to construct new
> elements?
>
> 2012/7/23 Patrick Browne <patrick.browne at dit.ie <patrick.browne at dit.ie>>
>
>>
>>
>> On 22/07/12, *Ertugrul Söylemez * <es at ertes.de <es at ertes.de>> wrote:
>>
>>
>>
>> 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:
>>
>>
>>
>> No really. I am investigating the strengths and weaknesses of type
>> classes as a *unit of specification*.
>> 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
>> Haskell-Cafe at haskell.org <Haskell-Cafe at haskell.org>
>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120723/f6a71877/attachment.htm>