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] Need help with learning Parsec
Am 22.07.2012 17:21, schrieb C K Kashyap: I've updated the parser here - https://github.com/ckkashyap/LearningPrograms/blob/master/Haskell/Parsing/xml_3.hs The whole thing is less than 100 lines and it can handle comments as well. This code is still not nice: Duplicate code in openTag and withoutExplictCloseTag. The toplevel-try in try withoutExplictCloseTag | withExplicitCloseTag should be avoided by factoring out the common prefix. Again, I would avoid notFollowedBy by using many1. tag - try(char '' many1 (letter | digit)) In quotedChar you do not only want to escape the quote but at least the backslash, too. You could allow to escape any character by a backslash using: quotedChar c = try (char '\\' anyChar) | noneOf [c, '\\'] Writing a separate parser stripLeadingSpaces is overkill. Just use spaces parseXML (or apply dropWhile isSpace to the input string) C. [...] ___ 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] Haskell's type inference considered harmful
Thanks for your answer and your examples. It would be worthwile
collecting such examples in a small article.
I think some of the problems with type inference come from insufficient
theory about metavariables. When I started studying higher-order
unification I always wondered what the scope of a metavariable is. It
is created at some point and then just sits there waiting to be solved
by a constraint. However, it is not clear where these constraints may
come from and at what time a metavariable should be declared unsolved or
be generalized over.
In the HM toy calculus (lambda + let), it is spelled out:
generalization must happen after a let, such that the solution for a
metavariable is determined solely by constraints in the *definition* of
a symbol, not in its *use*.
I'd be grateful for pointers to work that considers metavariable scope
in some bigger, more realistic calculi. In Haskell, one thing that goes
wrong is that all definitions in a module are considered mutually
recursive by the type inference algorithm. But in fact, the definitions
can be stratified by a strongly connected components analysis. Doing
such an analysis, and limiting metavariable scope to an SCC, would
overcome the problem I outlined in my original mail and would result in
a more principled treatment of metavariables.
That concerned type inference for global definitions. It is not clear
we want the same for local definitions. There, it makes more sense to
assume that the programmer can overlook what he is doing, and thus one
could allow flow of information from the use of a symbol to its
definition.
Do we want information flow from dead code to live code? I'd say no.
Dead is unfortunately undecidable; but at least one can identify
unused local definitions, i.e., statically unreachable definitions.
Your examples seem to suggest you want such information flow, or maybe not?
On 21.07.2012 12:26, o...@okmij.org wrote:
However, if your are using ExtendedDefaultRules then you are likely to
know you are leaving the clean sound world of type inference.
First of all, ExtendedDefaultRules is enabled by default in
GHCi. Second, my example will work without ExtendedDefaultRules, in
pure Haskell98. It is even shorter:
instance Num Char
main = do
x - return []
let y = x
print . fst $ (x, abs $ head x)
-- let dead = if False then y == else True
return ()
The printed result is either [] or .
Mainly, if the point is to demonstrate the non-compositionality of type
inference and the effect of the dead code, one can give many many
examples, in Haskell98 or even in SML.
Here is a short one (which does not relies on defaulting. It uses
ExistentialQuantification, which I think is in the new standard or is
about to be.).
{-# LANGUAGE ExistentialQuantification #-}
data Foo = forall a. Show a = Foo [a]
main = do
x - return []
let z = Foo x
let dead = if False then x == else True
return ()
The code type checks. If you _remove_ the dead code, it won't. As you
can see, the dead can have profound, and beneficial influence on
alive, constraining them. (I guess this example is well-timed for Obon).
Ah, I have never been in Japan at that time.
For another example, take type classes. Haskell98 prohibits overlapping of
instances. Checking for overlapping requires the global analysis of the
whole program and is clearly non-compositional. Whether you may define
instance Num (Int,Int)
depends on whether somebody else, in a library you use indirectly,
has already introduced that instance. Perhaps that library is imported
for a function that has nothing to do with treating a pair of Ints as
a Num -- that is, the instance is a dead code for your
program. Nevertheless, instances are always imported, implicitly.
Yes, that's a known problem.
The non-compositionality of type inference occurs even in SML (or
other language with value restriction). For example,
let x = ref [];;
(* let z = if false then x := [1] else ();; *)
x := [true];;
This code type checks. If we uncomment the dead definition, it
won't. So, the type of x cannot be fully determined from its
definition; we need to know the context of its use -- which is
precisely what seems to upset you about Haskell.
To stirr action, mails on haskell-cafe seem useless.
What made you think that? Your questions weren't well answered? What
other venue would you propose?
Yes, they were. But for discussion about metavariables maybe something
like a haskell implementor's forum would be more appropriate. Yet I am
only an Agda implementor.
Cheers,
Andreas
--
Andreas AbelDu bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
___
Haskell-Cafe mailing list
Re: [Haskell-cafe] Need help with learning Parsec
Thank you so much Christian for your feedback ... I shall incorporate them. Regards, Kashyap On Mon, Jul 23, 2012 at 3:17 PM, Christian Maeder christian.mae...@dfki.dewrote: Am 22.07.2012 17:21, schrieb C K Kashyap: I've updated the parser here - https://github.com/ckkashyap/**LearningPrograms/blob/master/** Haskell/Parsing/xml_3.hshttps://github.com/ckkashyap/LearningPrograms/blob/master/Haskell/Parsing/xml_3.hs The whole thing is less than 100 lines and it can handle comments as well. This code is still not nice: Duplicate code in openTag and withoutExplictCloseTag. The toplevel-try in try withoutExplictCloseTag | withExplicitCloseTag should be avoided by factoring out the common prefix. Again, I would avoid notFollowedBy by using many1. tag - try(char '' many1 (letter | digit)) In quotedChar you do not only want to escape the quote but at least the backslash, too. You could allow to escape any character by a backslash using: quotedChar c = try (char '\\' anyChar) | noneOf [c, '\\'] Writing a separate parser stripLeadingSpaces is overkill. Just use spaces parseXML (or apply dropWhile isSpace to the input string) C. [...] ___ 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
Re: [Haskell-cafe] TLS 0.9.6, question about session resumption.
On 07/21/2012 05:12 PM, C Gosch wrote: Hi Cafe, and then the server says (AlertLevel_Fatal,UnexpectedMessage) I'm not sure whether the ServerHelloDone should happen when resuming. Does anyone have a hint what may be going wrong? I am using TLS10 and the tls package with version 0.9.6. Hi Christian, Domique is right, a sucessful session resumption should have a Finished message after ServerHello. It's not really clear what's your setup (are you trying to use TLS on server/client/both ?), and without some code, it's hard to debug your problem. The only thing that come to my mind is, did you setup your session callbacks correctly ? -- Vincent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] TLS 0.9.6, question about session resumption.
Thank you Vincent and Dominique,
I saw the session callbacks before, and guessed that I needed to store
the SessionData for all SessionIDs and return them on resumption
(correct me if that's wrong).
However, I could not find a module that exports these two data types, so
I figured maybe that's work in progress or something I am not meant to
fumble with ... or maybe I was just too blind to see where I get the
data types from. Can you help me out?
Maybe it helps if I post the configuration that I used:
initServerState :: IO ServerState
initServerState = do
gen - newGenIO :: IO SystemRandom
cert - fileReadCertificate cacert.pem
pk - fileReadPrivateKey privatekey2.pem
-- sessionMap - newTMVar M.empty
let params = defaultParams {
pConnectVersion = TLS10
, pCiphers = ciphersuite_all
, pLogging = TLSLogging { loggingPacketSent = noLog
, loggingPacketRecv = noLog
, loggingIOSent = \_ - return ()
, loggingIORecv = \_ _ - return () }
, onHandshake = handshakeCallback
, pUseSession = False -- FIXME: This should be True for session
resumption, but session resumption fails so far ...
-- The next two functions need SessionID and
SessionData as arguments, but these are not exported by any module.
-- , onSessionEstablished = \_ _ - sessionEst sessionMap
-- , onSessionResumption = \_ - sessionRes sessionMap
, onCertificatesRecv = certRecv
, pCertificates = [(cert, Just pk)] }
s - listenOn (PortNumber 3000)
-- ... and some more stuff down here having nothing to do with the
-- networking...
The client is a small Java program that just sends some data via a ssl
connection. It works with the pUseSession = False setting as above, and
it also works with an openssl s_server.
Cheers,
Christian
On Mon, 2012-07-23 at 15:33 +0100, Vincent Hanquez wrote:
On 07/21/2012 05:12 PM, C Gosch wrote:
Hi Cafe,
and then the server says
(AlertLevel_Fatal,UnexpectedMessage)
I'm not sure whether the ServerHelloDone should happen when resuming.
Does anyone have a hint what may be going wrong?
I am using TLS10 and the tls package with version 0.9.6.
Hi Christian,
Domique is right, a sucessful session resumption should have a Finished
message
after ServerHello.
It's not really clear what's your setup (are you trying to use TLS on
server/client/both ?), and without some code, it's hard to debug your
problem.
The only thing that come to my mind is, did you setup your session callbacks
correctly ?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] TLS 0.9.6, question about session resumption.
I just modified TLS locally on my system to export SessionID and SessionData, and set the session callbacks to storing/retrieving the session data from a Map. After that, the resumption appears to work :-D Thanks a lot for that hint! Is that the way it's meant to be? If yes, how do I get the data types the official way? Cheers, Christian On Mon, 2012-07-23 at 15:33 +0100, Vincent Hanquez wrote: On 07/21/2012 05:12 PM, C Gosch wrote: Hi Cafe, and then the server says (AlertLevel_Fatal,UnexpectedMessage) I'm not sure whether the ServerHelloDone should happen when resuming. Does anyone have a hint what may be going wrong? I am using TLS10 and the tls package with version 0.9.6. Hi Christian, Domique is right, a sucessful session resumption should have a Finished message after ServerHello. It's not really clear what's your setup (are you trying to use TLS on server/client/both ?), and without some code, it's hard to debug your problem. The only thing that come to my mind is, did you setup your session callbacks correctly ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Which ghc binary does ghc-mod use?
Hi, I am a happy user of Emacs with ghc-mod for Haskell programming. There is just one issue I've run into: I have multiple versions of GHC installed on my machine. Now, ghc-mod seems to use the GHC binary that was used to compile ghc-mod itself, but that is not the version I want it to use for syntax checking, etc. In fact, I want to be able to switch ghc-mod between different GHC binaries depending on which project I'm working on, but I have no idea how to do that. Is there maybe some Elisp guru reading this list who can help me out? Can I somehow configure which GHC binary ghc-mod uses? Take care, Peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal install fails due to recent HUnit
On Mon, Jul 23, 2012 at 12:51:32PM -0500, Stephen Paul Weber wrote: Currently you would have to do the upgrade manually, as `cabal-install cabal-install` won't work (or alternatively edit your local ~/.cabl/packages/hackage.haskell.org/00-index.tar). Pending a fix on hackage (hopefully) I've been using `cabal copy cabal register` to grab specific packages today. How would I go about fixing my 00-index.tar? I tride de-tarring, deleting the recent versions of HUnit, and re-tarring, and when I copy that file in cabal starts telling me no packages exist...? E.g. with vim, you can edit files in the tar file (in-place). That is what I did, and it worked fine. Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal install fails due to recent HUnit
On Monday, July 23, 2012, Simon Hengel wrote: On Mon, Jul 23, 2012 at 12:51:32PM -0500, Stephen Paul Weber wrote: Currently you would have to do the upgrade manually, as `cabal-install cabal-install` won't work (or alternatively edit your local ~/.cabl/packages/hackage.haskell.org/00-index.tar). Pending a fix on hackage (hopefully) I've been using `cabal copy cabal register` to grab specific packages today. How would I go about fixing my 00-index.tar? I tride de-tarring, deleting the recent versions of HUnit, and re-tarring, and when I copy that file in cabal starts telling me no packages exist...? E.g. with vim, you can edit files in the tar file (in-place). That is what I did, and it worked fine. I use tar f 00-index.tar --delete Hunit/1.2.5.0/Hunit.cabal Works with GNU tar, not with BSD/mac. Erik ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] TLS 0.9.6, question about session resumption.
On 07/23/2012 06:54 PM, . wrote: I just modified TLS locally on my system to export SessionID and SessionData, and set the session callbacks to storing/retrieving the session data from a Map. After that, the resumption appears to work :-D Thanks a lot for that hint! Is that the way it's meant to be? If yes, how do I get the data types the official way? Cool. this is indeed an omission, it should have been exported. I realized and fixed it couple of weeks ago in the next branch (upcoming tls 1.0) when doing cleanup around session management, but forgot to check master (tls-0.9.x). I've fixed it now, and pushed tls-0.9.8. Thanks, -- Vincent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] TLS 0.9.6, question about session resumption.
Nice, thanks!! Christian Am 23.07.2012 um 22:28 schrieb Vincent Hanquez t...@snarc.org: On 07/23/2012 06:54 PM, . wrote: I just modified TLS locally on my system to export SessionID and SessionData, and set the session callbacks to storing/retrieving the session data from a Map. After that, the resumption appears to work :-D Thanks a lot for that hint! Is that the way it's meant to be? If yes, how do I get the data types the official way? Cool. this is indeed an omission, it should have been exported. I realized and fixed it couple of weeks ago in the next branch (upcoming tls 1.0) when doing cleanup around session management, but forgot to check master (tls-0.9.x). I've fixed it now, and pushed tls-0.9.8. Thanks, -- Vincent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Which ghc binary does ghc-mod use?
On 24 July 2012 04:06, Peter Simons sim...@cryp.to wrote: Hi, I am a happy user of Emacs with ghc-mod for Haskell programming. There is just one issue I've run into: I have multiple versions of GHC installed on my machine. Now, ghc-mod seems to use the GHC binary that was used to compile ghc-mod itself, but that is not the version I want it to use for syntax checking, etc. In fact, I want to be able to switch ghc-mod between different GHC binaries depending on which project I'm working on, but I have no idea how to do that. Is there maybe some Elisp guru reading this list who can help me out? Can I somehow configure which GHC binary ghc-mod uses? Just to get the potentially obvious out of the way: are you sure it's not a matter of which ghc it finds first in the PATH? It might even be using the internal emacs PATH: (getenv PATH) Take care, Peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Which ghc binary does ghc-mod use?
On Mon, Jul 23, 2012 at 2:06 PM, Peter Simons sim...@cryp.to wrote: I am a happy user of Emacs with ghc-mod for Haskell programming. There is just one issue I've run into: I have multiple versions of GHC installed on my machine. Now, ghc-mod seems to use the GHC binary that was used to compile ghc-mod itself, but that is not the version I want it to use for syntax I think you'd have to install a separate ghc-mod binary for each one, then, as it looks to me like ghc-mod is using ghc-as-a-library. That is, it actually has the compiler linked into itself. -- brandon s allbery allber...@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] why does a foldr not have a space leak effect?
Hi, I wonder why a foldr does not have a space leak effect? Any hints? Thanks. Qi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why does a foldr not have a space leak effect?
(Trying again using the real mailing list address rather than google groups) On 24 July 2012 12:37, Qi Qi qiqi...@gmail.com wrote: Hi, I wonder why a foldr does not have a space leak effect? Any hints? Thanks. Why should it? Does it not depend on the function you're folding, the type of data you're folding over, how you use it, etc.? Qi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why does a foldr not have a space leak effect?
Foldl has the space leak effect, and that's why foldl' has been recommended. On Monday, July 23, 2012 9:44:59 PM UTC-5, Ivan Lazar Miljenovic wrote: (Trying again using the real mailing list address rather than google groups) On 24 July 2012 12:37, Qi Qi qiqi...@gmail.com wrote: Hi, I wonder why a foldr does not have a space leak effect? Any hints? Thanks. Why should it? Does it not depend on the function you're folding, the type of data you're folding over, how you use it, etc.? Qi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ 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] why does a foldr not have a space leak effect?
On 24 July 2012 12:52, Qi Qi qiqi...@gmail.com wrote: Foldl has the space leak effect, and that's why foldl' has been recommended. foldl can have a space leak due to accumulation of thunks: foldl f a [b,c,d] = f (f (f a b) c) d ^^ Building up a chain of functions. As such, these thunks are kept around until the result is actually needed. foldl' forces each previous thunk first. foldr f a [b,c,d] = f b (f c (f d a)) ^^ This also builds up a chain of functions... but foldr is typically used in cases where f is lazy in the second argument. For example, and = foldr (); so as soon as it hits one False value, it doesn't need to go on with the rest of the list. Thus, it's not that foldr doesn't necessarily have a space-leak effect; it's just that foldr is used in cases where you're either a) using something that should stop traversing the list when it reaches a certain type of value, or b) you want to preserve the list order (e.g. using foldr to implement map). foldl is used in cases where the entire list _does_ need to be consumed, so the possibility of a space leak becomes more of an issue. Note also the recommendation of foldl' is a bit of a premature optimisation: it isn't _always_ needed (short lists, values are evaluated soon after the fold, etc.), but it's easier to always prefer foldl' over foldl rather than having to go through your code base and selectively replace foldl with foldl'. On Monday, July 23, 2012 9:44:59 PM UTC-5, Ivan Lazar Miljenovic wrote: (Trying again using the real mailing list address rather than google groups) On 24 July 2012 12:37, Qi Qi qiqi...@gmail.com wrote: Hi, I wonder why a foldr does not have a space leak effect? Any hints? Thanks. Why should it? Does it not depend on the function you're folding, the type of data you're folding over, how you use it, etc.? Qi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why does a foldr not have a space leak effect?
This question actually was risen when I read a relevant part in the RWH book. Now it's much clearer to me. Thanks Ivan! On Monday, July 23, 2012 10:04:00 PM UTC-5, Ivan Lazar Miljenovic wrote: On 24 July 2012 12:52, Qi Qi qiqi...@gmail.com wrote: Foldl has the space leak effect, and that's why foldl' has been recommended. foldl can have a space leak due to accumulation of thunks: foldl f a [b,c,d] = f (f (f a b) c) d ^^ Building up a chain of functions. As such, these thunks are kept around until the result is actually needed. foldl' forces each previous thunk first. foldr f a [b,c,d] = f b (f c (f d a)) ^^ This also builds up a chain of functions... but foldr is typically used in cases where f is lazy in the second argument. For example, and = foldr (); so as soon as it hits one False value, it doesn't need to go on with the rest of the list. Thus, it's not that foldr doesn't necessarily have a space-leak effect; it's just that foldr is used in cases where you're either a) using something that should stop traversing the list when it reaches a certain type of value, or b) you want to preserve the list order (e.g. using foldr to implement map). foldl is used in cases where the entire list _does_ need to be consumed, so the possibility of a space leak becomes more of an issue. Note also the recommendation of foldl' is a bit of a premature optimisation: it isn't _always_ needed (short lists, values are evaluated soon after the fold, etc.), but it's easier to always prefer foldl' over foldl rather than having to go through your code base and selectively replace foldl with foldl'. On Monday, July 23, 2012 9:44:59 PM UTC-5, Ivan Lazar Miljenovic wrote: (Trying again using the real mailing list address rather than google groups) On 24 July 2012 12:37, Qi Qi qiqi...@gmail.com wrote: Hi, I wonder why a foldr does not have a space leak effect? Any hints? Thanks. Why should it? Does it not depend on the function you're folding, the type of data you're folding over, how you use it, etc.? Qi ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com http://IvanMiljenovic.wordpress.com ___ 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
