-
Von: haskell-cafe-boun...@haskell.org [mailto:haskell-cafe-boun...@haskell.org]
Im Auftrag von Wolfgang Jeltsch
Gesendet: Donnerstag, 19. Februar 2009 14:22
An: haskell-cafe@haskell.org
Betreff: Re: [Haskell-cafe] Haskell.org GSoC
Am Donnerstag, 19. Februar 2009 11:35 schrieb Alberto G. Corona
On Thu, 19 Feb 2009, Sterling Clover wrote:
Thanks for the update on plugins! I look forward to trying them out from the
GHC mainline at some point. I don't think that units as I envision them would
need to mess with the type system directly, but could be implemented simply
as a static
Am Freitag, 20. Februar 2009 09:42 schrieben Sie:
Hello,
but to specify that “this function turns a list into its sorted equivalent”
would probably require to specify e.g. sort in terms of the type system
and to write code that actually does the sorting. The first task is much
like
Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain:
Haskell is a nice, mature and efficient programming language.
By its very nature it could also become a nice executable formal
specification language, provided there is tool support.
Wouldn’t it be better to achieve the goals you describe
2009/2/19 Wolfgang Jeltsch g9ks1...@acme.softbase.org
Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain:
Haskell is a nice, mature and efficient programming language.
By its very nature it could also become a nice executable formal
specification language, provided there is tool
This could look like:
module Integer where
..
theorem read_parses_what_show_shows :
(a :: Integer, Show a, Read a) =
show . read a = id a
proof
axiom
There are several problems with this approach.
For example, I can show:
const 0 (head []) = 0
But if I pretend that I don't
Am Donnerstag, 19. Februar 2009 11:35 schrieb Alberto G. Corona:
2009/2/19 Wolfgang Jeltsch g9ks1...@acme.softbase.org
Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain:
Haskell is a nice, mature and efficient programming language.
By its very nature it could also become a nice
Unfortunately the proofs in dependently typed languages are
extremely long and tedious to write. Some kind of compiler proofing
tool could ease the pain, but I do not think it has low enough
complexity for a GSoC project.
Regards,
John A. De Goes
N-BRAIN, Inc.
The Evolution of
Yes, this is indeed the point. Right now we express properties that a
type class should obey, but there is no compiler assistance to prove
or verify them.
A compiler aware of properties can do additional symbolic
manipulation to increase performance. Surely there has been some
research
Am Donnerstag, 19. Februar 2009 14:50 schrieb John A. De Goes:
Unfortunately the proofs in dependently typed languages are
extremely long and tedious to write. Some kind of compiler proofing
tool could ease the pain, but I do not think it has low enough
complexity for a GSoC project.
I was
Unfortunately the proofs in dependently typed languages are
extremely long and tedious to write. Some kind of compiler proofing
tool could ease the pain, but I do not think it has low enough
complexity for a GSoC project.
I wouldn't say that.
Here's the complete proof script in Coq
Alberto G. Corona wrote:
Wouldn't it be better to achieve the goals you describe with a dependently
typed programming language?
But I wonder how a dependent typed language can express certain properties,
for example, the distributive property between the operation + and * in a
ring or simply
On Feb 18, 2009, at 4:43 AM, Max Bolingbroke wrote:
2009/2/18 Sterling Clover s.clo...@gmail.com:
The punchline: With GHC plugins, it should be possible, and
reasonable, to
add a proper unit system for Haskell.
Alas, GHC plugins cannot change the type system - only meddle with the
Am Dienstag, 17. Februar 2009 21:01 schrieben Sie:
Wolfgang Jeltsch wrote:
* making Applicative a superclass of Monad
* getting rid of MonadPlus (use (Alternative m, Monad m) instead of
(MonadPlus m) or, with another extension, even something like
(forall a. Monoid (m
2009/2/18 Sterling Clover s.clo...@gmail.com:
Something that hit me tonight: Last GSoC gave us GHC compiler plugins. We
have examples, but no documented significant uses, suitable for production
code. Plugins, in essence, as I understand them, let us extend the type
system in useful ways.
On Tue, 17 Feb 2009, Sterling Clover wrote:
Something that hit me tonight: Last GSoC gave us GHC compiler plugins.
Never heard of it. Sometimes I thought it would be nice to modify or
extend GHCs error messages by libraries in order make they feel more like
domain specific languages. E.g.
Le mercredi 11 février 2009 à 11:12 +0100, Daniel Kraft a écrit :
Hi,
Hi,
Do you think something would be
especially nice to have and is currently missing?
In my humble opinion, Haskell presently fall short of its promises
because it does not embed theorem proving. Quickcheck-like testing
Hi,
sylvain wrote:
In my humble opinion, Haskell presently fall short of its promises
because it does not embed theorem proving. Quickcheck-like testing is
truly great, but can not replace proofs to produce bug free software.
With use of equational reasoning + induction, one can already prove
Am Dienstag, 17. Februar 2009 01:13 schrieb Martijn van Steenbergen:
Daniel Kraft wrote:
Do you think something would be especially nice to have and is currently
missing?
Have type class aliases been implemented yet? This proposal (or parts or
it) seems like a very useful compiler
Wolfgang Jeltsch wrote:
* making Applicative a superclass of Monad
* getting rid of MonadPlus (use (Alternative m, Monad m) instead of
(MonadPlus m) or, with another extension, even something like
(forall a. Monoid (m a), Monad m))
* getting rid of ugly Monoid method names
Something that hit me tonight: Last GSoC gave us GHC compiler
plugins. We have examples, but no documented significant uses,
suitable for production code. Plugins, in essence, as I understand
them, let us extend the type system in useful ways. Haskell has
libraries for units[1], but no
Daniel Kraft wrote:
Do you think something would be
especially nice to have and is currently missing?
Have type class aliases been implemented yet? This proposal (or parts or
it) seems like a very useful compiler extension to have, and might be an
interesting GSoC project.
Daniel Kraft wrote:
Hi,
I noticed last year Haskell.org was a mentoring organization for
Google's Summer of Code, and I barely noticed some discussion about it
applying again this year :)
I participated for GCC in 2008 and would like to try again this year;
while I'm still active for GCC
I think the recent discussion about advanced markup for Haddock
documentation could yield a Summer of code project. I still like my
suggestion to use Haskell code as description for math formulas and I like
Wolfgang's idea to use an existing tool like Template Haskell for
conversion from
Am Mittwoch, 11. Februar 2009 18:51 schrieb Don Stewart:
For example, if all the haddocks on hackage.org were a wiki, and
interlinked, every single package author would benefit, as would all
users.
You mean, everyone should be able to mess about with my documentation? This
would be similar to
g9ks157k:
Am Mittwoch, 11. Februar 2009 18:51 schrieb Don Stewart:
For example, if all the haddocks on hackage.org were a wiki, and
interlinked, every single package author would benefit, as would all
users.
You mean, everyone should be able to mess about with my documentation? This
From: haskell-cafe-boun...@haskell.org
[mailto:haskell-cafe-boun...@haskell.org] On Behalf Of Don Stewart
You mean, everyone should be able to mess about with my
documentation? This
would be similar to give everyone commit rights to my
repositories or allow
everyone to edit the
Am Donnerstag, 12. Februar 2009 09:15 schrieben Sie:
g9ks157k:
Am Mittwoch, 11. Februar 2009 18:51 schrieb Don Stewart:
For example, if all the haddocks on hackage.org were a wiki, and
interlinked, every single package author would benefit, as would all
users.
You mean, everyone
Hi,
I noticed last year Haskell.org was a mentoring organization for
Google's Summer of Code, and I barely noticed some discussion about it
applying again this year :)
I participated for GCC in 2008 and would like to try again this year;
while I'm still active for GCC and will surely stay
d:
Hi,
I noticed last year Haskell.org was a mentoring organization for
Google's Summer of Code, and I barely noticed some discussion about it
applying again this year :)
I participated for GCC in 2008 and would like to try again this year;
while I'm still active for GCC and will
30 matches
Mail list logo
