Relational Algebra library: first version on GitHub

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
20 messages Options
Reply | Threaded
Open this post in threaded view
|

Relational Algebra library: first version on GitHub

Paul Visschers-2
Hello,

A couple of weeks ago I asked if there was interest in a library that implements a type-safe relational algebra. The response was positive, so I have spruced up the code I had a bit and created a repository on GitHub at:


It is a very rudimentary version. The code is not documented and there is only a very basic example database in Test.hs. It might be helpful to look at HaskellDB's PrimQuery and PrimExpr, as this library is mostly a direct copy from that (but typed). I will add some decent examples of expressions and queries shortly.

If you check it out, please comment on it and let me know if you want to contribute. Since this is going to be my first release, any feedback is welcome.

Paul Visschers

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Relational Algebra library: first version on GitHub

Ertugrul Söylemez
Hello there Paul,

Paul Visschers <[hidden email]> wrote:

> A couple of weeks ago I asked if there was interest in a library that
> implements a type-safe relational algebra. The response was positive,
> so I have spruced up the code I had a bit and created a repository on
> GitHub at:
>
> https://github.com/PaulVisschers/relational-algebra
>
> It is a very rudimentary version. The code is not documented and there
> is only a very basic example database in Test.hs. It might be helpful
> to look at HaskellDB's PrimQuery and PrimExpr, as this library is
> mostly a direct copy from that (but typed). I will add some decent
> examples of expressions and queries shortly.
>
> If you check it out, please comment on it and let me know if you want
> to contribute. Since this is going to be my first release, any
> feedback is welcome.
Well, the demonstration could be a bit more comprehensive.  I would be
very interested in seeing queries, especially nontrivial ones with joins
and such.

Would you mind writing a more comprehensive demonstration?


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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Relational Algebra library: first version on GitHub

Carter Schonwald
In reply to this post by Paul Visschers-2
Great / thanks!!! This will be incredibly helpful for some of my present work. :-)

On Saturday, July 21, 2012, Paul Visschers wrote:
Hello,

A couple of weeks ago I asked if there was interest in a library that implements a type-safe relational algebra. The response was positive, so I have spruced up the code I had a bit and created a repository on GitHub at:


It is a very rudimentary version. The code is not documented and there is only a very basic example database in Test.hs. It might be helpful to look at HaskellDB's PrimQuery and PrimExpr, as this library is mostly a direct copy from that (but typed). I will add some decent examples of expressions and queries shortly.

If you check it out, please comment on it and let me know if you want to contribute. Since this is going to be my first release, any feedback is welcome.

Paul Visschers

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Relational Algebra library: first version on GitHub

Paul Visschers-2
In reply to this post by Ertugrul Söylemez
Hey Ertugrul,

You are absolutely right and the first item on my todo list is to add better examples.

Paul

On Sun, Jul 22, 2012 at 5:24 AM, Ertugrul Söylemez <[hidden email]> wrote:
Hello there Paul,

Paul Visschers <[hidden email]> wrote:

> A couple of weeks ago I asked if there was interest in a library that
> implements a type-safe relational algebra. The response was positive,
> so I have spruced up the code I had a bit and created a repository on
> GitHub at:
>
> https://github.com/PaulVisschers/relational-algebra
>
> It is a very rudimentary version. The code is not documented and there
> is only a very basic example database in Test.hs. It might be helpful
> to look at HaskellDB's PrimQuery and PrimExpr, as this library is
> mostly a direct copy from that (but typed). I will add some decent
> examples of expressions and queries shortly.
>
> If you check it out, please comment on it and let me know if you want
> to contribute. Since this is going to be my first release, any
> feedback is welcome.

Well, the demonstration could be a bit more comprehensive.  I would be
very interested in seeing queries, especially nontrivial ones with joins
and such.

Would you mind writing a more comprehensive demonstration?


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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

specifying using type class

Patrick Browne
In reply to this post by Ertugrul Söylemez
{-
Below is a *specification* of a queue.
If possible I would like to write the equations in type class.
Does the type class need two type variables?
How do I represent the constructors?
Can the equations be written in the type class rather than the instance?
-}

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)

My first stab at a class
class QUEUE_SPEC q e where
 new :: q e
 insert :: q e -> q e
 isEmpty :: q  e  -> Bool
 first :: q  e  -> e
 rest :: q  e  -> q e
 size :: q e  -> Int

-}


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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Ertugrul Söylemez
Patrick Browne <[hidden email]> wrote:

> {-
> Below is a *specification* of a queue.
> If possible I would like to write the equations in type class.
> Does the type class need two type variables?
> How do I represent the constructors?
> Can the equations be written in the type class rather than the
> instance? -}

(Side note:  When opening a new topic, please don't /reply/ to a post,
but post it separately by creating a new mail.)

The type class needs to know the element type, so your observation is
correct.  Usually, as in your case, the element type follows from the
data structure type, and you will want to inform the type system about
this connection.  There are basically three ways to do it.  The first is
using MultiParamTypeClasses and FunctionalDependencies:

    class Stacklike a s | s -> a where
        empty :: s a
        null  :: s a -> Bool
        push  :: a -> s a -> s a
        pop   :: s a -> Maybe a
        size  :: s a -> Int
        tail  :: s a -> Maybe (s a)

Another way is using an associated type (TypeFamilies).  This is
cleaner, but much more noisy in the type signatures:

    class Stacklike s where
        type StackElement s

        empty :: s (StackElement s)
        null  :: s (StackElement s) -> Bool
        push  :: StackElement s -> s (StackElement s) -> s (StackElement s)
        pop   :: s (StackElement s) -> Maybe (StackElement s)
        size  :: s (StackElement s) -> Int
        tail  :: s (StackElement s) -> Maybe (s (StackElement s))

Finally once you realize that there is really no need to fix the element
type in the type class itself, you can simply write a type class for the
type constructor, similar to how classes like Functor are defined:

    class Stacklike s where
        empty :: s a
        null  :: s a -> Bool
        push  :: a -> s a -> s a
        pop   :: s a -> Maybe a
        size  :: s a -> Int
        tail  :: s a -> Maybe (s a)

The big question is whether you want to write a class at all.  Usually
classes are used to capture patterns, not operations.


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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
In reply to this post by Patrick Browne
 Ertugrul ,
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



On 22/07/12, Ertugrul Söylemez <[hidden email]> wrote:
Patrick Browne <[hidden email]> wrote:

> {-
> Below is a *specification* of a queue.
> If possible I would like to write the equations in type class.
> Does the type class need two type variables?
> How do I represent the constructors?
> Can the equations be written in the type class rather than the
> instance? -}

(Side note:  When opening a new topic, please don't /reply/ to a post,
but post it separately by creating a new mail.)

The type class needs to know the element type, so your observation is
correct.  Usually, as in your case, the element type follows from the
data structure type, and you will want to inform the type system about
this connection.  There are basically three ways to do it.  The first is
using MultiParamTypeClasses and FunctionalDependencies:

    class Stacklike a s | s -> a where
        empty :: s a
        null  :: s a -> Bool
        push  :: a -> s a -> s a
        pop   :: s a -> Maybe a
        size  :: s a -> Int
        tail  :: s a -> Maybe (s a)

Another way is using an associated type (TypeFamilies).  This is
cleaner, but much more noisy in the type signatures:

    class Stacklike s where
        type StackElement s

        empty :: s (StackElement s)
        null  :: s (StackElement s) -> Bool
        push  :: StackElement s -> s (StackElement s) -> s (StackElement s)
        pop   :: s (StackElement s) -> Maybe (StackElement s)
        size  :: s (StackElement s) -> Int
        tail  :: s (StackElement s) -> Maybe (s (StackElement s))

Finally once you realize that there is really no need to fix the element
type in the type class itself, you can simply write a type class for the
type constructor, similar to how classes like Functor are defined:

    class Stacklike s where
        empty :: s a
        null  :: s a -> Bool
        push  :: a -> s a -> s a
        pop   :: s a -> Maybe a
        size  :: s a -> Int
        tail  :: s a -> Maybe (s a)

The big question is whether you want to write a class at all.  Usually
classes are used to capture patterns, not operations.


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.

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Ertugrul Söylemez
Hi there Patrick,

Patrick Browne <[hidden email]> wrote:

> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
In reply to this post by Patrick Browne


On 22/07/12, Ertugrul Söylemez <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Alejandro Serrano Mena
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 <[hidden email]>


On 22/07/12, Ertugrul Söylemez <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
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 <[hidden email]> 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 <[hidden email] <[hidden email]>>


On 22/07/12, Ertugrul Söylemez <[hidden email] <[hidden email]>> 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
[hidden email] <[hidden email]>
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]>
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 <[hidden email]> 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 <[hidden email] <[hidden email]>>


On 22/07/12, Ertugrul Söylemez <[hidden email] <[hidden email]>> 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
[hidden email] <[hidden email]>
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


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
In reply to this post by Patrick Browne
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

[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

On 23/07/12, Alejandro Serrano Mena <[hidden email]> wrote:
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 <[hidden email] <[hidden email]>>
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 <[hidden email] <[hidden email]>> 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 <[hidden email] <[hidden email]> <[hidden email] <[hidden email]>>>


On 22/07/12, Ertugrul Söylemez <[hidden email] <[hidden email]> <[hidden email] <[hidden email]>>> 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
[hidden email] <[hidden email]> <[hidden email] <[hidden email]>>
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


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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Dominique Devriese-2
In reply to this post by Patrick Browne
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
Dominique,
That is exactly the information that I required.
Thank you very much,
Pat


On 23/07/12, Dominique Devriese <[hidden email]> wrote:
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


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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Ertugrul Söylemez
In reply to this post by Patrick Browne
Patrick Browne <[hidden email]> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Ryan Ingram
In reply to this post by Patrick Browne
Generally the way this is done in Haskell is that the interface to the type is specified in a typeclass (or, alternatively, in a module export list, for concrete types), and the axioms are specified in a method to be tested in some framework (i.e. QuickCheck, SmallCheck, SmartCheck) which can automatically generate instances of your type and test that the axioms hold.

For example:

class QueueLike q where
    empty :: q a
    insert :: a -> q a -> q a
    viewFirst :: q a -> Maybe (a, q a)
    size :: q a -> Integer

-- can use a single proxy type if have kind polymorphism, but that's an experimental feature right now
data Proxy2 (q :: * -> *) = Proxy2
instance Arbitrary (Proxy2 q) where arbitrary = return Proxy2

prop_insertIncrementsSize :: forall q. QueueLike q => q () -> Bool
prop_insertIncrementsSize q = size (insert () q) == size q + 1

prop_emptyQueueIsEmpty :: forall q. QueueLike q => Proxy2 q => Bool
prop_emptyQueueIsEmpty Proxy2 = maybe True (const False) $ view (empty :: q ())

Then you specialize these properties to your type and test them:

instance QueueLike [] where ...

ghci> quickCheck (prop_insertIncrementsSize :: [()] -> Bool)
Valid, passed 100 tests
or
Failed with: [(), (), ()]

QuickCheck randomly generates objects of your data structure and tests your property against them.  While not as strong as a proof, programs with 100% quickcheck coverage are *extremely* reliable.  SmartCheck is an extension of QuickCheck that tries to reduce test cases to the minimum failing size.

SmallCheck does exhaustive testing on the properties for finite data structures up to a particular size.  It's quite useful when you can prove your algorithms 'generalize' after a particular point.

There aren't any libraries that I know of for dependent-type style program proof for haskell; I'm not sure it's possible.  The systems I know of have you program in a more strongly typed language (Coq/agda) and export Haskell programs once they are proven safe.  Many of these rely on unsafeCoerce in the Haskell code because they have proven stronger properties about the types than Haskell can; I look at that code with some trepidation--I am not sure what guarantees the compiler makes about unsafeCoerce.

  -- ryan

On Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne <[hidden email]> wrote:
{-
Below is a *specification* of a queue.
If possible I would like to write the equations in type class.
Does the type class need two type variables?
How do I represent the constructors?
Can the equations be written in the type class rather than the instance?
-}

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)

My first stab at a class
class QUEUE_SPEC q e where
 new :: q e
 insert :: q e -> q e
 isEmpty :: q  e  -> Bool
 first :: q  e  -> e
 rest :: q  e  -> q e
 size :: q e  -> Int

-}


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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
In reply to this post by Patrick Browne

Hi,
Thanks for all the very useful feed back on this thread.
I would like to present my possibly incorrect summarized  view:
Class signatures can contain placeholders for constructors.
These place-holder-constructors cannot be used in the class to define functions (I assume other in-scope constructors can be used).
In the instance a real constructor can be substituted for the place-holder-constructor.
Does this restrict the type of equation that can be used in a type class?
It seems that some equations respecting the constructor discipline are not allowed.

I appreciate that in Haskell the most equations occur in the instances, but from my earlier post:
"I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification*"

Is my summarized view is correct?
Regards,
Pat
 
On 31/07/12, Ryan Ingram <[hidden email]> wrote:
Generally the way this is done in Haskell is that the interface to the type is specified in a typeclass (or, alternatively, in a module export list, for concrete types), and the axioms are specified in a method to be tested in some framework (i.e. QuickCheck, SmallCheck, SmartCheck) which can automatically generate instances of your type and test that the axioms hold.

For example:

class QueueLike q where
    empty :: q a
    insert :: a -> q a -> q a
    viewFirst :: q a -> Maybe (a, q a)
    size :: q a -> Integer

-- can use a single proxy type if have kind polymorphism, but that's an experimental feature right now
data Proxy2 (q :: * -> *) = Proxy2
instance Arbitrary (Proxy2 q) where arbitrary = return Proxy2

prop_insertIncrementsSize :: forall q. QueueLike q => q () -> Bool
prop_insertIncrementsSize q = size (insert () q) == size q + 1

prop_emptyQueueIsEmpty :: forall q. QueueLike q => Proxy2 q => Bool
prop_emptyQueueIsEmpty Proxy2 = maybe True (const False) $ view (empty :: q ())

Then you specialize these properties to your type and test them:

instance QueueLike [] where ...

ghci> quickCheck (prop_insertIncrementsSize :: [()] -> Bool)
Valid, passed 100 tests
or
Failed with: [(), (), ()]

QuickCheck randomly generates objects of your data structure and tests your property against them.  While not as strong as a proof, programs with 100% quickcheck coverage are *extremely* reliable.  SmartCheck is an extension of QuickCheck that tries to reduce test cases to the minimum failing size.

SmallCheck does exhaustive testing on the properties for finite data structures up to a particular size.  It's quite useful when you can prove your algorithms 'generalize' after a particular point.

There aren't any libraries that I know of for dependent-type style program proof for haskell; I'm not sure it's possible.  The systems I know of have you program in a more strongly typed language (Coq/agda) and export Haskell programs once they are proven safe.  Many of these rely on unsafeCoerce in the Haskell code because they have proven stronger properties about the types than Haskell can; I look at that code with some trepidation--I am not sure what guarantees the compiler makes about unsafeCoerce.

  -- ryan

On Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne <[hidden email] <[hidden email]>> wrote:
{-
Below is a *specification* of a queue.
If possible I would like to write the equations in type class.
Does the type class need two type variables?
How do I represent the constructors?
Can the equations be written in the type class rather than the instance?
-}

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)

My first stab at a class
class QUEUE_SPEC q e where
 new :: q e
 insert :: q e -> q e
 isEmpty :: q  e  -> Bool
 first :: q  e  -> e
 rest :: q  e  -> q e
 size :: q e  -> Int

-}


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
[hidden email] <[hidden email]>
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Ertugrul Söylemez
Patrick Browne <[hidden email]> wrote:

> Thanks for all the very useful feed back on this thread.
> I would like to present my possibly incorrect summarized  view:
> Class signatures can contain placeholders for constructors.
> These place-holder-constructors cannot be used in the class to define
> functions (I assume other in-scope constructors can be used). In the
> instance a real constructor can be substituted for the
> place-holder-constructor. Does this restrict the type of equation
> that can be used in a type class? It seems that some equations
> respecting the constructor discipline are not allowed.

Your intuition seems to be near the truth, although your terminology is
currently wrong.  Let's look at an example:

    class Functor f where
        fmap :: (a -> b) -> (f a -> f b)

The 'f' in the class header is probably what you call a "placeholder for
constructors".  This is not a placeholder, but a type variable.  It
represents a type.  Incidentally in this case it indeed represents a
constructor, namely a /type/ constructor (like Maybe).  This is an
important distinction, because generally when we talk about
"constructors", we mean /value/ constructors (like Just or Nothing):

    data Maybe a = Just a | Nothing

Here Maybe is a type constructor.  This is because it's not a type in
its own right, but is applied to another type (like Int) to yield an
actual type (Maybe Int).  The type Maybe is applied to is represented
by the type variable 'a' in the code above.  To simplify communication
we often call Maybe itself also a type, but it's really not.

Let's write the Functor instance for Maybe.  It is common to use a
helper function (a so-called fold function), which allows us to express
many operations more easily.  It's called 'maybe' for Maybe:

    maybe :: b -> (a -> b) -> Maybe a -> b
    maybe n j (Just x) = j x
    maybe n j Nothing  = n

    instance Functor Maybe where
        fmap f = maybe Nothing (Just . f)

This is the instance for Maybe.  The type variable 'f' from the class
now becomes a concrete type constructor Maybe.  In this instance you
have f = Maybe, so the type of 'fmap' for this particular instance
becomes:

    fmap :: (a -> b) -> (Maybe a -> Maybe b)

The notable thing here is that this is really not a
placeholder/replacement concept, but much more like a function and
application concept.  There is nothing that stops you from having type
variables in an instance:

    instance Functor (Reader e) where

As you can see there is still what you called a "placeholder" in this
instance, so the placeholder concept doesn't really make sense here.
The declaration can be read as:

    "For every type 'e' the type 'Reader e' is an instance of the
    Functor type class."


> I appreciate that in Haskell the most equations occur in the
> instances, [...]

Not at all.  When programming Haskell you write lots and lots of
equations outside of class instances.  Whenever you write "=" you
introduce an equation, for example in top-level definitions and in 'let'
and 'where' bindings.


> [...] but from my earlier post: "I merely wish to identify the
> strengths and weakness of *current Haskell type classes* as a pure
> *unit of specification*"

I think you will be interested in this Stack Overflow answer:

    <http://stackoverflow.com/a/8123973>

Even though the actual question answered is different, it does give a
nice overview of the strengths and weaknesses of type classes.


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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: specifying using type class

Patrick Browne
Ertugrul,
Thank you for your detailed and helpful reply.
I was unaware of the distinction between data/value and type constructors.
Regards,
Pat



On 31/07/12, Ertugrul Söylemez <[hidden email]> wrote:
Patrick Browne <[hidden email]> wrote:

> Thanks for all the very useful feed back on this thread.
> I would like to present my possibly incorrect summarized  view:
> Class signatures can contain placeholders for constructors.
> These place-holder-constructors cannot be used in the class to define
> functions (I assume other in-scope constructors can be used). In the
> instance a real constructor can be substituted for the
> place-holder-constructor. Does this restrict the type of equation
> that can be used in a type class? It seems that some equations
> respecting the constructor discipline are not allowed.

Your intuition seems to be near the truth, although your terminology is
currently wrong.  Let's look at an example:

    class Functor f where
        fmap :: (a -> b) -> (f a -> f b)

The 'f' in the class header is probably what you call a "placeholder for
constructors".  This is not a placeholder, but a type variable.  It
represents a type.  Incidentally in this case it indeed represents a
constructor, namely a /type/ constructor (like Maybe).  This is an
important distinction, because generally when we talk about
"constructors", we mean /value/ constructors (like Just or Nothing):

    data Maybe a = Just a | Nothing

Here Maybe is a type constructor.  This is because it's not a type in
its own right, but is applied to another type (like Int) to yield an
actual type (Maybe Int).  The type Maybe is applied to is represented
by the type variable 'a' in the code above.  To simplify communication
we often call Maybe itself also a type, but it's really not.

Let's write the Functor instance for Maybe.  It is common to use a
helper function (a so-called fold function), which allows us to express
many operations more easily.  It's called 'maybe' for Maybe:

    maybe :: b -> (a -> b) -> Maybe a -> b
    maybe n j (Just x) = j x
    maybe n j Nothing  = n

    instance Functor Maybe where
        fmap f = maybe Nothing (Just . f)

This is the instance for Maybe.  The type variable 'f' from the class
now becomes a concrete type constructor Maybe.  In this instance you
have f = Maybe, so the type of 'fmap' for this particular instance
becomes:

    fmap :: (a -> b) -> (Maybe a -> Maybe b)

The notable thing here is that this is really not a
placeholder/replacement concept, but much more like a function and
application concept.  There is nothing that stops you from having type
variables in an instance:

    instance Functor (Reader e) where

As you can see there is still what you called a "placeholder" in this
instance, so the placeholder concept doesn't really make sense here.
The declaration can be read as:

    "For every type 'e' the type 'Reader e' is an instance of the
    Functor type class."


> I appreciate that in Haskell the most equations occur in the
> instances, [...]

Not at all.  When programming Haskell you write lots and lots of
equations outside of class instances.  Whenever you write "=" you
introduce an equation, for example in top-level definitions and in 'let'
and 'where' bindings.


> [...] but from my earlier post: "I merely wish to identify the
> strengths and weakness of *current Haskell type classes* as a pure
> *unit of specification*"

I think you will be interested in this Stack Overflow answer:

    <http://stackoverflow.com/a/8123973>

Even though the actual question answered is different, it does give a
nice overview of the strengths and weaknesses of type classes.


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.

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe