Re: [Haskell-cafe] why does a foldr not have a space leak effect?

[Qi Qi]

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

Re: [Haskell-cafe] why does a foldr not have a space leak effect?

[Ivan Lazar Miljenovic]

On 24 July 2012 12:52, Qi Qi  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  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?

[Qi Qi]

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

[Ivan Lazar Miljenovic]

(Trying again using the real mailing list address rather than google groups)

On 24 July 2012 12:37, Qi Qi  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] why does a foldr not have a space leak effect?

[Qi Qi]

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] Which ghc binary does ghc-mod use?

[Brandon Allbery]

On Mon, Jul 23, 2012 at 2:06 PM, Peter Simons  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

Re: [Haskell-cafe] Which ghc binary does ghc-mod use?

[Ivan Lazar Miljenovic]

On 24 July 2012 04:06, Peter Simons  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] TLS 0.9.6, question about session resumption.

[C Gosch]

Nice, thanks!!
Christian




Am 23.07.2012 um 22:28 schrieb Vincent Hanquez :

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

[Vincent Hanquez]

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] Cabal install fails due to recent HUnit

[Erik Hesselink]

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] Cabal install fails due to recent HUnit

[Simon Hengel]

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

[Haskell-cafe] Which ghc binary does ghc-mod use?

[Peter Simons]

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

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.

[Vincent Hanquez]

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] specifying using type class

[Ertugrul Söylemez]

Patrick Browne  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] specifying using type class

[Patrick Browne]

Dominique,That is exactly the information that I required.Thank you very much,PatOn 23/07/12, Dominique Devriese   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

[Dominique Devriese]

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

[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 
) 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 

> 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 *  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 >
>
>>
>>
>> On 22/07/12, *Ertugrul Söylemez * > 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 teachtairea

Re: [Haskell-cafe] Need help with learning Parsec

[C K Kashyap]

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
wrote:

> 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] Haskell's type inference considered harmful

[Andreas Abel]

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 Abel  <><  Du 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
Has

Re: [Haskell-cafe] 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   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 >

On 22/07/12, Ertugrul Söylemez  > 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 
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] Need help with learning Parsec

[Christian Maeder]

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

[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 

>
>
> On 22/07/12, *Ertugrul Söylemez *  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

[Patrick Browne]

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