Re: [Haskell-cafe] specifying using type class
Ertugrul,Thank you for your detailed and helpful reply.I was unaware of the distinction between data/value and type constructors.Regards,PatOn 31/07/12, Ertugrul Söylemez e...@ertes.de wrote:Patrick Browne patrick.bro...@dit.ie 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 iscurrently 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 forconstructors. This is not a placeholder, but a type variable. Itrepresents a type. Incidentally in this case it indeed represents aconstructor, namely a /type/ constructor (like Maybe). This is animportant distinction, because generally when we talk aboutconstructors, we mean /value/ constructors (like Just or Nothing): data Maybe a = Just a | NothingHere Maybe is a type constructor. This is because it's not a type inits own right, but is applied to another type (like Int) to yield anactual type (Maybe Int). The type Maybe is applied to is representedby the type variable 'a' in the code above. To simplify communicationwe 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 ahelper function (a so-called fold function), which allows us to expressmany 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 classnow becomes a concrete type constructor Maybe. In this instance youhave f = Maybe, so the type of 'fmap' for this particular instancebecomes: fmap :: (a - b) - (Maybe a - Maybe b)The notable thing here is that this is really not aplaceholder/replacement concept, but much more like a function andapplication concept. There is nothing that stops you from having typevariables in an instance: instance Functor (Reader e) whereAs you can see there is still what you called a placeholder in thisinstance, 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 ofequations outside of class instances. Whenever you write = youintroduce 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/8123973Even though the actual question answered is different, it does give anice 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
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 ryani.s...@gmail.com 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 :: * - *) = Proxy2instance Arbitrary (Proxy2 q) where arbitrary = return Proxy2prop_insertIncrementsSize :: forall q. QueueLike q = q () - Boolprop_insertIncrementsSize q = size (insert () q) == size q + 1
prop_emptyQueueIsEmpty :: forall q. QueueLike q = Proxy2 q = Boolprop_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 testsorFailed 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.
-- ryanOn Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie 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 wheredata Queue e = New | Insert (Queue e) e deriving ShowisEmpty :: Queue e - BoolisEmpty 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 erest (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 codesize (Insert (Insert (Insert New 5) 6) 3)rest (Insert (Insert (Insert New 5) 6) 3)My first stab at a classclass 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
Haskell-Cafe@haskell.org Haskell-Cafe@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
Re: [Haskell-cafe] specifying using type class
Patrick Browne patrick.bro...@dit.ie 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. signature.asc Description: PGP signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
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 patrick.bro...@dit.iewrote:
{-
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
On 22/07/12, Ertugrul Söylemez e...@ertes.de wrote:You are probably confusing the type class system with something fromOOP. A type class captures a pattern in the way a type is used. Thecorresponding concrete representation of that pattern is then written inthe 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 270module 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
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.bro...@dit.ie
On 22/07/12, *Ertugrul Söylemez * e...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
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 trup...@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.bro...@dit.ie patrick.bro...@dit.ie
On 22/07/12, Ertugrul Söylemez e...@ertes.de e...@ertes.de wrote:
You are probably confusing the type class system with something fromOOP. A type class captures a pattern in the way a type is used. The
corresponding concrete representation of that pattern is then written inthe 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@haskell.org Haskell-Cafe@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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
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.bro...@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 * trup...@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.bro...@dit.ie patrick.bro...@dit.ie
On 22/07/12, *Ertugrul Söylemez * e...@ertes.de e...@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
Re: [Haskell-cafe] specifying using type class
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Dominique,That is exactly the information that I required.Thank you very much,PatOn 23/07/12, Dominique Devriese dominique.devri...@cs.kuleuven.be 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 aThe 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 wrongCorrect me if I'm wrong, but what I understand you want to do here isspecify 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 === Trueand similar for possible other equations. With such axioms you don'tneed access to actual constructors and you don't want access to thembecause concrete implementations may use a different representationthat does not use such constructors. Anyway, in current Haskell, suchtype class axioms can not be formally specified or proven but they aretypically formulated as part of the documentation of a type class andimplementations of the type class are required to satisfy them butthis 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Patrick Browne patrick.bro...@dit.ie 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.
signature.asc
Description: PGP signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] specifying using type class
{-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 wheredata Queue e = New | Insert (Queue e) e deriving ShowisEmpty :: Queue e - BoolisEmpty New = True isEmpty (Insert q e) = False first :: Queue e - efirst (Insert q e) = if (isEmpty q) then e else (first q) rest :: Queue e - Queue erest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)size :: Queue e - Intsize New = 0 size (Insert q e) = succ (size q){- some tests of above codesize (Insert (Insert (Insert New 5) 6) 3)rest (Insert (Insert (Insert New 5) 6) 3)My first stab at a classclass 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Patrick Browne patrick.bro...@dit.ie 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.
signature.asc
Description: PGP signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
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 dependencyclass 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 wrongOn 22/07/12, Ertugrul Söylemez e...@ertes.de wrote:Patrick Browne patrick.bro...@dit.ie 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 iscorrect. Usually, as in your case, the element type follows from thedata structure type, and you will want to inform the type system aboutthis connection. There are basically three ways to do it. The first isusing 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 iscleaner, 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 elementtype in the type class itself, you can simply write a type class for thetype 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. Usuallyclasses 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Hi there Patrick, Patrick Browne patrick.bro...@dit.ie 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. signature.asc Description: PGP signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
