Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell

2010-05-27 Thread Ketil Malde
b...@telenet.be writes:

 Or maybe this would be a nice research topic: how to generate C code
 that looks like it’s human written…  

Nah, that's too easy: just add a sprinkling of buffer overflows,
undefined behavior, and off-by one index errors.

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.

2010-05-27 Thread Magicloud Magiclouds
I only have one alex installed under ~/.cabal/bin.
It seems working with shell environment, but not cabal.

On Thu, May 27, 2010 at 1:40 PM, Axel Simon axel.si...@in.tum.de wrote:
 Hi Magicloud,

 On May 27, 2010, at 4:11, Magicloud Magiclouds wrote:

 Hi, I have met similar problem before, and I do not know what to do.

 # cabal install --reinstall gtk2hs-buildtools
 Resolving dependencies...
 Configuring gtk2hs-buildtools-0.9...
 cabal: alex is required but it could not be found.
 cabal: Error: some packages failed to install:
 gtk2hs-buildtools-0.9 failed during the configure step. The exception was:
 ExitFailure 1
 # alex -v
 Alex version 2.3.3, (c) 2003 Chris Dornan and Simon Marlow

 I don't think this is due to us. Are there perhaps other alex installations
 on your path? Or in ~/.cabal/bin?

 Axel


 --
 竹密岂妨流水过
 山高哪阻野云飞


 --

 ___
 Gtk2hs-users mailing list
 gtk2hs-us...@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/gtk2hs-users





-- 
竹密岂妨流水过
山高哪阻野云飞
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Jasper Van der Jeugt
Dear all,

BlazeHtml started out on ZuriHac 2010. Now, Jasper Van der Jeugt is
working on it as a student to Google Summer of Code for haskell.org.
His mentors are Simon Meier and Johan Tibell. The goal is to create a
high-performance HTML generation library.

In the past few weeks, we have been exploring the performance and
design of different drafts of this library. Now, the time has come to
ask some questions to the Haskell community — more specifically the
future users of BlazeHtml as well as current users of other HTML
generation libraries.

We have written an RFC to gather feedback from the community:

HTML version: http://jaspervdj.be/posts/2010-05-27-blazehtml-rfc.html
Plain version: http://github.com/jaspervdj/BlazeHtml/raw/develop/doc/RFC.lhs

The easiest way of sending us feedback, comments or criticism is
replying to the haskell-cafe thread here. Alternatively, drop a
comment at the bottom of the HTML version or at reddit.

Looking forward to your feedback,
Kind regards,
Simon Meier
Jasper Van der Jeugt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.

2010-05-27 Thread Ivan Miljenovic
On 27 May 2010 16:46, Magicloud Magiclouds
magicloud.magiclo...@gmail.com wrote:
 I only have one alex installed under ~/.cabal/bin.
 It seems working with shell environment, but not cabal.

This sounds like a similar problem to one that occurred a couple of months ago.

If you use ~/.cabal/bin/ for your PATH variable, try replacing that
with $HOME/.cabal/bin/.


 On Thu, May 27, 2010 at 1:40 PM, Axel Simon axel.si...@in.tum.de wrote:
 Hi Magicloud,

 On May 27, 2010, at 4:11, Magicloud Magiclouds wrote:

 Hi, I have met similar problem before, and I do not know what to do.

 # cabal install --reinstall gtk2hs-buildtools
 Resolving dependencies...
 Configuring gtk2hs-buildtools-0.9...
 cabal: alex is required but it could not be found.
 cabal: Error: some packages failed to install:
 gtk2hs-buildtools-0.9 failed during the configure step. The exception was:
 ExitFailure 1
 # alex -v
 Alex version 2.3.3, (c) 2003 Chris Dornan and Simon Marlow

 I don't think this is due to us. Are there perhaps other alex installations
 on your path? Or in ~/.cabal/bin?

 Axel


 --
 竹密岂妨流水过
 山高哪阻野云飞


 --

 ___
 Gtk2hs-users mailing list
 gtk2hs-us...@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/gtk2hs-users





 --
 竹密岂妨流水过
 山高哪阻野云飞
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] currying combinators

2010-05-27 Thread wren ng thornton

David Sankel wrote:

keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b

On Wed, May 26, 2010 at 12:49 PM, Lennart Augustsson lenn...@augustsson.net

wrote:



There are no interesting (i.e. total) functions of that type.



I wonder how one would prove that to be the case. I tried and didn't come up
with anything.


By parametricty, presumably.

We must ultimately construct some value of type b, where b is 
universally quantified. Therefore, the only 'constructors' available for 
b are the ((t - b) - u - b) and ((t1 - t) - b) arguments. However, 
since b is universally quantified, these arguments have no way of 
actually constructing some b, other than by returning bottom.


Remember, if a language lacks typecase, (forall a. X - a) is just 
another way of saying (X - Void).


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Michael Snoyman
Two comments:

* The exclamation point seems good enough for attributes. I copied that for
Hamlet as well.

* If you're standardizing on UTF-8, why not support bytestrings? I'm aware
that a user could shoot him/herself in the foot by passing in non-UTF8 data,
but I would imagine the performance gains would outweigh this. My recent
benchmarks on the BigTable benchmark[1] imply a huge performance gap between
ByteStrings and other contenders.

As we've discussed before, I think combining BlazeHtml and Hamlet would be
very nice, though I'm dubious that a BlazeHtml backend for Hamlet would be
faster than a raw backend.

Looking forward to hearing more progress, good luck!
Michael

[1] http://www.snoyman.com/blog/entry/bigtable-benchmarks/

On Thu, May 27, 2010 at 10:16 AM, Jasper Van der Jeugt
jasper...@gmail.comwrote:

 Dear all,

 BlazeHtml started out on ZuriHac 2010. Now, Jasper Van der Jeugt is
 working on it as a student to Google Summer of Code for haskell.org.
 His mentors are Simon Meier and Johan Tibell. The goal is to create a
 high-performance HTML generation library.

 In the past few weeks, we have been exploring the performance and
 design of different drafts of this library. Now, the time has come to
 ask some questions to the Haskell community — more specifically the
 future users of BlazeHtml as well as current users of other HTML
 generation libraries.

 We have written an RFC to gather feedback from the community:

 HTML version: http://jaspervdj.be/posts/2010-05-27-blazehtml-rfc.html
 Plain version:
 http://github.com/jaspervdj/BlazeHtml/raw/develop/doc/RFC.lhs

 The easiest way of sending us feedback, comments or criticism is
 replying to the haskell-cafe thread here. Alternatively, drop a
 comment at the bottom of the HTML version or at reddit.

 Looking forward to your feedback,
 Kind regards,
 Simon Meier
 Jasper Van der Jeugt
 ___
 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] Re: [Gtk2hs-users] Problem when installing gtk2hs.

2010-05-27 Thread Magicloud Magiclouds
That might be it. However, I linked ~/.cabal/bin/* to
/usr/local/bin And it worked.

On Thu, May 27, 2010 at 3:24 PM, Ivan Miljenovic
ivan.miljeno...@gmail.com wrote:
 On 27 May 2010 16:46, Magicloud Magiclouds
 magicloud.magiclo...@gmail.com wrote:
 I only have one alex installed under ~/.cabal/bin.
 It seems working with shell environment, but not cabal.

 This sounds like a similar problem to one that occurred a couple of months 
 ago.

 If you use ~/.cabal/bin/ for your PATH variable, try replacing that
 with $HOME/.cabal/bin/.


 On Thu, May 27, 2010 at 1:40 PM, Axel Simon axel.si...@in.tum.de wrote:
 Hi Magicloud,

 On May 27, 2010, at 4:11, Magicloud Magiclouds wrote:

 Hi, I have met similar problem before, and I do not know what to do.

 # cabal install --reinstall gtk2hs-buildtools
 Resolving dependencies...
 Configuring gtk2hs-buildtools-0.9...
 cabal: alex is required but it could not be found.
 cabal: Error: some packages failed to install:
 gtk2hs-buildtools-0.9 failed during the configure step. The exception was:
 ExitFailure 1
 # alex -v
 Alex version 2.3.3, (c) 2003 Chris Dornan and Simon Marlow

 I don't think this is due to us. Are there perhaps other alex installations
 on your path? Or in ~/.cabal/bin?

 Axel


 --
 竹密岂妨流水过
 山高哪阻野云飞


 --

 ___
 Gtk2hs-users mailing list
 gtk2hs-us...@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/gtk2hs-users





 --
 竹密岂妨流水过
 山高哪阻野云飞
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




 --
 Ivan Lazar Miljenovic
 ivan.miljeno...@gmail.com
 IvanMiljenovic.wordpress.com




-- 
竹密岂妨流水过
山高哪阻野云飞
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Ivan Miljenovic
On 27 May 2010 17:55, Michael Snoyman mich...@snoyman.com wrote:
 Two comments:
 * The exclamation point seems good enough for attributes. I copied that for
 Hamlet as well.
 * If you're standardizing on UTF-8, why not support bytestrings? I'm aware
 that a user could shoot him/herself in the foot by passing in non-UTF8 data,
 but I would imagine the performance gains would outweigh this. My recent
 benchmarks on the BigTable benchmark[1] imply a huge performance gap between
 ByteStrings and other contenders.

Wow, I find it rather surprising that String out-performs Text; any
idea why that is?  I wonder if you're just using it wrong...

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Mujtaba Boori
*Pete Chown and Dan Doel. Thank you for your solution. I actually It was not
homework . It was just a a past exam question trying to answer . *
**but your solution is very long , so I don't think he wants answer this
long in the exams. I think this answer agree100 f g = map f xs == map g xs
where xs = [1..100] from  Richard O'Keefe
is do the job.

**Anyway , your solution help understand more about Haskell not only this
question . Many thanks to you guys.

On 27 May 2010 02:04, Dan Doel dan.d...@gmail.com wrote:

 On Wednesday 26 May 2010 5:38:57 pm Pete Chown wrote:
  test :: (Eq a) = (Int - a) - (Int - a) - Bool
  test f1 f2 = unsafePerformIO $ do
   goodSoFar - newIORef True
   forLoop 1 100 $ \i -
 when (f1 i /= f2 i) $ writeIORef goodSoFar False
   readIORef goodSoFar

 The problem with this algorithm is that it needlessly tests f1 against f2
 for
 all i, even when a non-matching value has has already been found. Using the
 power of call-with-current-continuation, I have constructed an algorithm
 that
 lacks this deficiency:

import Control.Monad.Cont

test f g = flip runCont id . callCC $ \escape -
  do forM_ [1..100] $ \n -
   when (f n /= g n) $
 escape False
 return True

 This should perform almost 75% less work in the testFunc1 case! It
 certainly
 feels much snappier.

 -- Dan
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Mujtaba Ali Alboori
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Michael Snoyman
On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic ivan.miljeno...@gmail.com
 wrote:

 On 27 May 2010 17:55, Michael Snoyman mich...@snoyman.com wrote:
  Two comments:
  * The exclamation point seems good enough for attributes. I copied that
 for
  Hamlet as well.
  * If you're standardizing on UTF-8, why not support bytestrings? I'm
 aware
  that a user could shoot him/herself in the foot by passing in non-UTF8
 data,
  but I would imagine the performance gains would outweigh this. My recent
  benchmarks on the BigTable benchmark[1] imply a huge performance gap
 between
  ByteStrings and other contenders.

 Wow, I find it rather surprising that String out-performs Text; any
 idea why that is?  I wonder if you're just using it wrong...

 Could be, I'd be very happy if that were the case. All of the benchmarks
are available on Github, and the bytestring[1], text[2] and string[3]
versions are all rather short.

Michael

[1]
http://github.com/snoyberg/benchmarks/blob/master/bigtable/cgi/bytestring.hs
[2] http://github.com/snoyberg/benchmarks/blob/master/bigtable/cgi/text.hs
[3] http://github.com/snoyberg/benchmarks/blob/master/bigtable/cgi/string.hs
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Ivan Miljenovic
On 27 May 2010 18:23, Michael Snoyman mich...@snoyman.com wrote:


 On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic
 ivan.miljeno...@gmail.com wrote:

 On 27 May 2010 17:55, Michael Snoyman mich...@snoyman.com wrote:
  Two comments:
  * The exclamation point seems good enough for attributes. I copied that
  for
  Hamlet as well.
  * If you're standardizing on UTF-8, why not support bytestrings? I'm
  aware
  that a user could shoot him/herself in the foot by passing in non-UTF8
  data,
  but I would imagine the performance gains would outweigh this. My recent
  benchmarks on the BigTable benchmark[1] imply a huge performance gap
  between
  ByteStrings and other contenders.

 Wow, I find it rather surprising that String out-performs Text; any
 idea why that is?  I wonder if you're just using it wrong...

 Could be, I'd be very happy if that were the case. All of the benchmarks are
 available on Github, and the bytestring[1], text[2] and string[3] versions
 are all rather short.

Does using lazy Text values improve this?  I find it a little strange
that you concatenate so many individual Strings that much.  Also, how
about explicitly using Text values rather than OverloadedStrings?

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Michael Snoyman
On Thu, May 27, 2010 at 11:28 AM, Ivan Miljenovic ivan.miljeno...@gmail.com
 wrote:

 On 27 May 2010 18:23, Michael Snoyman mich...@snoyman.com wrote:
 
 
  On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic
  ivan.miljeno...@gmail.com wrote:
 
  On 27 May 2010 17:55, Michael Snoyman mich...@snoyman.com wrote:
   Two comments:
   * The exclamation point seems good enough for attributes. I copied
 that
   for
   Hamlet as well.
   * If you're standardizing on UTF-8, why not support bytestrings? I'm
   aware
   that a user could shoot him/herself in the foot by passing in non-UTF8
   data,
   but I would imagine the performance gains would outweigh this. My
 recent
   benchmarks on the BigTable benchmark[1] imply a huge performance gap
   between
   ByteStrings and other contenders.
 
  Wow, I find it rather surprising that String out-performs Text; any
  idea why that is?  I wonder if you're just using it wrong...
 
  Could be, I'd be very happy if that were the case. All of the benchmarks
 are
  available on Github, and the bytestring[1], text[2] and string[3]
 versions
  are all rather short.

 Does using lazy Text values improve this?  I find it a little strange
 that you concatenate so many individual Strings that much.  Also, how
 about explicitly using Text values rather than OverloadedStrings?

 I don't do any string concatenation (look closely), I was very careful to
avoid it. I tried with lazy text as well: it was slower. This isn't
surprising, since lazy text- under the surface- is just a list of strict
text. And the benchmark itself already has a lazy list of strict text. Using
lazy text would just be adding a layer of wrapping.

I don't know what you mean by explicitly using Text values; you mean
calling pack manually? That's really all that OverloadedStrings does.

You can try out lots of different variants on that benchmark. I did that
already, and found this to be the fastest version.

Michael
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Bas van Dijk
Q14: Do you see any problems with respect to integrating BlazeHtml in
your favourite web-framework/server?

How about also providing an enumerator back-end?
http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM

Then your library can integrate more easily with the snap framework:
http://snapframework.com

Regards,

Bas
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Ivan Miljenovic
On 27 May 2010 18:33, Michael Snoyman mich...@snoyman.com wrote:
 I don't do any string concatenation (look closely), I was very careful to
 avoid it. I tried with lazy text as well: it was slower. This isn't
 surprising, since lazy text- under the surface- is just a list of strict
 text. And the benchmark itself already has a lazy list of strict text. Using
 lazy text would just be adding a layer of wrapping.
 I don't know what you mean by explicitly using Text values; you mean
 calling pack manually? That's really all that OverloadedStrings does.
 You can try out lots of different variants on that benchmark. I did that
 already, and found this to be the fastest version.

Fair enough.  Now that I think about it, I recall once trying to have
pretty generate Text values rather than String for graphviz (by using
fullRender, so it was still using String under the hood until it came
time to render) and it too was much slower than String (unfortunately,
I didn't record a patch with these changes so I can't just go back and
play with it anymore as I reverted them all :s).

Maybe Bryan can chime in with some best-practices for using Text?

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Michael Snoyman
On Thu, May 27, 2010 at 11:40 AM, Ivan Miljenovic ivan.miljeno...@gmail.com
 wrote:

 On 27 May 2010 18:33, Michael Snoyman mich...@snoyman.com wrote:
  I don't do any string concatenation (look closely), I was very careful to
  avoid it. I tried with lazy text as well: it was slower. This isn't
  surprising, since lazy text- under the surface- is just a list of strict
  text. And the benchmark itself already has a lazy list of strict text.
 Using
  lazy text would just be adding a layer of wrapping.
  I don't know what you mean by explicitly using Text values; you mean
  calling pack manually? That's really all that OverloadedStrings does.
  You can try out lots of different variants on that benchmark. I did that
  already, and found this to be the fastest version.

 Fair enough.  Now that I think about it, I recall once trying to have
 pretty generate Text values rather than String for graphviz (by using
 fullRender, so it was still using String under the hood until it came
 time to render) and it too was much slower than String (unfortunately,
 I didn't record a patch with these changes so I can't just go back and
 play with it anymore as I reverted them all :s).

 Maybe Bryan can chime in with some best-practices for using Text?

 Here's my guess at an explanation for what's happening in my benchmark:

text will clearly beat String in memory usage, that's what it's designed
for. However, the compiler is still generating String values which are being
encoded to Text as runtime.

Now, this is the same process for bytestrings. However, bytestrings never
have to be decoded: the IO routines simply read the character buffer. In the
case of text, however, the encoded data must be decoded again to a
bytestring.

In other words, here's what I think the three different benchmarks are
really doing:

* String: generates a list of Strings, passes each String to a relatively
inefficient IO routine.
* ByteString: encodes Strings one by one into ByteStrings, generates a list
of these ByteStrings, and passes each ByteString to a very efficient IO
routine.
: Text: encodes Strings one by one into Texts, generates a list of these
Texts, calls a UTF-8 decoding function to decode each Text into a
ByteString, and passes each resulting ByteString to a very efficient IO
routine.

In the case of ASCII data to be output as UTF-8, uses the
Data.ByteString.Char8.pack function will most likely always be the most
efficient choice, and thus it seems like something BlazeHtml should support.
I'm considering releasing a Hamlet 0.3 based entirely on UTF-8 encoded
ByteStrings, but I'd also like to hear from Bryan about this.

Michael
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Jasper Van der Jeugt
Hey Bas,

 How about also providing an enumerator back-end?
 http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM

 Then your library can integrate more easily with the snap framework:
 http://snapframework.com

Sure, I can do that. But I already tested integration with the snap
framework, the best path here seems to call the `writeLBS` function
from the snap framework on the `L.ByteString` that BlazeHtml produces
(`writeLBS` internally uses an enumerator).

Kind regards,
Jasper Van der Jeugt

On Thu, May 27, 2010 at 10:38 AM, Bas van Dijk v.dijk@gmail.com wrote:
 Q14: Do you see any problems with respect to integrating BlazeHtml in
 your favourite web-framework/server?

 How about also providing an enumerator back-end?
 http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM

 Then your library can integrate more easily with the snap framework:
 http://snapframework.com

 Regards,

 Bas

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Ketil Malde
Michael Snoyman mich...@snoyman.com writes:

 * If you're standardizing on UTF-8, why not support bytestrings? 

+1

 I'm aware that a user could shoot him/herself in the foot by passing
 in non-UTF8 data, but I would imagine the performance gains would outweigh 
 this.

Wrap them in a (new)type?

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Announce : New haskell-llvm mailing list.

2010-05-27 Thread Erik de Castro Lopo
Hi all,

I have set up a mailing list for discussion of haskell and LLVM related
topics.

All discussion on using Haskell with LLVM is relevant. That includes
the haskell-llvm bindings on Hackage, custom LLVM bindings and
directly generating LLVM IR code from haskell and passing that
through the LLVM tools.

In particular, this list is a place to share code, information,
techniques and user experiences.

The subscription page is here:

http://projects.haskell.org/cgi-bin/mailman/listinfo/haskell-llvm

Cheers,
Erik
-- 
--
Erik de Castro Lopo
http://www.mega-nerd.com/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Bas van Dijk
On Thu, May 27, 2010 at 10:48 AM, Jasper Van der Jeugt
jasper...@gmail.com wrote:
 How about also providing an enumerator back-end?
 http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM

 Then your library can integrate more easily with the snap framework:
 http://snapframework.com

 Sure, I can do that. But I already tested integration with the snap
 framework, the best path here seems to call the `writeLBS` function
 from the snap framework on the `L.ByteString` that BlazeHtml produces
 (`writeLBS` internally uses an enumerator).

I think it's worth analyzing if using enumerators directly gives a
significant performance improvement over converting from lazy
ByteStrings.

Looking a the conversion functions in the snap framework it looks like
we can avoid some intermediate lists for one:

writeLBS :: L.ByteString - Snap ()
writeLBS s = addToOutput $ enumLBS s

addToOutput :: (forall a . Enumerator a) - Snap ()
addToOutput enum = modifyResponse $ modifyResponseBody (. enum)

enumLBS :: (Monad m) = L.ByteString - Enumerator m a
enumLBS lbs iter = foldM k iter enums
  where
enums = map (enumPure1Chunk . WrapBS) $ L.toChunks lbs
k i e = e i

-- from iteratee:
enumPure1Chunk :: (SC.StreamChunk s el, Monad m) =
  s el -
  EnumeratorGM s el m a
enumPure1Chunk str iter = runIter iter (Chunk str) = checkIfDone return

Regards,

Bas
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Johan Tibell
On Thu, May 27, 2010 at 10:23 AM, Michael Snoyman mich...@snoyman.comwrote:

 On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic 
 ivan.miljeno...@gmail.com wrote:

 Wow, I find it rather surprising that String out-performs Text; any
 idea why that is?  I wonder if you're just using it wrong...

 Could be, I'd be very happy if that were the case. All of the benchmarks
 are available on Github, and the bytestring[1], text[2] and string[3]
 versions are all rather short.


Do you include the cost of encoding the result as e.g. UTF-8? The hope would
be that the more compact Text would be faster to traverse, and thus encode,
than the list based String.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Michael Snoyman
On Thu, May 27, 2010 at 12:57 PM, Johan Tibell johan.tib...@gmail.comwrote:

 On Thu, May 27, 2010 at 10:23 AM, Michael Snoyman mich...@snoyman.comwrote:

 On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic 
 ivan.miljeno...@gmail.com wrote:

 Wow, I find it rather surprising that String out-performs Text; any
 idea why that is?  I wonder if you're just using it wrong...

 Could be, I'd be very happy if that were the case. All of the benchmarks
 are available on Github, and the bytestring[1], text[2] and string[3]
 versions are all rather short.


 Do you include the cost of encoding the result as e.g. UTF-8? The hope
 would be that the more compact Text would be faster to traverse, and thus
 encode, than the list based String.

 No, but this is done on purpose. One of my goals in this benchmark was to
determine whether I should consider switching Hamlet to ByteStrings. If I
were to do so, then the UTF-8 encoding would be done at compile-time instead
of run-time.

You're correct that a fair comparison would be to UTF-8 encode the Strings
as well. However, that's not what most users are going to do most of the
time: when dealing with ASCII data, a straight Char8.pack encoding will do
the same as UTF-8. I'm simply pointing out that I think Blaze should support
this style.

Michael
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Johan Tibell
On Thu, May 27, 2010 at 10:53 AM, Michael Snoyman mich...@snoyman.comwrote:

 In other words, here's what I think the three different benchmarks are
 really doing:

 * String: generates a list of Strings, passes each String to a relatively
 inefficient IO routine.
 * ByteString: encodes Strings one by one into ByteStrings, generates a list
 of these ByteStrings, and passes each ByteString to a very efficient IO
 routine.
 : Text: encodes Strings one by one into Texts, generates a list of these
 Texts, calls a UTF-8 decoding function to decode each Text into a
 ByteString, and passes each resulting ByteString to a very efficient IO
 routine.


If Text used UTF-8 internally rather than UTF-16 we could create Texts from
string literals much more efficiently, in the same manner as done in
Char8.pack for bytestrings:

{-# RULES
   FPS pack/packAddress forall s .
  pack (unpackCString# s) = inlinePerformIO (B.unsafePackAddress s)
 #-}

This rule skips the creation of an intermediate String when packing a string
literal by having the created ByteString point directly to the memory GHC
allocates (outside the heap) for the string literal. This rule could be
added directly to a builder monoid for lazy Texts so that no copying is done
at all. In addition, if Text was internally represented using UTF-8
encodeUtf8 would be free.

Johan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Alberto G. Corona
As a user, I have too many HTML generators, a few of them with Ajax and none
with server-side event handling (like ASPX or JSPX).  Ajax is complicated
but server side event handling is  what I really miss because it is simple
 from the user point of view, my ervents could be handled in haskell code
rather than in javaScript and I  implicitly could  use the advantages of
 dinamic HTML and Ajax without the need to know them at all.

Imagine a dynamic Web application  with 100% haskell code made with dynamic
widgets created by third party developers.

So, anyone want to create a HTML templating system with server side event
handling? It is not terribly hard to do. (I refer to ASP.NET documentation
or the JavaServer Faces framework).

By the way, I vote for XML templating or else, combinator templating that
produce XHML templating because it can be handled by a future graphical IDE.

2010/5/27 Jasper Van der Jeugt jasper...@gmail.com

 Hey Bas,

  How about also providing an enumerator back-end?
 
 http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM
 
  Then your library can integrate more easily with the snap framework:
  http://snapframework.com

 Sure, I can do that. But I already tested integration with the snap
 framework, the best path here seems to call the `writeLBS` function
 from the snap framework on the `L.ByteString` that BlazeHtml produces
 (`writeLBS` internally uses an enumerator).

 Kind regards,
 Jasper Van der Jeugt

 On Thu, May 27, 2010 at 10:38 AM, Bas van Dijk v.dijk@gmail.com
 wrote:
  Q14: Do you see any problems with respect to integrating BlazeHtml in
  your favourite web-framework/server?
 
  How about also providing an enumerator back-end?
 
 http://hackage.haskell.org/packages/archive/iteratee/0.3.5/doc/html/Data-Iteratee-Base.html#t%3AEnumeratorGM
 
  Then your library can integrate more easily with the snap framework:
  http://snapframework.com
 
  Regards,
 
  Bas
 
 ___
 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] Re: [Gtk2hs-users] Problem when installing gtk2hs.

2010-05-27 Thread Daniel Fischer
On Thursday 27 May 2010 08:46:04, Magicloud Magiclouds wrote:
 I only have one alex installed under ~/.cabal/bin.
 It seems working with shell environment, but not cabal.


My guess:

You added ~/.cabal/bin to the path, but have quoted the path, like

export PATH=~/.cabal/bin:$PATH

in your .bashrc

That does not work. Tilde expansion is *not* done for quoted strings, so 
cabal looks (among other places) for ~/.cabal/bin/alex. Now, there is no 
directory ~ in your file system, so alex is not found.

Check:
$ printenv PATH

If the output contains ~, it won't work. If it doesn't, well then something 
else must be broken.

Fixes
1) don't quote the path,
export PATH=~/.cabal/bin:$PATH
works.
2) (better) Use $HOME instead of ~ (works quoted or unquoted)
3) write out your home directory completely
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Yitzchak Gale
Mujtaba Boori wrote:
 I think this answer agree100 f g = map f xs == map g xs where
 xs = [1..100] from  Richard O'Keefe
 is do the job.

agree100 = (==) `on` for [1..100]

Regards,
Yitz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell

2010-05-27 Thread Pierre-Etienne Meunier
There is a enormous bunch of C code out there on the internet. It is not that 
hard to simply take arbitrary commentaries and variable names from it, then 
using it to replace GHC's jjaksh34$-like variables in the core.

Doing objective-c is a bit harder, as you have to use the objects, or else the 
choice of objective-c instead of c would look suspicious. This requires to find 
the rules that make an object programmer happy.


El 27/05/2010, a las 02:40, Ketil Malde escribió:

 b...@telenet.be writes:
 
 Or maybe this would be a nice research topic: how to generate C code
 that looks like it’s human written…  
 
 Nah, that's too easy: just add a sprinkling of buffer overflows,
 undefined behavior, and off-by one index errors.
 
 -k
 -- 
 If I haven't seen further, it is by standing in the footprints of giants
 ___
 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] Google Summer of Code: BlazeHTML RFC

2010-05-27 Thread Pierre-Etienne Meunier
** Advertisement **
Have you tried the library I have written, Data.Rope ?
** End of advertisement **

The algorithmic complexity of most operations on ropes is way better than on 
bytestrings : log n for all operations, except traversals, of course.

Cheers,
PE



El 27/05/2010, a las 06:01, Michael Snoyman escribió:

 
 
 On Thu, May 27, 2010 at 12:57 PM, Johan Tibell johan.tib...@gmail.com wrote:
 On Thu, May 27, 2010 at 10:23 AM, Michael Snoyman mich...@snoyman.com wrote:
 On Thu, May 27, 2010 at 11:16 AM, Ivan Miljenovic ivan.miljeno...@gmail.com 
 wrote:
 Wow, I find it rather surprising that String out-performs Text; any
 idea why that is?  I wonder if you're just using it wrong...
 
 Could be, I'd be very happy if that were the case. All of the benchmarks are 
 available on Github, and the bytestring[1], text[2] and string[3] versions 
 are all rather short.
 
 Do you include the cost of encoding the result as e.g. UTF-8? The hope would 
 be that the more compact Text would be faster to traverse, and thus encode, 
 than the list based String.
 
 No, but this is done on purpose. One of my goals in this benchmark was to 
 determine whether I should consider switching Hamlet to ByteStrings. If I 
 were to do so, then the UTF-8 encoding would be done at compile-time instead 
 of run-time.
 
 You're correct that a fair comparison would be to UTF-8 encode the Strings as 
 well. However, that's not what most users are going to do most of the time: 
 when dealing with ASCII data, a straight Char8.pack encoding will do the same 
 as UTF-8. I'm simply pointing out that I think Blaze should support this 
 style.
 
 Michael
 ___
 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


[Haskell-cafe] Re: Unicode vs. System.Directory

2010-05-27 Thread Andy Stewart
Hi Arie,

If you don't mind binding code.
You can try to use GIO APIs from my repository:
http://patch-tag.com/r/AndyStewart/gio-branch/home

GIO APIs handle unicode filename every well, and cross-platform.

Cheers,

  -- Andy

Arie Peterson ar...@xs4all.nl writes:

 After upgrading to haskell-platform-2010.1.0.0, with the improved unicode
 support for IO in ghc-6.12, I hoped to be able to deal with filenames
 containing non-ascii characters. This still seems problematic, though:

 $ ls
 m×n♯α
 $ ghci
 GHCi, version 6.12.1: http://www.haskell.org/ghc/  :? for help
 Prelude :m +System.Directory 
 Prelude System.Directory getDirectoryContents . = mapM_ putStrLn
 ..
 mÃnâ¯Î±
 .

 I hope this passes through the various email systems unharmed; on my
 terminal, the output of 'ls' contains shiny unicode characters, while
 'ghci' garbles up the filename. (My locale is en_GB.utf8.)

 Similar problems arise with functions such as 'copyFile', which refuses to
 handle filenames with non-ascii characters (unless wrapping it with
 encoding functions).


 Is this a known problem? I searched ghc's trac, but there are no relevant
 bugs for the component 'libraries/directory'.


 I have parts of a unicode-aware layer on top of System.Directory laying
 around somewhere. I was rather hoping to ditch it, but I can polish it and
 put it on hackage, if people are interested.


 Kind regards,

 Arie

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Ionut G. Stan

Hi,

I was just wondering if there's any particular reason for which the two 
constructors of the Either data type are named Left and Right. I'm 
thinking that something like Success | Failure or Right | Wrong would 
have been a little better.


I've recently seen that Scala uses a similar convention for some error 
notifications so I'm starting to believe there's more background behind 
it than just an unfortunate naming.


Thanks,
--
Ionuț G. Stan  |  http://igstan.ro
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Günther Schmidt

Hi all,

I'm exploring the use of church encodings of algebraic data types in 
Haskell.
Since it's hard to imagine being the first to do so I wonder if folks 
here could point me to some references on the subject.


I'm looking for examples of church encodings in Haskell a little bit 
beyond Church Booleans and Church Numerals.


Günther


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma

2010-05-27 Thread Carlos Camarao
On 05/26/10 15:42, Carlos Camarao wrote:

 I think you are proposing using the current set of instances in
 scope in order to remove ambiguity.  Am I right?

I think that an important point is that it is not exactly to remove
ambiguity, because the proposal tries to solve the problem exactly
when there is really no ambiguity. There would be ambiguity if there
were two or more conflicting definitions, and the proposal is to use,
upon occurrence of an unreachable type variable in a constraint, an
instance in the current context that is the single instance that could
be used to instantiate that type variable.

This was perhaps made unclear when I incorrectly wrote in haskell-cafe
that the proposal eliminates the need for defaulting. I should have
said that defaulting is not necessary to force instantiation (of
unreachable variables) when there are no conflicting definitions in
the current context. That is, defaulting should be used exactly to
remove ambiguity, i.e. when there exist conflicting definitions and
when unreachable type variables appear that can be instantiated to
such conflicting definitions.

 Your proposal appears to allow /incoherent/ instance selection.
 This means that an expression can be well-typed in one module, and
 well-typed in another module, but have different semantics in the
 two modules.  For example (drawing from above discussion) :

 module C where

 class F a b where f :: a - b
 class O a where o :: a

 module P where
 import C

 instance F Bool Bool where f = not
 instance O Bool where o = True
 k :: Bool
 k = f o

 module Q where
 import C
 instance F Int Bool where f = even
 instance O Int where o = 0
 k :: Bool
 k = f o

 module Main where
 import P
 import Q
 -- (here, all four instances are in scope)
 main = do { print P.k ; print Q.k }
 -- should result, according to your proposal, in
 -- False
 -- True
 -- , am I correct?

If qualified importation of k from both P and from Q was specified, we
would have two *distinct* terms, P.k and Q.k.

Unqualified importation must cause an error (two distinct definitions
for the same non-overloaded name).

For overloaded names with distinct instances, *ambiguity* would be reported,
as e.g. in:

  module C where class O a where o::a
  module P where instance O Bool where o = True
  module Q where instance O Bool where o = False
  moduke Main where
import P
import Q
main = do { print o::Bool }

 Also, in your paper, example 2 includes
m = (m1 * m2) * m3
 and you state
 In Example 2, there is no means of specializing type variable c0
 occurring in the type of m to Matrix.
 In Example 2, there is no means of specializing type variable c0
 occurring in the type of m to Matrix.
 I suggest that there is an appropriate such means, namely, to write
 m = (m1 * m2 :: Matrix) * m3

Yes, that solution is fine. Sorry, I should have written There is no means
of specializing type variable c0 occurring in the type of m to Matrix,
without an explicit type annotation in the expression defining m.

 (Could the paper address how that solution falls short?
 Are there other cases in which there is more than just a little
 syntactical convenience at stake?
 , or is even that much added code too much for some use-case?)

The point should have been that you cannot make a class with
FDs eliminate the need for having to make explicit type annotations,
in cases such as these. The example should also be such that it
would need more type annotations, instead of just one...

Cheers,

Carlos
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Vo Minh Thu
2010/5/27 Ionut G. Stan ionut.g.s...@gmail.com:
 Hi,

 I was just wondering if there's any particular reason for which the two
 constructors of the Either data type are named Left and Right. I'm thinking
 that something like Success | Failure or Right | Wrong would have been a
 little better.

 I've recently seen that Scala uses a similar convention for some error
 notifications so I'm starting to believe there's more background behind it
 than just an unfortunate naming.

Hi,

Either *can* be used to represent success and failures, but not
necessarily. It is a convention, when using Either to model
success/failure, to use Right for success and Left for failure. Even
if Left as a word does not match with the meaning of failure, it is
easy to get it Right :)

Cheers,
Thu
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Thomas Davie

On 27 May 2010, at 15:25, Ionut G. Stan wrote:

 Hi,
 
 I was just wondering if there's any particular reason for which the two 
 constructors of the Either data type are named Left and Right. I'm thinking 
 that something like Success | Failure or Right | Wrong would have been a 
 little better.

The reason I guess is that Success/Failure and Right/Wrong are a lot less 
general than Left/Right.  One can use Either for types with two possible valid 
types contained within, it doesn't only have to be used for types where one is 
for correct results and the other for erroneous.

Of course, there's nothing stopping you implementing your own type :)

Bob___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Thomas Schilling
It's indeed arbitrary.  Other common names are Inl and Inr (presumably
standing for inject left/right).  Some Haskell project do indeed use
a more specific name.  The advantage of using the generic Left/Right
is reusability of library code.  The particular name of the datatype
and its constructors are competely arbitrary.  The use of Right for
Success is a handy pun -- the program returned the right answer.

HTH,

/ Thomas

On 27 May 2010 15:25, Ionut G. Stan ionut.g.s...@gmail.com wrote:
 Hi,

 I was just wondering if there's any particular reason for which the two
 constructors of the Either data type are named Left and Right. I'm thinking
 that something like Success | Failure or Right | Wrong would have been a
 little better.

 I've recently seen that Scala uses a similar convention for some error
 notifications so I'm starting to believe there's more background behind it
 than just an unfortunate naming.

 Thanks,
 --
 Ionuț G. Stan  |  http://igstan.ro
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe




-- 
Push the envelope.  Watch it bend.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread C. McCann
On Thu, May 27, 2010 at 10:25 AM, Ionut G. Stan ionut.g.s...@gmail.com wrote:
 I was just wondering if there's any particular reason for which the two
 constructors of the Either data type are named Left and Right. I'm thinking
 that something like Success | Failure or Right | Wrong would have been a
 little better.

Because that would confuse matters when using the type for something
other than representing success or failure.

Either is a generic sum type. That is, Either A B only means either
you have an A, or you have a B. Use of Left to represent failure is
merely a matter of convention. Similarly, the generic product type in
Haskell is the 2-tuple--(A, B) only means you have both an A and a
B.

Left and Right work well because they don't carry much extra semantic
baggage, and they make it easy to remember which type parameter goes
with which constructor. Other than the mnemonic value, something even
more bland like This and That would work as well.

Personally, I advocate instead using Sinister and Dexter. Nice and
catchy, don't you think?

- C.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] currying combinators

2010-05-27 Thread Dan Doel
On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote:
 By parametricty, presumably.

Actually, I imagine the way he proved it was to use djinn, which uses a 
complete decision procedure for intuitionistic propositional logic. The proofs 
of theorems for that logic correspond to total functions for the analogous 
type. Since djinn is complete, it will either find a total function with the 
right type, or not, in which case there is no such function.

At that point, all you have left to do is show that djinn is in fact complete. 
For that, you can probably look to the paper it's based on: Contraction-Free 
Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy 
Dyckhoff.

-- Dan

[*] http://www.cs.st-andrews.ac.uk/~rd/publications/jsl57.pdf
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread C. McCann
2010/5/27 Günther Schmidt gue.schm...@web.de:
 I'm exploring the use of church encodings of algebraic data types in
 Haskell.
 Since it's hard to imagine being the first to do so I wonder if folks here
 could point me to some references on the subject.

 I'm looking for examples of church encodings in Haskell a little bit beyond
 Church Booleans and Church Numerals.

The fully general description of Church encoding is rather simple, but
I've rarely seen it described explicitly. Consider the type of Church
encodings for Bool, Either, and the 2-tuple (written here as Pair
for clarity):

churchedBool :: t - t - t
churchedEither :: (a - t) - (b - t) - t
churchedPair :: (a - b - t) - t

And compare the signatures for the constructors of the non-Church encoded types:

True :: Bool
False :: Bool
Left :: a - Either a b
Right :: b - Either a b
Pair :: a - b - Pair a b

We can observe two patterns: 1) The Church encodings take as many
arguments as the type has constructors 2) The type of each argument is
the same as the signature of a constructor, except returning an
arbitrary type. As this suggests, Church decoding is as simple as
applying the Church encoded type to each of the constructors.

From the above, a general description of Church encoding can be
deduced: The encoding of a value is a function that replaces each data
constructor with an arbitrary function. The Church encoding
represents, in a way, the most generalized means of using values of
that type--which is why Haskell already includes variations of Church
encode functions for a few standard types, like so:

encodeEither x = \f g - either f g x
encodeMaybe x = \z f - maybe z f x
encodeTuple x = \f - uncurry f x
encodeBool x = \t e - if x then t else e

But what of Church numerals? First, we must consider the
Church-encoding of recursive data types. Given arbitrary nested data
types, there's nothing else that can be done--the outer types know
nothing of the types they contain. But if an inner type is known to be
the same as the outer type, there are two options for the encoding:
Work only with the outermost value, as with non-recursive types, or
work with the recursive value as a whole, by having the outermost
value pass its arguments inward.

Now, consider the signature of a Church numeral:

churchedNumeral :: (t - t) - t - t

Given the above, what can we say about the equivalent decoded data
type? It takes two arguments, so we have two constructors. The second
argument is a single value, so the associated constructor is nullary.
The first argument must be associated with a unary constructor, but
look at the parameter it takes: the same type as the result! This is
how we can tell that Church numerals are the encoding of a recursive
type. Since the only way a recursive constructor can do anything with
the values it contains is to pass its arguments inward, the value it
has to work with is the result of doing so. Thus, the other
constructor must take a single argument of its own type. What does
this look like as a standard data type?

data Nat = S Nat | Z

Good old inefficient Peano numbers, of course!

Keeping all that in mind, consider a List type, and both ways of encoding it:

data List a = Nil | Cons a (List a)

churchedListOuter :: t - (a - ___ - t) - t
churchedListRecursive :: t - (a - t - t) - t

For the outermost method, what type belongs in place of the ___? The
second argument of Cons is itself a List, so naively we would like to
simply put the type of churchedListOuter itself in place of ___, but
that won't work. In fact, nothing will work here, because recursion on
an outermost encoded list is impossible in a typed λ-calculus
without some means of using general recursion provided as a primitive
operation. Nested tuples can be used, but the length of the list will
be reflected in the type, preventing polymorphism over arbitrary
lists. This is also why Church encoding is most often seen in the
setting of the untyped λ-calculus.

The implicitly recursive encoding, however, presents no such problems.
So, perhaps a function to Church encode lists would be useful? Indeed
it would, and as before, it already exists:

encodeList x = \z f - foldr f z x

Recall the earlier observation that decoding involves applying the
encoded type to its equivalent constructors; the same holds true for
recursive types, as demonstrated by right-folding a list with (:) and
[], or applying a Church numeral to 0 and (+ 1).

Regarding recursive data types as the least fixed point of a
non-recursive data type is thus tied to replacing the outermost
encoding with the recursive encoding, and the Church encode
function for a recursive type is simply a generalized right fold,
partially applied.

Now, the descriptions above are rather informal, and ignore the
possibility of infinite lazy recursive data structures, among other
gaps; but perhaps will help to get you started regardless.

- C.
___
Haskell-Cafe mailing list

Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Alberto G. Corona
Left-Right also good for representing binary trees.

2010/5/27 C. McCann c...@uptoisomorphism.net

 On Thu, May 27, 2010 at 10:25 AM, Ionut G. Stan ionut.g.s...@gmail.com
 wrote:
  I was just wondering if there's any particular reason for which the two
  constructors of the Either data type are named Left and Right. I'm
 thinking
  that something like Success | Failure or Right | Wrong would have been a
  little better.

 Because that would confuse matters when using the type for something
 other than representing success or failure.

 Either is a generic sum type. That is, Either A B only means either
 you have an A, or you have a B. Use of Left to represent failure is
 merely a matter of convention. Similarly, the generic product type in
 Haskell is the 2-tuple--(A, B) only means you have both an A and a
 B.

 Left and Right work well because they don't carry much extra semantic
 baggage, and they make it easy to remember which type parameter goes
 with which constructor. Other than the mnemonic value, something even
 more bland like This and That would work as well.

 Personally, I advocate instead using Sinister and Dexter. Nice and
 catchy, don't you think?

 - C.
 ___
 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] currying combinators

2010-05-27 Thread wren ng thornton

wren ng thornton wrote:

David Sankel wrote:

keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b

Lennart Augustsson  wrote:

There are no interesting (i.e. total) functions of that type.


I wonder how one would prove that to be the case. I tried and didn't 
come up with anything.


By parametricty, presumably.

We must ultimately construct some value of type b, where b is 
universally quantified. Therefore, the only 'constructors' available for 
b are the ((t - b) - u - b) and ((t1 - t) - b) arguments. However, 
since b is universally quantified, these arguments have no way of 
actually constructing some b, other than by returning bottom.


Er, that's not quite right. That's only true if those arguments are 
rank-2 quantified. I'd had a longer (correct) explanation and tried 
shortening it. So here's the better proof:



In order to produce a value of type b, keep must either use one of those 
two arguments or return bottom.


If it uses the ((t - b) - u - b) argument, then keep can only return 
non-bottom if that function [1] ignores its arguments and returns an 
arbitrary b, or [2] uses the (t - b) argument to construct the b. If we 
assume #1 then keep is not total, because we have no way of proving that 
the assumption is valid. So we must expect #2; so in order for keep to 
be total it must be able to construct a total function (t - b). In 
order to construct such a function it must use one of the original two 
arguments, so this is only possible if we can construct a b via ((t1 - 
t) - b).


If it uses the ((t1 - t) - b) argument, then keep can only return 
non-bottom if that function [1] ignores its arguments, or [2] uses the 
(t1 - t) argument. We can't assume #1 and be total, so we must expect 
#2. In order to construct (t1 - t) we must construct a t. But, since t 
is universally quantified, keep knows of no total functions which return 
t. Thus, keep can only construct a function which returns bottom.


Thus, keep can only return non-bottom under the assumption that the ((t 
- b) - u - b) and ((t1 - t) - b) arguments ignore their arguments 
to return a constant b.


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] currying combinators

2010-05-27 Thread wren ng thornton

Dan Doel wrote:

On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote:

By parametricty, presumably.


Actually, I imagine the way he proved it was to use djinn, which uses a 
complete decision procedure for intuitionistic propositional logic. The proofs 
of theorems for that logic correspond to total functions for the analogous 
type. Since djinn is complete, it will either find a total function with the 
right type, or not, in which case there is no such function.


At that point, all you have left to do is show that djinn is in fact complete. 
For that, you can probably look to the paper it's based on: Contraction-Free 
Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy 
Dyckhoff.


Sure, that's another option. But the failure of exhaustive search isn't 
a constructive/intuitionistic technique, so not everyone would accept 
the proof. Djinn is essentially an implementation of reasoning by 
parametricity, IIRC, so it comes down to the same first principles.



(Sorry, just finished writing a philosophy paper on intuitionism :)

--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Re: [Gtk2hs-users] Problem when installing gtk2hs.

2010-05-27 Thread Brandon S. Allbery KF8NH

On May 27, 2010, at 02:46 , Magicloud Magiclouds wrote:

I only have one alex installed under ~/.cabal/bin.
It seems working with shell environment, but not cabal.



But you're doing the Cabal install as root, so it's likely using / 
root/.cabal/bin instead of your home directory.  Or possibly doing a  
global install which would ignore ~/.cabal.  Better would be a global  
install of tools like Alex.


--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com
system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu
electrical and computer engineering, carnegie mellon universityKF8NH




PGP.sig
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] double2Float is faster than (fromRational . toRational)

2010-05-27 Thread Bulat Ziganshin
Hello Daniel,

Friday, May 21, 2010, 11:55:35 PM, you wrote:

 xf = (fromRational $ toRational xd) :: Float
 xf = double2Float xd

 am still surprised how often such kinds of unobvious problems occur
 while programming in Haskell

does it mean that all other languages you are used doesn't have such
problem or that you are an inexperienced programmer? :)


-- 
Best regards,
 Bulatmailto:bulat.zigans...@gmail.com

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Mike Dillon
begin C. McCann quotation:
 Personally, I advocate instead using Sinister and Dexter. Nice and
 catchy, don't you think?

Has anyone done a translation of the Prelude into Latin?

 modulus PraeLudus ubi

 data Uter a b = Sinister a
   | Dexter b
   derivare (Aequo, Ordinaro, Lego, Monstro)

Ha.

-md
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Brandon S. Allbery KF8NH

On May 27, 2010, at 19:07 , Brandon S. Allbery KF8NH wrote:

reordered_cons  :: (t - (t1 - t2)) - t - (t1 - t2)
churchedNumeral :: (t - t ) - t - t

t unifies with (t1 - t2), giving us a Church numeral made up of  
(t1,t2).  (I think.)



Which also explains why that record representation isn't used:  it's  
as inefficient as Peano numbers are.


--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com
system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu
electrical and computer engineering, carnegie mellon universityKF8NH




PGP.sig
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Wire GUI

2010-05-27 Thread Andrew Coppin
I'm looking at a project which involves a GUI where you can insert 
components and wire up connections between them. Obviously the details 
of what the components are and what code gets executed for them is 
domain-specific, however the general idea of graphically wiring things 
together is quite generic. Has anybody already put together a Haskell 
library for doing this kind of thing?


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Claus Reinke
The approach is so simple and trivial that it must have occurred to 
people a hundred times over. Yet I do not find any other examples of 
this. Whenever I google for church encoding the examples don't go beyond 
church numerals.


Am I googling for the wrong keywords?


You might find Typing Record Concatenation for Free
interesting:

   http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.401

Claus

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] currying combinators

2010-05-27 Thread Dan Doel
On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote:
 Sure, that's another option. But the failure of exhaustive search isn't
 a constructive/intuitionistic technique, so not everyone would accept
 the proof. Djinn is essentially an implementation of reasoning by
 parametricity, IIRC, so it comes down to the same first principles.

How, exactly, is it non-constructive to encode the propositional calculus and 
its proofs as, say, types in intuitionistic type theory, write the algorithm 
djinn uses in the same (it was specially crafted to be provably terminating, 
after all), and prove the algorithm complete (again, hopefully in the type 
theory)? I realize this has not all been done, strictly speaking, but I see 
nowhere that it is necessarily non-constructive.

If you point is that the result you get is:

  ¬ ⊢ (...)

instead of 

  ⊢ ¬ (...)

then this is true, but the former is what was originally claimed (there are no 
total functions of that type == that proposition is not a theorem). In fact, 
if one can prove the second, then we're in trouble, because the proposition is 
a classical theorem, and djinn provides a result for

  ⊢ ¬ ¬ (...)

which contradicts the second statement above.

-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Ivan Lazar Miljenovic
Günther Schmidt gue.schm...@web.de writes:

 Hi all,

 I'm exploring the use of church encodings of algebraic data types in
 Haskell.
 Since it's hard to imagine being the first to do so I wonder if folks
 here could point me to some references on the subject.

 I'm looking for examples of church encodings in Haskell a little bit
 beyond Church Booleans and Church Numerals.

It's not quite practical, but have a look at Paul Bailes' Totally
Functional Programming papers:
http://www.itee.uq.edu.au/~paul/tfp-papers/

Also, Types and Programming Languages by Benjamin Pierce (who keeps
reminding me of M*A*S*H, even though his middle name starts with a C...)
has a decent section on church encodings.

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Brandon S. Allbery KF8NH

On May 27, 2010, at 10:53 , Vo Minh Thu wrote:

2010/5/27 Ionut G. Stan ionut.g.s...@gmail.com:


I was just wondering if there's any particular reason for which the  
two
constructors of the Either data type are named Left and Right. I'm  
thinking
that something like Success | Failure or Right | Wrong would have  
been a

little better.

I've recently seen that Scala uses a similar convention for some  
error
notifications so I'm starting to believe there's more background  
behind it

than just an unfortunate naming.


Either *can* be used to represent success and failures, but not
necessarily. It is a convention, when using Either to model
success/failure, to use Right for success and Left for failure. Even
if Left as a word does not match with the meaning of failure, it is
easy to get it Right :)



Historically it *has* been related to negativity in many cultures.   
(Consider sinister, cognate of Italian sinistro/a, and the  
prevalence of and preference for right-handed-ness.)


--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com
system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu
electrical and computer engineering, carnegie mellon universityKF8NH




PGP.sig
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Unicode vs. System.Directory

2010-05-27 Thread Bulat Ziganshin
Hello Andy,

Thursday, May 27, 2010, 5:45:27 PM, you wrote:

does it work both on linux and windows? i'm very interested to run
executables of both kinds and look what features are really supported
(i write file/archive manager and it seems that you have solved many
problems that drive me crazy, such as displaying icons/filetypes,
launching documents...)

 Hi Arie,

 If you don't mind binding code.
 You can try to use GIO APIs from my repository:
 http://patch-tag.com/r/AndyStewart/gio-branch/home

 GIO APIs handle unicode filename every well, and cross-platform.

 Cheers,

   -- Andy

 Arie Peterson ar...@xs4all.nl writes:

 After upgrading to haskell-platform-2010.1.0.0, with the improved unicode
 support for IO in ghc-6.12, I hoped to be able to deal with filenames
 containing non-ascii characters. This still seems problematic, though:

 $ ls
 m?n??
 $ ghci
 GHCi, version 6.12.1: http://www.haskell.org/ghc/  :? for help
 Prelude :m +System.Directory 
 Prelude System.Directory getDirectoryContents . = mapM_ putStrLn
 ..
 mAna?I±
 .

 I hope this passes through the various email systems unharmed; on my
 terminal, the output of 'ls' contains shiny unicode characters, while
 'ghci' garbles up the filename. (My locale is en_GB.utf8.)

 Similar problems arise with functions such as 'copyFile', which refuses to
 handle filenames with non-ascii characters (unless wrapping it with
 encoding functions).


 Is this a known problem? I searched ghc's trac, but there are no relevant
 bugs for the component 'libraries/directory'.


 I have parts of a unicode-aware layer on top of System.Directory laying
 around somewhere. I was rather hoping to ditch it, but I can polish it and
 put it on hackage, if people are interested.


 Kind regards,

 Arie

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


-- 
Best regards,
 Bulatmailto:bulat.zigans...@gmail.com

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma

2010-05-27 Thread David Menendez
On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
carlos.cama...@gmail.com wrote:
 Isaac Dupree:
 Your proposal appears to allow /incoherent/ instance selection.
 This means that an expression can be well-typed in one module, and
 well-typed in another module, but have different semantics in the
 two modules.  For example (drawing from above discussion) :

 module C where

 class F a b where f :: a - b
 class O a where o :: a

 module P where
 import C

 instance F Bool Bool where f = not
 instance O Bool where o = True
 k :: Bool
 k = f o

 module Q where
 import C
 instance F Int Bool where f = even
 instance O Int where o = 0
 k :: Bool
 k = f o

 module Main where
 import P
 import Q
 -- (here, all four instances are in scope)
 main = do { print P.k ; print Q.k }
 -- should result, according to your proposal, in
 -- False
 -- True
 -- , am I correct?

 If qualified importation of k from both P and from Q was specified, we
 would have two *distinct* terms, P.k and Q.k.

I think Isaac's point is that P.k and Q.k have the same definition (f
o). If they don't produce the same value, then referential
transparency is lost.

-- 
Dave Menendez d...@zednenem.com
http://www.eyrie.org/~zednenem/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Brandon S. Allbery KF8NH

On May 27, 2010, at 13:44 , Günther Schmidt wrote:
The approach is so simple and trivial that it must have occurred to  
people a hundred times over. Yet I do not find any other examples of  
this. Whenever I google for church encoding the examples don't go  
beyond church numerals.



Hm.  If I reorder your (.+.) slightly and reparenthesize:

reordered_cons  :: (t - (t1 - t2)) - t - (t1 - t2)
churchedNumeral :: (t - t ) - t - t

t unifies with (t1 - t2), giving us a Church numeral made up of  
(t1,t2).  (I think.)


--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com
system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu
electrical and computer engineering, carnegie mellon universityKF8NH




PGP.sig
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Stephen Tetley
Of interest, (.+.) is the T combinator - called (##) in Peter
Thiemann's Wash and the queer bird in Raymond Smullyan's To Mock a
Mockingbird.

Your technique might well relate to the 'element transforming style'
of Wash, see the Modelling HTML in Haskell paper.

Best wishes

Stephen
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell

2010-05-27 Thread Richard O'Keefe
I think some of us may be missing the point about language  
identification.

It's not a _technical_ question, it's a _legal_ one.
Apple's lawyers have available to them exactly the kind of instrument
they expect (as lawyers) to have:  legal testimony.  If you sign up to  
the

new rules, you are entering into a contract, and whether Apple
_engineers_ can tell what you originally wrong in or not, if Apple's
_lawyers_ are called in, you will find yourself answering:

Q: Well, Mr/Ms/Dr/ Developer, did you personally write
   any of the code in this program?
A: Yes.
Q: And did you write it directly in one of the programming
   languages allowed in the contract, or did you use some
   other programming language?
A: The code that was checked into the repository was in
   C and had never been in any other known programming
   language, but it was actually generated from a table of
   player descriptions using a little AWK script.
Q: So what you are saying is that you knowingly violated
   the terms of the contract?

Given the code generation and refactoring capabilities of things
like NetBeans and Eclipse, notions of written and originally are
getting even fuzzier than they always were, which is saying
something.  If this ever gets to court, we may have a criterion
imposed on us, possibly one as silly as the distinction between
programs and algorithms said to be made in patent-land.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread Lutz Donnerhacke
* Ionut G. Stan wrote:
 I was just wondering if there's any particular reason for which the two
 constructors of the Either data type are named Left and Right.

Yes. The basic function on this type is either.

either a b (Left  x) = Left  (a x)
either a b (Right x) = Right (b x)

So the names of the constuctors are natural.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Why Either = Left | Right instead of something like Result = Success | Failure

2010-05-27 Thread aditya siram
 Monstro
I'm going to call it that from now on. Stay out of the IO Monstro.

-deech

On 5/27/10, Mike Dillon m...@embody.org wrote:
 begin C. McCann quotation:
 Personally, I advocate instead using Sinister and Dexter. Nice and
 catchy, don't you think?

 Has anyone done a translation of the Prelude into Latin?

 modulus PraeLudus ubi

 data Uter a b = Sinister a
   | Dexter b
   derivare (Aequo, Ordinaro, Lego, Monstro)

 Ha.

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


[Haskell-cafe] Multidimensional generalization of the vector package

2010-05-27 Thread Gregory Crosswhite
Hey everyone,

I have been thinking about how to generalize the vector package to multiple 
dimensions, and I'd like to share my ideas with you all in the hope of having 
people smarter than me share their thoughts on how it could be improved --- 
*especially* regarding how to make it efficient!

The standard way to represent a memory layout is to use a stride vector --- 
i.e., a vector which lets you get the (flat) index in memory of a given element 
by dotting the stride vector with the multidimensional index vector.  This has 
the advantage that one can efficiently manipulate it to represent views with 
arbitrary slices, subranges, subranges plus striping (i.e., take every k-th 
element), and transpositions.  Basically the only thing it can't do is 
represent a weird view where we, say, take every index along a particular 
dimension that is a prime number.

Having said this, it might be useful to abstract the memory layout in order to 
preserve generality.  Thus, I was thinking that the layout of the 
multidimensional vector could be represented as a type class with an associated 
type family:

class MemoryLayout layout where
type LayoutIndex layout :: *

indexOf :: layout - (LayoutIndex layout) - Int
firstIndex :: layout - (LayoutIndex layout) - Int
lastIndex :: layout - (LayoutIndex layout) - Int
withinBounds :: layout - (LayoutIndex layout) - Bool

... etc.

It is important that we be able to iterate through the array efficiently.  One 
way that this could be done is through the use of cursors.

class MemoryLayout layout where
...
type LayoutCursor layout :: *
...
getCursorAt :: layout - (LayoutIndex layout) - (LayoutCursor cursor)
getFirstCursor :: layout - (LayoutCursor cursor)
getLastCursor :: layout - (LayoutCursor cursor)
indexOfCursor :: layout - (LayoutCursor cursor) - Int
advanceCursor :: layout - (LayoutCursor cursor) - (LayoutCursor 
cursor)

In general these unfortunately cannot be integers because integers don't 
contain enough information to tell us about where we need to go next inside a 
non-contiguous array.  The alternative is to use a data structure, but then we 
may potentially have lots of potentially wasteful allocations, deallocations, 
and copying going on unless we can somehow cause the cursor to be updated 
destructively.

Fortunately, much of the time our array will be contiguous, so we can have a 
special case fast-path for this case:

class MemoryLayout layout where
...
layoutIsContiguous :: layout - Bool
layoutIsContiguousWhenTraversedInRowMajorOrder :: layout - Bool
layoutIsContiguousWhenTraversedInColumnMajorOrder :: layout - Bool

Then we know that we can just iterate through the array in the order of the 
indices.  It turns out that it is not hard to compute whether a layout is 
contiguous efficiently.  For example, in the code that implements cuts and 
slicing we can actually check to see if the new view is still contiguous and 
simply cache this in the layout.  For restricted cases of layouts (when there 
aren't transpositions) it isn't too hard to just scan through the layout and 
see if it is contiguous.

Another way to iterate through the array is to provide this capability by 
constructing functions that traverse through the array for us and call some 
user-supplied function on each element.  This actually can be a lot more 
efficient (since by using recursive algorithms it can store the information 
that it needs on the stack rather than using heap allocations) but it is much 
more restrictive, and it requires special cases for traversing multiple arrays 
in parallel.

Probably the most general way to sum/fold/etc. over particular dimensions 
(i.e., given a 4D vector, sum over the first and third dimensions leaving the 
second and fourth dimensions) is simply to generalize the notion of cursors, so 
that rather than iterating over elements we are iterating over views of the 
array.

class (MemoryLayout layout1, MemoryLayout layout2) = MemoryLayoutSubviewable 
layout1 layout2 where
type MemoryLayoutViewSetSlicer layout1 layout2 :: *
type MemoryLayoutViewSet layout1 layout2 :: *

getViewSet :: (MemoryLayoutViewSetSlicer layout1 layout2) - layout1 - 
(MemoryLayoutViewSet layout1 layout2)
advanceViewSet :: (MemoryLayoutViewSet layout1 layout2) - 
(MemoryLayoutViewSet layout1 layout2)
currentView :: MemoryLayoutViewSet layout1 layout2 - layout2

This way we can hand getViewSet some slicer that selects some dimensions to 
be reduced but not others and get back a set of views that we can iterate over, 
providing a generalization of the sum and fold functionality provided by repa.

Although these framework allows us to stay general, in practice working with 
shapes that are fixed-length vectors (I personally would prefer the Vec package 
over the hand-rolled one in repa) tends to be 

[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma

2010-05-27 Thread Carlos Camarao
On Thu, May 27, 2010 at 5:43 PM, David Menendez d...@zednenem.com wrote:

 On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
 carlos.cama...@gmail.com wrote:
  Isaac Dupree:
  Your proposal appears to allow /incoherent/ instance selection.
  This means that an expression can be well-typed in one module, and
  well-typed in another module, but have different semantics in the
  two modules.  For example (drawing from above discussion) :
 
  module C where
 
  class F a b where f :: a - b
  class O a where o :: a
 
  module P where
  import C
 
  instance F Bool Bool where f = not
  instance O Bool where o = True
  k :: Bool
  k = f o
 
  module Q where
  import C
  instance F Int Bool where f = even
  instance O Int where o = 0
  k :: Bool
  k = f o
 
  module Main where
  import P
  import Q
  -- (here, all four instances are in scope)
  main = do { print P.k ; print Q.k }
  -- should result, according to your proposal, in
  -- False
  -- True
  -- , am I correct?
 
  If qualified importation of k from both P and from Q was specified, we
  would have two *distinct* terms, P.k and Q.k.

 I think Isaac's point is that P.k and Q.k have the same definition (f
 o). If they don't produce the same value, then referential
 transparency is lost.

 --
 Dave Menendez d...@zednenem.com
 http://www.eyrie.org/~zednenem/ http://www.eyrie.org/%7Ezednenem/


The definitions of P.k and Q.k are textually the same but the contexts are
different. f and o denote distinct values in P and Q. Thus, P.k and Q.k
don't have the same definition.

Thanks for the clarification. I thought the point was about coherence.

Cheers,

Carlos
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Richard O'Keefe


On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote:


Mujtaba Boori wrote:

I think this answer agree100 f g = map f xs == map g xs where
xs = [1..100] from  Richard O'Keefe
is do the job.


agree100 = (==) `on` for [1..100]


Search for on and for in the Haskell 98 Report and you
will not find them.  If you want to tell someone to use them,
you ought to tell them where to find them.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Optimizations and constant unboxed values

2010-05-27 Thread Pierre-Etienne Meunier
Hi Cafe,

Profiling a function that I thought ultra simple revealed that it consumed more 
than half the execution time of my code. After noticing that GHC did not unbox 
all I thought it did, I rewrote it with primitive types, and it did a little 
better, but not much. Then, examining the core (with of course -O3 on) revealed 
things like :

 (GHC.Prim.*##
  (GHC.Prim.-## 1.0 (GHC.Prim.**## 2.0 -53.0))
  (GHC.Prim.**## 2.0 1024.0))

or

 case GHC.Prim.## x_aB9 (GHC.Prim.**## 2.0 -1021.0) of _  {...

Then I wondered if this was really the last stage of GHC's optimizations, as 
constants are not yet propagated. Or maybe GHC does not propagate constants, in 
which case I'd really like to write my 1-2^53 and 2^-1021 once and for all in 
my program. But since unsafeCoerce# does not work between doubles and words ( 
there is a trac ticket about it : 
http://hackage.haskell.org/trac/ghc/ticket/4092 ), I do not even think this is 
possible (and of course, specifying a double in decimal notation with ## is not 
precise enough for this program).

Any clue about how to do it ?

Thanks,
PE

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] currying combinators

2010-05-27 Thread Lennart Augustsson
So what would you consider a proof that there are no total Haskell
functions of that type?
Or, using Curry-Howard, a proof that the corresponding logical formula
is unprovable in intuitionistic logic?
As I understand, in general this can only be proven using meta theory
rather than the logic itself (it could happen that the given formula
implies absurdity, and then we'd know it can't be proven, given that
the logic is consistent).
If Djinn correctly implements the decision procedure that have been
proven to be total (using meta theory), then I would regard Djinn
saying no as a proof that there is no function of that type.

   -- Lennart

On Thu, May 27, 2010 at 7:49 PM, wren ng thornton w...@freegeek.org wrote:
 Dan Doel wrote:

 On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote:

 By parametricty, presumably.

 Actually, I imagine the way he proved it was to use djinn, which uses a
 complete decision procedure for intuitionistic propositional logic. The
 proofs of theorems for that logic correspond to total functions for the
 analogous type. Since djinn is complete, it will either find a total
 function with the right type, or not, in which case there is no such
 function.

 At that point, all you have left to do is show that djinn is in fact
 complete. For that, you can probably look to the paper it's based on:
 Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not
 mistaken) by Roy Dyckhoff.

 Sure, that's another option. But the failure of exhaustive search isn't a
 constructive/intuitionistic technique, so not everyone would accept the
 proof. Djinn is essentially an implementation of reasoning by parametricity,
 IIRC, so it comes down to the same first principles.


 (Sorry, just finished writing a philosophy paper on intuitionism :)

 --
 Live well,
 ~wren
 ___
 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] Chuch encoding of data structures in Haskell

2010-05-27 Thread Dan Doel
On Thursday 27 May 2010 7:15:15 pm Brandon S. Allbery KF8NH wrote:
 On May 27, 2010, at 19:07 , Brandon S. Allbery KF8NH wrote:
  reordered_cons  :: (t - (t1 - t2)) - t - (t1 - t2)
  churchedNumeral :: (t - t ) - t - t
  
  t unifies with (t1 - t2), giving us a Church numeral made up of
  (t1,t2).  (I think.)
 
 Which also explains why that record representation isn't used:  it's
 as inefficient as Peano numbers are.

Church encoding has additional efficiency problems, too. If we look at Peano 
numerals for instance, the Church encoding is:

  forall r. r - (r - r) - r

This means that our only method of computation with them is the structurally 
recursive fold. So, suppose we want to implement a predecessor operation. With 
Haskell-like data, we do:

  pred :: Nat - Nat
  pred Zero= Zero
  pred (Suc n) = n

This operation is expected to be O(1). What if we want to write this using 
only fold? Well, we have to do tricks (this same trick works to define tail 
with foldr):

  pred n = snd $ fold (Zero, Zero) (\ ~(m, _) - (Suc m, m))

So, we've done it, but if you look closely, you'll see that we've actually 
rebuilt the entire 'tail' of the number. So this definition is O(n) (at least, 
if it all gets evaluated). So, Church encodings are less efficient than a 
direct implementation is capable of being.

There is a dual problem with codata. You can encode the extended natural 
numbers as:

  exists s. (s, s - Either () s)

but this only gives you the anamorphism. So, if you want to write the 
successor operation, it's:

  succ n = (Nothing, step)
   where
   step Nothing  = Right (Just n)
   step (Just m) = case observe m of
 Left ()  - Left ()
 Right m' - Right (Just m')

so we end up re-unfolding the entire number.

Taking the paramorphism/apomorphism as a primitive operation fixes this, I 
believe, but you cannot, to my knowledge, encode types that way in, say, 
System F, because it would involve:

  Nat = forall r. r - (Nat - r - r) - r

which is still a recursive equation.

-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell

2010-05-27 Thread Pierre-Etienne Meunier
 If this ever gets to court, we may have a criterion imposed on us,
 possibly one as silly as the distinction between programs and
 algorithms said to be made in patent-land.


I really do agree with your post, but what I dont get is why Apple does not 
intent anything against George Hotz, who publicly acknowledged having 
disassembled his iphone for performing FPGA black magic on it, and would sue 
someone for refusing objects and mallocs in programming.

This makes me wonder if they really have the legal means of doing anything.

Cheers,
PE___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Ivan Miljenovic
On 28 May 2010 09:37, Richard O'Keefe o...@cs.otago.ac.nz wrote:

 On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote:

 agree100 = (==) `on` for [1..100]

 Search for on and for in the Haskell 98 Report and you
 will not find them.  If you want to tell someone to use them,
 you ought to tell them where to find them.

You mean like this?

http://haskell.org/hoogle/?hoogle=on
http://haskell.org/hoogle/?hoogle=for

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Re: Chuch encoding of data structures in Haskell

2010-05-27 Thread Stefan Monnier
 churchedBool :: t - t - t

Important detail: the precise type is ∀t. t → t → t.

 encodeBool x = \t e - if x then t else e

So the type of encodeBool should be:

 Bool → ∀t. t → t → t

whereas Haskell will infer it to be

  ∀t. Bool → t → t → t

which means that a given object can only be eliminated to one type.
I.e. to make such an encoding really usable, you need deep
polymorphism (which GHC supports just fine, but which is not part of
the Haskell standard).


Stefan

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell] Re: [Haskell-cafe] Work on Video Games in Haskell

2010-05-27 Thread John Meacham
On Thu, May 27, 2010 at 08:41:02PM -0400, Pierre-Etienne Meunier wrote:
  If this ever gets to court, we may have a criterion imposed on us,
  possibly one as silly as the distinction between programs and
  algorithms said to be made in patent-land.
 
 I really do agree with your post, but what I dont get is why Apple does not 
 intent anything against George Hotz, who publicly acknowledged having 
 disassembled his iphone for performing FPGA black magic on it, and would sue 
 someone for refusing objects and mallocs in programming.
 
 This makes me wonder if they really have the legal means of doing anything.

Sure, they have the legal means to simply deny your program access to
the App store. They don't need to sue you, you did nothing wrong by
writing a haskell-c compiler and writing a game in it. They just won't
distribute it. They are already under no obligation to distribute your
work or make it available.

John

-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] llvm on windows

2010-05-27 Thread John Lask

on the topic of llvm,

is anybody using llvm binding on windows ? The official llvm windows 
distro does not have a precompiled library which is required for the 
llvm bindings ?


jvl
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Chuch encoding of data structures in Haskell

2010-05-27 Thread C. McCann
On Thu, May 27, 2010 at 9:11 PM, Stefan Monnier
monn...@iro.umontreal.ca wrote:
 I.e. to make such an encoding really usable, you need deep
 polymorphism (which GHC supports just fine, but which is not part of
 the Haskell standard).

Ah, yes, and thank you for pointing that out. My message involved a
great deal of hand-waving that I neglected to clearly identify as
such. The same caveat of course applies to most Church encodings. For
instance, the proper type of a (recursive) encoded list would be:

type ChurchList a = ∀t. t - (a - t - t) - t

...where a is fixed as the type of the list elements. Thus, cons
ought to look something like this charming type:

cons :: ∀a. a - (∀t. t - (a - t - t) - t) - (∀t. t - (a - t - t) - t)

For extra fun, try writing an instance such as:

instance (Show a) = Show (ChurchList a) where [...etc.]

...at which point, perhaps, we remind ourselves that the language is
named Haskell, not Alonzo, and drop the whole matter.

- C.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] gemcutter src?

2010-05-27 Thread Jens Petersen
On 16 May 2010 05:13, Henning Thielemann
schlepp...@henning-thielemann.de wrote:
 http://resources.businessobjects.com/labs/cal/gemcutter-techpaper.pdf

Does anyone have the url to the source code?
(I guess businessobjects was acquired by SAP.)

Jens
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Steven S. Skiena of The Algorithm Design Manual, Second Edition, 2008 has sent me a message that if there is a Haskell page of algorithms he will link to it.

2010-05-27 Thread Casey Hawthorne
Hi:

Steven S. Skiena of The Algorithm Design Manual, Second Edition,
2008 has sent me a message that if there is a Haskell page of
algorithms he will link to it.

So, is there such a page and/or is there some collection(s) of
algorithms and data structures some where that I can massage into the
shape of his book?

:)
 
--
Regards,
Casey
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Chuch encoding of data structures in Haskell

2010-05-27 Thread Jason Dagit
2010/5/27 Günther Schmidt gue.schm...@web.de

 Hello C,

 thank you for explaining.

 The funny thing is that I have never seen anybody take this even a single
 step further than you have in your email.

 In particular I have not found anything where someone might use church
 encoding to solve a quite practical problem, namely for implementing
 extensible records.


I think this article uses Church encoded lists, I could be wrong:
http://okmij.org/ftp/Algorithms.html#zip-folds

Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Richard O'Keefe


On May 28, 2010, at 1:05 PM, Ivan Miljenovic wrote:


On 28 May 2010 09:37, Richard O'Keefe o...@cs.otago.ac.nz wrote:


On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote:


agree100 = (==) `on` for [1..100]


Search for on and for in the Haskell 98 Report and you
will not find them.  If you want to tell someone to use them,
you ought to tell them where to find them.


You mean like this?

http://haskell.org/hoogle/?hoogle=on
http://haskell.org/hoogle/?hoogle=for


Yes, that kind of thing.
Remember, this was a BEGINNER-type question.
If one is giving a *serious* answer, it has to be an answer a
beginner (who has almost certainly never heard of Traversable)
can make sense of, and if it uses functions that are pretty
much certain not to be in said beginner's text book, said
beginner has to be told quite clearly where to find them.


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Ivan Miljenovic
On 28 May 2010 14:52, Richard O'Keefe o...@cs.otago.ac.nz wrote: Yes,
that kind of thing.
 Remember, this was a BEGINNER-type question.
 If one is giving a *serious* answer, it has to be an answer a
 beginner (who has almost certainly never heard of Traversable)
 can make sense of, and if it uses functions that are pretty
 much certain not to be in said beginner's text book, said
 beginner has to be told quite clearly where to find them.

I think this is an example of the Haskell effect (more typically
seen on #haskell), which can be categorised as follows:

1) Someone asks a (usually rather simple) question.

2) People discuss this and provide several straightforward and relevant answers.

3) Out of curiosity (and probably a fair dose of masochism) others
then start to golf the solution into the most interesting approach
possible.

4) The person that asked the question initially gets lost (but is
quite often awed at all the amazing stuff that's going on around them
zooming past at light speed).

5) People suddenly remember that there was an initial question and
make an attempt to explain the more advanced solutions to the person
that asked the question in the first place.

6) They smile and nod and pretend they understand whilst putting a
note onto their copious TODO list to someday sit down and try to work
out wtf was going on.

7) ???

8) Profit!!!

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Casey Hawthorne
This is an effect with any language that offers a very high degree of
abstraction.


I think this is an example of the Haskell effect (more typically
seen on #haskell), which can be categorised as follows:

1) Someone asks a (usually rather simple) question.

2) People discuss this and provide several straightforward and relevant 
answers.

3) Out of curiosity (and probably a fair dose of masochism) others
then start to golf the solution into the most interesting approach
possible.

4) The person that asked the question initially gets lost (but is
quite often awed at all the amazing stuff that's going on around them
zooming past at light speed).

5) People suddenly remember that there was an initial question and
make an attempt to explain the more advanced solutions to the person
that asked the question in the first place.

6) They smile and nod and pretend they understand whilst putting a
note onto their copious TODO list to someday sit down and try to work
out wtf was going on.

7) ???

8) Profit!!!

--
Regards,
Casey
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Chuch encoding of data structures in Haskell

2010-05-27 Thread wren ng thornton

Stefan Monnier wrote:

churchedBool :: t - t - t


Important detail: the precise type is ∀t. t → t → t.


encodeBool x = \t e - if x then t else e


So the type of encodeBool should be:

 Bool → ∀t. t → t → t

whereas Haskell will infer it to be

  ∀t. Bool → t → t → t



Those are the same type.



which means that a given object can only be eliminated to one type.



No, the t is universally quantified just fine. Perhaps you're thinking 
of the need for rank-2 polymorphism in functions which take 
Church-encoded arguments?


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Math questions

2010-05-27 Thread Dan Doel
On Thursday 27 May 2010 9:05:40 pm Ivan Miljenovic wrote:
 On 28 May 2010 09:37, Richard O'Keefe o...@cs.otago.ac.nz wrote:
  On May 27, 2010, at 11:50 PM, Yitzchak Gale wrote:
  agree100 = (==) `on` for [1..100]
  
  Search for on and for in the Haskell 98 Report and you
  will not find them.  If you want to tell someone to use them,
  you ought to tell them where to find them.
 
 You mean like this?
 
 http://haskell.org/hoogle/?hoogle=on
 http://haskell.org/hoogle/?hoogle=for

for from Data.Traversable cannot be what was intended, because it would 
require the functions to have type:

  a - F b

for some Applicative F (which, moreover, should be providing the Eq instance 
you want to check with). This works for the identity functor (assuming the 
instance is declared), but the code is still not right, since the definition 
given doesn't lift the functions.

Rather:

  for = flip map

presumably. But this definition isn't in any of the standard libraries (at 
least visibly) to my knowledge.

-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re[2]: [Haskell-cafe] Re: Unicode vs. System.Directory

2010-05-27 Thread Bulat Ziganshin
Hello Andy,

Friday, May 28, 2010, 1:05:59 AM, you wrote:

 Looks my file-manager:
 http://farm5.static.flickr.com/4027/4584389024_782b1e09ee_o.png

can you please share windows and linux executables and source code?

 I have finish all necessary GIO APIs at
 http://patch-tag.com/r/AndyStewart/gio-branch/home
 I will try to merge those APIs to next release version of gtk2hs when i
 have spare time.

it seems that i can just merge these sources into my program for a
while. but what is the license? believe it or not, but i have
commercial project on the march

-- 
Best regards,
 Bulatmailto:bulat.zigans...@gmail.com

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Re: Chuch encoding of data structures in Haskell

2010-05-27 Thread Ivan Miljenovic
On 28 May 2010 15:18, wren ng thornton w...@freegeek.org wrote:
 Stefan Monnier wrote:

 churchedBool :: t - t - t

 Important detail: the precise type is ∀t. t → t → t.

 encodeBool x = \t e - if x then t else e

 So the type of encodeBool should be:

  Bool → ∀t. t → t → t

 whereas Haskell will infer it to be

  ∀t. Bool → t → t → t


 Those are the same type.

I can see a slight distinction between them, based upon when the
quantification occurs (the former returns a function that work on all
t, the latter will do that encoding for all t).

For most purposes there is no difference, but IIUC the former will let
you do hlist style stuff post-encoding whilst the latter doesn't.

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re[3]: [Haskell-cafe] Re: Unicode vs. System.Directory

2010-05-27 Thread Bulat Ziganshin
Hello Bulat,

Friday, May 28, 2010, 9:24:02 AM, you wrote:

 I have finish all necessary GIO APIs at
 http://patch-tag.com/r/AndyStewart/gio-branch/home

 but what is the license?

heh, i've found COPYING file. but what you mean? if it's just about
one should share all improvements to the library he was made, it's
fine for me. but strictly speaking, LGPL also means you should allow
user to replace himself GIO library with newer versions, it may be
both hard for me and useless for users


-- 
Best regards,
 Bulatmailto:bulat.zigans...@gmail.com

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma

2010-05-27 Thread Isaac Dupree

On 05/27/10 17:42, Carlos Camarao wrote:

On Thu, May 27, 2010 at 5:43 PM, David Menendezd...@zednenem.com  wrote:


On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
carlos.cama...@gmail.com  wrote:

Isaac Dupree:

Your proposal appears to allow /incoherent/ instance selection.
This means that an expression can be well-typed in one module, and
well-typed in another module, but have different semantics in the
two modules.  For example (drawing from above discussion) :

module C where

class F a b where f :: a -  b
class O a where o :: a

module P where
import C

instance F Bool Bool where f = not
instance O Bool where o = True
k :: Bool
k = f o

module Q where
import C
instance F Int Bool where f = even
instance O Int where o = 0
k :: Bool
k = f o

module Main where
import P
import Q
-- (here, all four instances are in scope)
main = do { print P.k ; print Q.k }
-- should result, according to your proposal, in
-- False
-- True
-- , am I correct?


If qualified importation of k from both P and from Q was specified, we
would have two *distinct* terms, P.k and Q.k.


I think Isaac's point is that P.k and Q.k have the same definition (f
o). If they don't produce the same value, then referential
transparency is lost.

--
Dave Menendezd...@zednenem.com
http://www.eyrie.org/~zednenem/http://www.eyrie.org/%7Ezednenem/



The definitions of P.k and Q.k are textually the same but the contexts are
different. f and o denote distinct values in P and Q. Thus, P.k and Q.k
don't have the same definition.


Oh, I guess you are correct: it is like defaulting: it is a similar 
effect where the same expression means different things in two different 
modules as if you had default (Int) in one, and default (Bool) in the 
other.  Except: Defaulting according to the standard only works in 
combination with the 8 (or however many it is) standard classes; and 
defaulting in Haskell is already a bit poorly designed / frowned upon / 
annoying that it's specified per-module when nothing else in the 
language is*.(that's a rather surmountable argument)


It may be worth reading the GHC user's guide which attempts to explain 
the difference between incoherent and non-incoherent instance selection,

http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/type-class-extensions.html#instance-overlap
I didn't read both it and your paper closely enough that I'm sure 
anymore whether GHC devs would think your extension would require or 
imply -XIncoherentInstances ... my intuition was that 
IncoherentInstances would be implied...


*(it's nice when you can substitute any use of a variable, such as P.k, 
with the expression that it is defined as -- i.e. the expression written 
so that it refer to the same identifiers, not a purely textual 
substitution -- but in main above, you can't write [assuming you 
imported C] print (f o) because it will be rejected for ambiguity. 
(Now, there is already an instance-related situation like this where 
Main imports two different modules that define instances that overlap in 
an incompatible way, such as two different instances for Functor (Either 
e) -- not everyone is happy about how GHC handles this, but at least 
those overlaps are totally useless and could perhaps legitimately result 
in a compile error if they're even imported into the same module.))

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] currying combinators

2010-05-27 Thread wren ng thornton

Dan Doel wrote:

On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote:

Sure, that's another option. But the failure of exhaustive search isn't
a constructive/intuitionistic technique, so not everyone would accept
the proof. Djinn is essentially an implementation of reasoning by
parametricity, IIRC, so it comes down to the same first principles.


How, exactly, is it non-constructive to encode the propositional calculus and 
its proofs as, say, types in intuitionistic type theory, write the algorithm 
djinn uses in the same (it was specially crafted to be provably terminating, 
after all), and prove the algorithm complete (again, hopefully in the type 
theory)? I realize this has not all been done, strictly speaking, but I see 
nowhere that it is necessarily non-constructive.



All I'm saying is that a proof of (\forall x. ~ P x) does not constitute 
 a proof of (~ \exist x. P x) for some intuitionists. The issue is one 
of the range of quantification and whether \forall truly exhausts every 
possibility. The BHK interpretation says the two propositions are the 
same, but others say the latter is a stronger claim.


If you believe that Djinn truly does exhaust the search space, then it's 
fine to convert Djinn's proof of (\forall x. ~ P x) into a proof of (~ 
\exist x. P x). However, that just pushes the question back to why you 
feel justified in believing that Djinn truly exhausts the search space. 
I'm not saying you shouldn't believe in Djinn, I'm saying that belief in 
Djinn is not justification for a theorem unless you have justification 
for believing in Djinn.


--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe