[Haskell] Call for participation: PLPV 2014
You are cordially invited to participate in the Eighth ACM SIGPLAN Workshop on Programming Languages meets Program Verification Date: 21 January 2014 Location: San Diego, in conjunction with POPL 2014 Program: http://www.cse.chalmers.se/~nad/plpv-2014/ Invited talks: - Ranjit Jhala on liquid types for Haskell. - Lee Pike on Programming Languages for High-Assurance Autonomous Vehicles. Contributed talks: - Verified Programs with Binders. Martin Clochard, Claude Marché and Andrei Paskevich. - Formalizing a Correctness Property of a Type-Directed Partial Evaluator. Noriko Hirota and Kenichi Asai. - An Abstract Categorical Semantics for Functional Reactive Programming with Processes. Wolfgang Jeltsch. - Substructural Typestates. Filipe Militao, Jonathan Aldrich and Luis Caires. - The Recursive Polarized Dual Calculus. Aaron Stump. Registration: https://regmaster3.com/2014conf/POPL14/register.php Early registration closes 31 December 2012. Best regards, Nils Anders Danielsson and Bart Jacobs ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] 2nd CFP: PLPV 2014, Programming Languages meets Program Verification
Second call for papers: PLPV 2014 Programming Languages meets Program Verification San Diego, CA, USA Co-located with POPL 2014 http://www.cse.chalmers.se/~nad/plpv-2014/ Overview The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification, by bringing together experts from diverse areas like types, contracts, interactive theorem proving, model checking and program analysis. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic or structural properties of the programming language. One example is provided by dependently typed programming languages, which make it possible to specify and check rich specifications using the languages' type systems. Another example is provided by extended static checking systems, which incorporate contracts with either static or dynamic contract checking. We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage interaction between different communities, we seek a broad scope for PLPV. In particular, submissions may have diverse foundations for verification (based on types, Hoare-logic, abstract interpretation, etc.), target different kinds of programming languages (functional, imperative, object-oriented, etc.), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, resource constraints, etc.). Important dates --- * Submission deadline: 2013-10-09T24:00-12 (midnight at the end of October 9, 2013, UTC-12) * Author notification: November 1, 2013 * Camera-ready papers due: November 17, 2013 * Workshop: January 21, 2014 Submissions --- For details about how to format submissions, where to send them, etc., see http://www.cse.chalmers.se/~nad/plpv-2014/call-for-papers.html. Programme committee --- * Adam Chlipala, MIT * Nils Anders Danielsson, University of Gothenburg (co-chair) * Manuel Fähndrich, Microsoft Research * Philipp Haller, Typesafe * Bart Jacobs, Katholieke Universiteit Leuven (co-chair) * Chantal Keller, Aarhus University * Neelakantan R. Krishnaswami, Max Planck Institute for Software Systems * Andres Löh, Well-Typed LLP * Magnus O. Myreen, University of Cambridge * Alexander J. Summers, ETH Zurich ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: Records in Haskell
On 2012-01-16 19:16, Yitzchak Gale wrote: Allow nested modules. [...] Perhaps Agda's module/record system can provide some inspiration: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Modules http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records (I don't think the wiki pages above are entirely complete/up to date, but for the purposes of this discussion they should do.) -- /NAD ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
On 2011-03-17 19:35, wren ng thornton wrote: Dependently typed languages tend to use the second definition because it gives a pure total function (unlike the first) and because it's less obnoxious to use than the third. In Haskell the third would be even more obnoxious. There is a fourth option: a comparison view. See The view from the left by Conor McBride and James McKinna (Section 6). (This option is similar to what Henning Thielemann suggested.) -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: RFC: migrating to git
On 2011-01-10 16:39, Daniel Peebles wrote: (especially if it lived on github) Even if GitHub is used you should probably arrange some other kind of backup solution, because GitHub reserves the right to delete your repository for any reason at any time (http://help.github.com/terms/). -- /NAD ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] GHC 7.0.1 developer challenges
On 2010-11-25 01:59, John D. Ramsdell wrote: The irony of this situation is deep. CPSA is a program that analyzes cryptographic protocols in an effort to expose security flaws. To ensure that the program does not crash a user's machine, I have to use a linker option that may expose the user to some security problems. Is CPSA intended to be run by untrusted users (for instance with the setuid bit set)? http://hackage.haskell.org/trac/ghc/ticket/3910 http://www.amateurtopologist.com/2010/04/23/security-vulnerability-in-haskell-with-cgi/ -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: dirs in Emacs/Vim in Cabal
On 2010-06-30 18:38, Chris BROWN wrote: My question is: Is it possible to allow the emacs/vim scripts that I have know where this directory is automatically? Maybe you could adapt the approach taken by Agda. Agda's Emacs mode is installed using Cabal plus a small script: 1) The Emacs Lisp sources are installed as data files, using Cabal. 2) A small program called agda-mode is compiled and installed, using Cabal. 3) If the user runs agda-mode setup, then the following code is copied into the user's .emacs (unless it is already there): (load-file (let ((coding-system-for-read 'utf-8)) (shell-command-to-string agda-mode locate))) The .emacs file is found by querying Emacs. 4) The command agda-mode locate prints out the path to a file which sets up the Agda mode (using the Paths_package name module). Note that if a newer version of Agda is installed, then Emacs will (after being restarted) automatically make use of the new version of the Agda mode. The source of agda-mode can be found in Agda's darcs repository: http://code.haskell.org/Agda/src/agda-mode/Main.hs -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Advice on Multiple GHC installations
On 2010-04-12 22:28, Bradford Larsen wrote: 2. If I cannot install multiple ghc versions from a different apt repository, does anyone have advice for how to work with multiple simultaneous installations? A how-to guide or anything like that? I install GHC under /usr/local/stow/ghc-version/ by using the --prefix flag when configuring the binary packages. I have seven versions installed at the moment: $ cd /usr/local/stow/ $ ls -d ghc* ghc-6.10.1 ghc-6.10.2 ghc-6.10.3 ghc-6.10.4 ghc-6.12.1 ghc-6.8.2 ghc-6.8.3 Using stow (http://www.gnu.org/software/stow/) I can then pick one version which is available directly under /usr/local (via symlinks). To use GHC 6.12.1: $ sudo stow ghc-6.12.1 To switch to GHC 6.10.4: $ sudo stow -D ghc-6.12.1 $ sudo stow ghc-6.10.4 If I want to use a non-default version to build something with cabal-install I use the --with-compiler flag: cabal install --with-compiler=/usr/local/stow/ghc-version/bin/ghc package -- /NAD ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Advice on Multiple GHC installations
On 2010-04-13 15:08, Dave Bayer wrote: Why not just use symbolic links? When using stow I am just using symbolic links (and directories), except that I don't need to create them all manually, and I can remove all of them with a single command. I don't need to modify my PATH. I only believe in scattering program parts through /usr/local/[bin,lib,doc] if I believe they will work, will never need upgrading for the life of my OS [...] When using stow you can easily uninstall things: just use stow -D to remove the symbolic links (and directories which only contain such links), and then you can delete the single directory which contains all the files. -- /NAD ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] Hierachical abstraction
On 2010-01-29 01:09, Edward Kmett wrote: Luke pretty much nailed the summary of what you can parse using Applicative means. I tend to consider them codata CFGs, because they can have infinite breadth and depth. However, a 'codata CFG' can handle a much larger class of languages than CFGs. To that end, it is interesting to consider that to maximize the ability to successfully parse such degenerate grammars you are well served to use a traversal that can handle both of those cases. Such a traversal can be built out of Luke's Omega monad or a logic monad with fair conjunction/disjunction and provides a straightforward if inefficient 'top-down' parser. If you restrict the amount of coinduction that you allow, then you can guarantee termination of parsing: http://www.cs.nott.ac.uk/~nad/publications/danielsson-parser-combinators.html -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Hierachical abstraction
On 2010-01-28 20:31, Luke Palmer wrote: I could be mistaken, but at least there are both Applicative and Arrow parser libraries. I don't know how to classify the language that they parse -- it is not strictly context-free. It corresponds roughly to context-free where certain types of infinite chains are allowed. If the token set is finite you don't get any expressive advantage from a monadic parser combinator library (in a lazy setting): you can parse any decidable language using a simple library with an applicative functor interface. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cabal
On 2009-11-09 12:39, Duncan Coutts wrote: You'll be glad to know this is addressed in Cabal-1.8, though not in a fully automatic way. The problem with sharing automatically is knowing when it is safe to do so and when it is not. Each component that shares a source file can use different compiler options, cpp flags, and include dirs (and perhaps other stuff that we cannot easily track). Also, when you link it into a library you actually compile it differently than when you compile it into an executable (the -package-name flag is different). So what we've done is to let executables depend on libraries. That makes the sharing explicit. At some point I also want to add support for private libs which would make this feature useful in more cases. I was hoping that I could make use of this feature now: $ cabal --version cabal-install version 0.7.5 using version 1.8.0.2 of the Cabal library However, when I try to use it I get the following error: cabal: internal error: could not construct a valid install plan. The proposed (invalid) plan contained the following problems: The following packages are involved in a dependency cycle ... The relevant tests in the Cabal source tree also fail for me: PackageTests/BuildDeps/InternalLibrary[123] Is this feature supposed to work now, or has it been postponed? -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsec-like parser combinator that handles left recursion?
On 2009-12-10 07:16, o...@okmij.org wrote: There are at least two parser combinator libraries that can deal with *any* left-recursive grammars. Parser combinators are often used to describe infinite grammars (with a finite number of parametrised non-terminals). The library described by Frost et al. cannot handle all such grammars. For instance, it fails to terminate on p n = memoize n (p (1 + n)). (I don't think they claim that their library can handle such grammars.) Your library seems to handle infinite grammars better, as long as you can find a way to insert the incs correctly. I like the definition of Stream; I read Inc as being coinductive, and Plus as being inductive, and then it is easy to see that run is terminating (assuming that its arguments are well-behaved). However, it seems as if one has to be very careful in the placement of incs. Consider the following grammar: S - A A - S | B B - A | eps The easiest implementation is incorrect: g1 = s where s = inc $ a a = inc $ s + b b = inc $ a + eps run g1 = Nothing The following one, where I have been more careful to only insert incs where absolutely necessary, works: g2 = s where s = a a = inc s + b b = inc a + eps run g2 = Just If I move the incs around it stops working again, though: g3 = s where s = inc a a = s + inc b b = a + eps run g3 = Nothing Have you proved that it is always possible to place the incs correctly? -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Natural Language Processing
On 2009-12-10 01:11, John D. Earle wrote: Is Parsec capable of parsing a mildly context sensitive language? I expect that one can parse any decidable language using Parsec. Whether it is convenient to do so is another question. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsec-like parser combinator that handles left recursion?
On 2009-12-08 16:11, S. Doaitse Swierstra wrote: In principle it is not possible to parse left-recursive grammars [...] I suspect that this statement is based on some hidden assumption. It /is/ possible to parse many left recursive grammars using parser combinators, without rewriting the grammars or representing the cycles in the grammars explicitly. See the following paper draft: Total Parser Combinators http://www.cs.nott.ac.uk/~nad/publications/danielsson-parser-combinators.html -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsec-like parser combinator that handles left recursion?
On 2009-12-09 18:50, Dan Doel wrote: (Your parsers aren't PEGs, are they? If so, I apologize for the redundancy.) No, my parsers use Brzozowski derivatives. See the related work section of the paper I mentioned for some other parser combinator libraries which can handle (some) left recursive grammars. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What *is* a DSL?
On 2009-10-22 14:56, Robert Atkey wrote: Yes, it might have been that, OTOH I'm sure I saw it in some Haskell code. Maybe I was imagining it. There is some related Haskell code in the Agda repository. Do you know of a characterisation of what languages having a possibly infinite amount of nonterminals gives you. Is it all context-sensitive languages or a subset? I found a PhD thesis by Marvin Solomon (Cornell, 1977) which mentions the following, in retrospect obvious, fact: With an infinite set of non-terminals you can represent /any/ (countable) language, by using one non-terminal for every string in the language. I adapted this argument to show that a total parser combinator library which I have implemented in Agda has exactly the same expressive power as (total) functions of type List Bool → List R (assuming the token type is Bool): Parser combinators are as expressive as possible http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=271 -- /NAD This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: What *is* a DSL?
On 2009-10-22 14:44, Robert Atkey wrote:
On Sat, 2009-10-10 at 20:12 +0200, Ben Franksen wrote:
Since 'some' is defined recursively, this creates an infinite production for
numbers that you can neither print nor otherwise analyse in finite time.
Yes, sorry, I should have been more careful there. One has to be careful
to handle EDSLs that have potentially infinite syntax properly.
I find it useful to carefully distinguish between inductive and
coinductive components of the syntax. Consider the following recogniser
combinator language, implemented in Agda, for instance:
data P : Bool → Set where
∅ : P false
ε : P true
tok : Bool → P false
_∣_ : ∀ {n₁ n₂} → P n₁ →P n₂ → P (n₁ ∨ n₂)
_·_ : ∀ {n₁ n₂} → P n₁ → ∞? n₁ (P n₂) → P (n₁ ∧ n₂)
The recognisers are indexed on their nullability; the index is true iff
the recogniser accepts the empty string. The definition of P is
inductive, except that the right argument of the sequencing combinator
(_·_) is allowed to be coinductive when the left argument does not
accept the empty string:
∞? : Set → Bool → Set
∞? true A = A
∞? false A = ∞ A
(You can read ∞ A as a suspended computation of type A.) The limitations
imposed upon coinduction in the definition of P ensure that recognition
is decidable. For more details, see
http://www.cs.nott.ac.uk/~nad/listings/parser-combinators/TotalRecognisers.html.
--
/NAD
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: ANNOUNCE: GHC 6.12.1 Release Candidate 1
On 2009-10-13 08:58, Ian Lynagh wrote: If you're installing one of the Linux bindists then you can use ./configure --prefix=/your/path and again you will have to set up the aliases yourself. And if installing from source you can likewise use ./configure --prefix=/your/path and set up aliases yourself. I install GHC under /usr/local/stow/ghc-version/, and use Stow (http://www.gnu.org/software/stow/) to create symlinks to my preferred version from /usr/local/…. -- /NAD This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] What *is* a DSL?
On 2009-10-07 17:29, Robert Atkey wrote:
A deep embedding of a parsing DSL (really a context-sensitive grammar
DSL) would look something like the following. I think I saw something
like this in the Agda2 code somewhere, but I stumbled across it when I
was trying to work out what free applicative functors were.
The Agda code you saw may have been due to Ulf Norell and me. There is a
note about it on my web page:
http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinators.html
Note that these grammars are strictly less powerful than the ones that
can be expressed using Parsec because we only have a fixed range of
possibilities for each rule, rather than allowing previously parsed
input to determine what the parser will accept in the future.
Previously parsed input /can/ determine what the parser will accept in
the future (as pointed out by Peter Ljunglöf in his licentiate thesis).
Consider the following grammar for the context-sensitive language
{aⁿbⁿcⁿ| n ∈ ℕ}:
data NT a where
Start ::NT () -- Start ∷= aⁿbⁿcⁿ
ABC :: Nat - NT () -- ABC n ∷= aˡbⁿ⁺ˡcⁿ⁺ˡ
X :: Char - Nat - NT () -- X x n ∷= xⁿ
g :: Grammar NT
g Start = nt (ABC 0)
g (ABC n) = char 'a' * nt (ABC (succ n))
| nt (X 'b' n) * nt (X 'c' n)
g (X c n)
| n == 0= pure ()
| otherwise = char c * nt (X c (pred n))
And a general definition for parsing single-digit numbers. This works
for any set of non-terminals, so it is a reusable component that works
for any grammar:
Things become more complicated if the reusable component is defined
using non-terminals which take rules (defined using an arbitrary
non-terminal type) as arguments. Exercise: Define a reusable variant of
the Kleene star, without using grammars of infinite depth.
--
/NAD
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] evaluation semantics of bind
On 2009-02-05 15:20, Gregg Reynolds wrote: I think I've just about got monads figured out, but [...] I don't think anyone has mentioned Simon's Tackling the awkward squad paper in this thread. This tutorial, which contains a semantics for a subset of IO, should answer some of the questions raised. http://research.microsoft.com/en-us/um/people/simonpj/Papers/marktoberdorf/ -- /NAD This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANNOUNCE: haskell-src-exts 0.4.8
On 2009-01-09 00:51, Niklas Broberg wrote: - Support for Unicode symbols for e.g. -. Fixing that would require me to have a Unicode-compliant editor Can't you just use character literals like '\x2192'? -- /NAD This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Using type-level programming to tag functions with time and space complexity
On Thu, 18 Oct 2007, Daniel McAllansmith [EMAIL PROTECTED] wrote: I was wondering if anyone had done work on tagging functions at the type level with their time or space complexity and, if it's even feasible, calculating the complexity of compound functions. Any pointers? I have done some work on this in the context of dependently typed languages. See Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures (http://www.cs.chalmers.se/~nad/publications/danielsson-popl2008.html). The paper also lists some related work which may be useful to you. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] agda v. haskell
On Fri, 28 Sep 2007, Jeff Polakow [EMAIL PROTECTED] wrote: Agda is essentially an implementation of a type checker for Martin-Lof type theory (i.e. dependent types). It is designed to be used as a proof assistant. Well, the language aims to become a practical programming language. Ulf's recently defended PhD thesis has the title Towards a practical programming language based on dependent type theory (http://www.cs.chalmers.se/~ulfn/papers/thesis.html). Lots of work remains to be done before this goal is reached, though. In the meantime, Agda is an excellent vehicle for experiments in dependently typed programming with inductive families (≈ GADTs). For more information, see the Agda wiki (http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php). -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Spot the difference!
On Thu, 20 Sep 2007, PR Stanley [EMAIL PROTECTED] wrote: \_ n - 1 + n \_ - (\n - 1 + n) The outcome seems to be identical. is there a substantive difference between the two definitions? No, since you do not pattern match on the first argument. Otherwise, due to the way these definitions are translated into the core fragment of Haskell in the report, and the presence of seq, the two definitions can have observably different semantics. See Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values, page 4. http://www.cs.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
On Sun, 13 May 2007, Stefan Holdermans [EMAIL PROTECTED] wrote: Anyway, Conor and James' Haskell Workshop paper on manipulating syntax that involves both free and bound variables [1] is really nice and could perhaps be of interest to you. If I remember correctly this paper is not about a pure de Bruijn index representation, but about a mix between names and indices which often goes under the name locally nameless. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] built-in lists vs inductively defined list
On Wed, 09 May 2007, Stefan O'Rear [EMAIL PROTECTED] wrote: To the best of my knowledge, there are no optimizations specific to [] in the compiler proper. However, the standard library has a *lot* of speed hacks you will need to duplicate! Some of which are not expressible in ordinary Haskell (rewrite rules used for short-cut deforestation). -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Article review: Category Theory
On Fri, 19 Jan 2007, Ulf Norell [EMAIL PROTECTED] wrote: Personally I think that the distinction between _|_ and \x - _|_ is a mistake and should be ignored whenever possible. If you want to write an accessible tutorial you should probably use a total programming language, or at least the total fragment of some language, for the programming-related examples. I'd mention the problems with Haskell, restrict the language in some way, and then move on. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Resending: [Haskell-cafe] MissingH: profiler support?
On Thu, 11 Jan 2007, Chris Eidhof [EMAIL PROTECTED] wrote: On 8 Jan, 2007, at 23:13 , Chris Eidhof wrote: I'm trying to profile my application, which makes use of MissingH. But when compiling with -prof -auto-all, I get the following error: Language.hs:8:7: Could not find module `Data.String': Perhaps you haven't installed the profiling libraries for package MissingH-0.18.0? Use -v to see a list of the files searched for. Use Cabal to compile and install the profiling libraries. There is a flag called --enable-profiling, or something like that. If you use GHC you will get two libraries, one without profiling, and one with, but that is a technical detail that Cabal takes care of. Just use the flag, and things should work. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Fractional/negative fixity?
On Wed, 08 Nov 2006, Arie Peterson [EMAIL PROTECTED] wrote: Specifying precedence 'lazily', by a partial order, does not suffer from this problem, because it only requires you to make local decisions. Assuming we only want to be able to make local decisions. Let's say that we want == to bind less tightly than +, as it is now. Let's also say that Eq and Num are defined in two different _unrelated_ modules (this of course implies that Eq is not a superclass of Num). Where and how would we specify the relation between these two operators? -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Fractional/negative fixity?
On Wed, 08 Nov 2006, Henning Thielemann [EMAIL PROTECTED] wrote: If the Prelude would be splitted into modules, where (==) and (+) are separated, and no module imports the other one, then we need a third module, which states the relation between (==) and (+). Yes, presumably. However, currently a fixity declaration for an operator can only be given in the module where the operator is defined. In this hypothetical new system, how would one import/export fixity declarations? Should they be named, or should they be treated like instance declarations are treated today? I've thought about this before, since I like the idea of not totally ordering operator precedences, but I haven't found an elegant and light-weight solution to this problem. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] List comparisons and permutation group code
On Thu, 19 Oct 2006, Tomasz Zielonka [EMAIL PROTECTED] wrote: On Thu, Oct 19, 2006 at 01:37:16PM -0400, Cale Gibbard wrote: In order to determine if [1..length xs] has an element at all, you have to evaluate length xs, which involves forcing the entire spine of xs, because integers can't be partially evaluated. Computing lengths of lists is a great way to introduce strictness. Right, so if Ints were represented as a datatype with Succ and Zero constructors (so integers could be partially evaluated), then the version with length would behave nicely on large and infinite lists :-) Using genericLength for unary, lazy natural numbers can be convenient for other tasks as well, for instance choosing the shorter of two lists in a simple and lazy way. See Modular Lazy Search for Constraint Satisfaction Problems, Nordin and Tolmach, http://web.cecs.pdx.edu/~apt/, around page 25, for another (related) example. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Automatic fixity allocation for symbolic operators
On Mon, 16 Oct 2006, Jón Fairbairn [EMAIL PROTECTED] wrote: I made a more concrete proposal later and Phil Wadler tidied it up. I think It even got as far as a draft of the language, [...] Do you know where this proposal/draft can be found? -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Functional progr., infinity, and the Universe
On Sat, 24 Jun 2006, Paul Hudak [EMAIL PROTECTED] wrote: Hmmm... never tried to write all this down in one place before, but I think this covers all cases: A partial list is one that ends in _|_. A total list is one that ends in []. A finite list is either partial or total. Any other list is infinite. To confuse the picture more I'd like to point out that some use different terminology: * A strictly (spine-) partial list is one that ends in _|_. * A (spine-) total list is one that ends in [] or doesn't end at all. * A finite list is one that ends (with [] or _|_). * An infinite list is one that doesn't end. The two concepts (finite/infinite and total/strictly partial) are orthogonal, and both partition the set of all lists. And of course this generalises to other data types: Finite: x is finite if it is contained in all ω-chains whose lubs are x. Infinite: Not finite. Total: No bottoms. Strictly partial: Not total. Partial: Total or strictly partial. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Re: lhs2TeX-friendly emacs mode?
On Mon, 17 Apr 2006, Conal Elliott [EMAIL PROTECTED] wrote:
Does anyone on this list use mmm-mode for Haskell+LaTeX?
I do. The following code snippet (which should be cleaned up a little)
from my .emacs makes the above combination work fairly well for me:
;;; mmm-mode
(add-to-list 'load-path ~/install/usr/share/emacs/site-lisp/mmm-mode/ t)
(require 'mmm-auto)
; The following expression was stolen from the Haskell Wiki, then
; modified extensively by me.
(mmm-add-classes
'((literate-haskell
:classes (literate-haskell-bird
literate-haskell-laTeX
)
)
(literate-haskell-bird
:submode literate-haskell-mode
:front ^
:include-front t
:back ^[^]\\|\\'
:include-back nil
:insert ((?b insert-literate-haskell-bird-region
nil
@ @ _ @ \n @ \n))
)
(literate-haskell-laTeX
:submode haskell-mode
:front ^begin{code}\n
:include-front nil
:back ^end{code}
:include-back nil
:insert ((?l insert-literate-haskell-laTeX-region
nil
@ \\begin{code}\n @ _ @ \\end{code} @ \n))
)
(literate-haskell-lhs2TeX
:classes (literate-haskell-lhs2TeX-code
literate-haskell-lhs2TeX-bird-code
literate-haskell-lhs2TeX-bird-spec
; The following two modes cause mmm-parse-buffer to go
; into a loop for || and @@.
; literate-haskell-lhs2TeX-verb
; literate-haskell-lhs2TeX-inline
)
)
(literate-haskell-lhs2TeX-code
:submode haskell-mode
:front ^begin{code}\\|^begin{spec}
:front-offset (end-of-line 1)
:back ^end{code}\\|^end{spec}
:back-offset (beginning-of-line -1)
)
(literate-haskell-lhs2TeX-bird-code
:submode literate-haskell-mode
:front ^
:include-front true
:back ^[^]
:back-offset (beginning-of-line -1)
)
; literate-haskell-mode doesn't understand ...
; mmm-mode doesn't handle :back $ :back-offset 0 very well. The
; keyboard bindings of the two modes aren't handled correctly.
(literate-haskell-lhs2TeX-bird-spec
:submode haskell-mode
:front ^
:back ^[^]
:back-offset -1
)
(literate-haskell-lhs2TeX-verb
:submode haskell-mode
:front @
:back @
:back-offset -1
)
(literate-haskell-lhs2TeX-inline
:submode haskell-mode
:front |
:back |
:back-offset -1
)
)
)
(dolist (entry '((flyspell-prog-text-faces region)
(flyspell-generic-check-word-p region)
(haskell-literate region (haskell literate-haskell))
))
(add-to-list 'mmm-save-local-variables entry))
These variables are set by custom-set-variables:
'(mmm-global-mode (quote maybe) nil (mmm-mode))
'(mmm-mode-ext-classes-alist (quote ((latex-mode \\.lhs$
literate-haskell-lhs2TeX) (text-mode \\.lhs$ literate-haskell))) nil
(mmm-mode))
'(mmm-submode-decoration-level 2)
--
/NAD
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: deeqSeq proposal
On Tue, 04 Apr 2006, Andy Gill [EMAIL PROTECTED] wrote: let xs' () = 1 : 2 : xs' () let xs2 = xs' let xs = 1 : 2 : xs So deepSeq xs2 == _|_, but deepSeq xs == xs I appeal to the morally correct reasoning argument .. If the program terminates, then it is still correct. To avoid confusion I'd like to note that this has nothing to do with the kind of moral correctness that I and some others wrote about recently. (I guess that this is the downside of choosing a phrase like that. :) -- /NAD ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: [Haskell-cafe] Distributing monadic(?) functions across dyadic functions
On Sun, 02 Apr 2006, Jared Updike [EMAIL PROTECTED] wrote: Something like distribute fst (==) where distribute f op x y = f x `op` f y A function like this has been suggested for the standard libraries a couple of times before. Someone suggested the name on, which I quite like: (*) `on` f = \x y - f x * f y unionBy (distribute fst (==)) listOfPairs1 listOfPairs2 unionBy ((==) `on` fst) xs ys I think on makes the code rather readable: union by equality on first. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Alternatives to . for composition
On Sat, 25 Mar 2006, Jon Fairbairn [EMAIL PROTECTED] wrote: For emacs, just bind a key (C-. say) to (ucs-insert #X2218). ucs-insert comes from ucs-tables. You can also activate the TeX input method using C-u C-\ TeX RET (if leim is installed). Then you can insert many characters by typing their TeX names. The character ∘ can be inserted by typing \comp, for instance. Of course, this is not very useful unless you already know some TeX. -- /NAD ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: [Haskell-cafe] Re: Positive integers
On Fri, 24 Mar 2006, Henning Thielemann [EMAIL PROTECTED] wrote: Further on think of QuickCheck: A Cardinal type with an Arbitrary instance would save us the (=0) condition and it would reduce the number of tests that must be skipped because of non-fulfilled conditions. Because I was confronted with adding positivity checks to QuickCheck properties quite frequently, I finally wrote wrappers newtype Cardinal = Cardinal Integer deriving (Show, Read, Eq, Ord, Ix) newtype Card = Card Int deriving (Show, Read, Eq, Ord, Ix) in order to simplify such checks. I wouldn't mind having a natural number type, but the technique above is useful anyway. When using QuickCheck you often need custom generators, and the technique removes the need for non-dependent forAlls: prop_foo (Cardinal n) (Balanced t) (Prime p) (Small s) = ... n ... t ... p ... s ... The property above is considerably easier to read than the following one: prop_foo = forAll cardinal $ \c - forAll balanced $ \t - forAll prime $ \p - forAll small $ \s - ... n ... t ... p ... s ... It would be nice to have a bunch of newtypes like these in a library. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] MUA written in Haskell (was: Getting GHC to print Done when it's finished linking?)
On Tue, 07 Mar 2006, Brian Hulley [EMAIL PROTECTED] wrote: (Moved from ghc-users.) Brian Hulley wrote: (time for a proper email client to be written in Haskell! ;-) ) I had the same thought yesterday, after an Emacs-Lisp session in which I was trying to get Gnus to do exactly what I wanted it to... Out of curiosity, how much work would it take to write an easily configurable, decent MUA in Haskell? I don't know too much about MUAs, but I have a feeling that we already have quite a few libraries that are needed for the job: UIs (including HTML rendering...), plugins, various protocols, encryption... -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Credit Card Authorization code
On Thu, 02 Mar 2006, S. Alexander Jacobson [EMAIL PROTECTED] wrote: I am looking for Haskell code that does credit card authorization? e.g. paypal website pro does not supply a Haskell lib. I think that WASH/CGI contains code for doing some sort of checksum check on credit card numbers: http://www.informatik.uni-freiburg.de/~thiemann/haskell/WASH/#washcgi -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] enforcing strictness on arbitrary subexpressions
On Thu, 16 Feb 2006, Udo Stenzel [EMAIL PROTECTED] wrote: hPutStr stdout $ foldr seq veryLongString veryLongString There is no primitive to do this for arbitrary data types, but the DeepSeq type class comes close. You can find DeepSeq and some more hints on strict evaluation at http://users.aber.ac.uk/afc/stricthaskell.html. You can also use Control.Parallel.Strategies: Prelude Control.Parallel.Strategies take 2 (repeat 'x') xx Prelude Control.Parallel.Strategies take 2 (repeat 'x' `using` rnf) (No more output.) -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] module for probability distributions
On Thu, 16 Feb 2006, Matthias Fischmann [EMAIL PROTECTED] wrote: I wrote a module for sampling arbitrary probability distribution, so far including normal (gaussian) and uniform. - There is probably a better implementation out there already. Please point me to it. Martin Erwig and Steve Kollmansberger have written a library for manipulating probability distributions, accompanied by a JFP article. The code seems to have a BSD-style license, but isn't Cabalised. http://web.engr.oregonstate.edu/~erwig/pfp/ -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
M-R: Test performance impact (was: The dreaded M-R)
On Mon, 30 Jan 2006, Simon Marlow [EMAIL PROTECTED] wrote: Given the new evidence that it's actually rather hard to demonstrate any performance loss in the absence of the M-R with GHC, I'm attracted to the option of removing it in favour of a warning. I also want to remove the M-R, because of various reasons that have been mentioned before. However, to stand on more solid ground I suggest that someone runs some performance tests, with and without -fno-monomorphism-restriction, to see whether the M-R has any great impact in practice. There are some performance test suites based on real code out there, right? Nofib? -- /NAD ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
[Haskell-cafe] Enforcing coding policy (was: Why or why not haskell ?)
On Sun, 11 Dec 2005, Tomasz Zielonka [EMAIL PROTECTED] wrote: I would like to see some support in tools for enforcing such a coding policy. It could look like this - a function written using only safe components would be marked as safe. Every unsafe feature like FFI, unsafePerformIO, etc. would taint a module/function, marking it unsafe. You could explicitly tag module/function as trusted/reviewed/etc. There would be different levels of trust. All this would be propagated through the libs and program modules. A Haskell IDE could mark safe/unsafe/trusted code with different background color, etc. You could get statistics about the proportions of safe/unsafe/trusted code. This sounds a lot like what they have been doing in the Programatica project. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Making Haskell more open
On Fri, 11 Nov 2005, Tomasz Zielonka [EMAIL PROTECTED] wrote: [Moved to cafe.] How about an integrated newsgroup+mailinglist+forum. If we had a two-way newsgroup+mailinglist integration, people could use it also as a forum, for example through gmail.google.com. But I don't use fora, so I probably talk nonsense. I think Gmane has everything you're looking for (bidirectional mail-to-news gateway, you can read and post via a web page, and quite a few Haskell mailing lists are already archived there; see http://dir.gmane.org/gmane.comp.lang.haskell.general, for instance). I've hardly used it, though, so I can't tell whether it works well. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Coarbitrary
On Thu, 27 Oct 2005, Shae Matijs Erisson [EMAIL PROTECTED] wrote: Joel Reymont [EMAIL PROTECTED] writes: I could not understand how to define this for arbitraries of my choosing and Shae seems to have defined coarbitrary = error Not implemented :-). Coarbitrary is for generator transformers, see section 3.3 on page 5 of the original paper http://www.md.chalmers.se/~koen/Papers/quick.ps You need coarbitrary for Word32 if you want to generate arbitrary functions of type Word32 - something. As you will see in the QuickCheck paper Coarbitrary instances can (often) be defined mechanically. I think QuickCheck 2 includes default coarbitrary methods implemented using generic classes (http://haskell.org/ghc/docs/latest/html/users_guide/generic-classes.html). -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Quickcheck examples and Data.Word32
On Thu, 27 Oct 2005, Sebastian Sylvan [EMAIL PROTECTED] wrote: instance Arbitrary Word32 where arbitrary = do c - arbitrary :: Gen Integer return (fromIntegral c) This definition will usually only generate very small or very large Word32 values. The reason is the wrapping mentioned elsewhere and the arbitrary definition for Integer: arbitrary = sized $ \n - choose (-fromIntegral n,fromIntegral n) You would need to manually ask for larger sizes (using Test.QuickCheck.check with a suitable Config). If a uniform distribution of Word32s is really needed then I would go with the other definition. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Detecting Cycles in Datastructures
On Thu, 27 Oct 2005, Lennart Augustsson [EMAIL PROTECTED] wrote: Tom Hawkins wrote: Or phased differently, is it possible to make Expr an instance of Eq such that cyclic == cyclic is smart enough to avoid a recursive decent? No. And there is nothing that says that your definition of cyclic will actually have a cycle in the implementation. On the other hand, other people have argued that observable sharing might be nice to have. See the following paper: Observable Sharing for Functional Circuit Description Koen Claessen, David Sands (Some version of it should be available online.) Adding observable sharing to Haskell would imply the loss of full beta equality. If I remember correctly the authors suggest that we only need the restricted form of beta equality where the argument is a defined value (for some notion of definedness). See the paper for their arguments. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parsing in Practice
On Tue, 18 Oct 2005, Philippa Cowderoy [EMAIL PROTECTED] wrote: If you've got a decent chunk of test data or don't mind generating it with QuickCheck odds are you can spot it reasonably quickly when it happens. When I write a parser I usually also write a pretty-printer (or ugly-printer) plus the following property: prop_parsePretty x = parse (pretty x) == x Randomly generating abstract syntax trees using QuickCheck is often straightforward. I can't remember ever having found a bug in code that has passed this kind of test. (But I guess that I haven't written parsers for very complicated languages...) -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Alternatives to hs-plugins?
On Thu, 06 Oct 2005, John Goerzen [EMAIL PROTECTED] wrote: Quick question: am I correct in thinking that this code, while it uses Hugs, won't actually run from Hugs, due to lack of piping support in Hugs? Quite possibly. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Alternatives to hs-plugins?
On Thu, 06 Oct 2005, John Goerzen [EMAIL PROTECTED] wrote: I'm wondering if there are any alternatives? Can a Haskell program using Hugs call Hugs to evaluate an arbitrary hunk of code? Although it is not very efficient you can of course call Hugs and parse its output. I have some working code in http://www.cs.chalmers.se/~nad/repos/diagnostic/Haskell.hs which you can build on if you want to. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Papers from the 2005 Haskell Workshop (Tallinn)?
On Wed, 05 Oct 2005, Dimitry Golubovsky [EMAIL PROTECTED] wrote: The papers presented at the Workshop are already available in the ACM library which requires membership/subscription to read full text PDFs. Are there any plans to make those papers available anywhere else on the Web without subscription? See http://www.acm.org/pubs/copyright_policy/. Particularly the following part: Under the ACM copyright transfer agreement, the original copyright holder retains: [...] * the right to post author-prepared versions of the work covered by ACM copyright in a personal collection on their own Home Page and on a publicly accessible server of their employer. Such posting is limited to noncommercial access and personal use by others, and must include [...] Most authors do put their papers on their web pages nowadays. On a side note, it is a little strange that the research community does the research, writes and typesets the papers, and does most (?) of the arrangements for the conferences, and still someone else gets the copyright. University libraries have to pay lots of money for access to publications. I may have missed some term in the equation, though. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to debug GHC
On Thu, 01 Sep 2005, Frederik Eaton [EMAIL PROTECTED] wrote: But getting a stack backtrace when there is an error should be a pretty basic feature. It's very hard to debug a large program when you can randomly get messages like *** Exception: Prelude.head: empty list and have no idea where they came from. From the GHC FAQ: My program is failing with head [], or an array bounds error, or some other random error, and I have no idea how to find the bug. Can you help? Compile your program with -prof -auto-all (make sure you have the profiling libraries installed), and run it with +RTS -xc -RTS to get a “stack trace” at the point at which the exception was raised. See Section 4.14.4, “RTS options for hackers, debuggers, and over-interested souls” for more details. I tried this out under GHC 6.4/Linux and got a segmentation fault instead of a stack trace. Under GHC 6.2.2 it seemed to work, though. -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Backwards-Compatibility
On Wed, 29 Jun 2005, Sven Moritz Hallberg [EMAIL PROTECTED] wrote: Am 29. Jun 2005 um 11.03 Uhr schrieb Simon Marlow: On 28 June 2005 14:11, Bulat Ziganshin wrote: [...] how about using Pesco's library versioning scheme? (see http://www.haskell.org/tmrwiki/EternalCompatibilityInTheory) I've read that article, and I think it's an interesting idea. I can't disagree with the arguments put forward, but somehow, the cure seems a bit painful. [...] What am I missing? I agree that the benefits of your scheme are desirable. However, in some sense the method amounts to manual version control. We have nice tools that take care of version control, and I wouldn't want to do that by hand. As a simple (but perhaps contrived) example, if a project consists of 50 modules, then after on average 10 changes per module the project will consist of at least 500 modules. If a feature from the first version of some module turned out to be buggy, and all versions needed to be fixed, then ~10 modules might need to be split into two (as per your A_3_9 and A_4_1 example). With a revision control system it should suffice to patch one module, and then users could choose whether to include that patch or not. (Of course, a basic revision control system has other drawbacks compared to your scheme.) -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: ghc -e
On Wed, 24 Nov 2004, Benjamin Franksen wrote: What about putting this thing on the Haskell Wiki? Feel free to do so. I recently noted that some version of GHC (6.3?) ships with a runghc program, so this problem will most likely disappear soon, though. http://cvs.haskell.org/cgi-bin/cvsweb.cgi/~checkout~/fptools/ghc/utils/runghc/runghc.hs /NAD ___ Glasgow-haskell-users mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: ghc -e
On Wed, 17 Nov 2004, Benjamin Franksen wrote: I want to use ghc as a script interpreter, using the '-e' option. The problem is that I can't give the script any command line arguments, because 'ghc -e' intepretes everything argument as the name of a module to compile. I once wrote a script which circumvented the issue above by using System.Environment.withArgs. It works, but it is of course a little clunky. See the attached sources. /NADmodule Main where import IO import System.Environment import System.Posix.Process ghc = ... -- Path to GHC. stripFirstLine = ... -- Path to the program below. -- #!/bin/sh -- grep -v '^#!' $2 $3 main = do args - getArgs if length args 1 then hPutStr stderr usage else do let file:progArgs = args cmd = System.Environment.withProgName ++ show file ++ $ System.Environment.withArgs ++ show progArgs ++ Main.main ghcArgs = [-F, -pgmF, stripFirstLine, -e, cmd, file] executeFile ghc False ghcArgs Nothing usage = Usage: runghc Haskell source file [Extra arguments to the program...]\n ___ Glasgow-haskell-users mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: getUserEntryForName weirdness
On Fri, 29 Oct 2004, Peter Simons wrote: Is anyone else seeing this on his system? getUserEntryForName [] = print . userName wasabi On Solaris I get the following results (GHC 6.2.2, GHC 6.2.1 exits with Illegal Instruction): Prelude System.Posix.User getUserEntryForName undefined user = print . userName Prelude System.Posix.User getUserEntryForName = print . userName \208\ACK Prelude System.Posix.User getUserEntryForName foo = print . userName \208\ACK Prelude System.Posix.User getUserEntryForName foo = print . userName Segmentation Fault /NAD ___ Glasgow-haskell-users mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] -allow-extension-for-bottom
On Mon, 11 Oct 2004, Serge D. Mechveliani wrote: Consider the compilation flag -allow-extension-for-bottom which changes the language meaning so that allows to ignore the bottom value. For example, the programs (1) (\ x - (if p x then foo (g x) else foo (h x)) ) and (2) (\ x - foo ((if p x then g x else h x)) ) become equivalent, and many program transformations become possible. You may be interested in knowing that, under some circumstances, the feature you are looking for is actually implemented, and you don't need any flag to activate it. Try this function under GHC 6.2.1, for example: f = \x - if x then (\y - 0) else (\y - 1) *Main ChasingBottoms isBottom (f bottom) False (Using your notation p = g = h = id, foo = const.) I prefer to call this a bug, though. See http://www.haskell.org/pipermail/glasgow-haskell-bugs/2003-November/003735.html and possibly http://www.cs.chalmers.se/~nad/software/ChasingBottoms/docs/index.html for more details. I should add that I think that the Haskell semantics makes proofs of correctness overly complicated. A conservative approximation should suffice in most cases. Hence there could also be a compiler setting which took advantage of such approximations. /NAD ___ Glasgow-haskell-users mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] -allow-extension-for-bottom
On Mon, 11 Oct 2004, Serge D. Mechveliani wrote: Consider the compilation flag -allow-extension-for-bottom which changes the language meaning so that allows to ignore the bottom value. For example, the programs (1) (\ x - (if p x then foo (g x) else foo (h x)) ) and (2) (\ x - foo ((if p x then g x else h x)) ) become equivalent, and many program transformations become possible. You may be interested in knowing that, under some circumstances, the feature you are looking for is actually implemented, and you don't need any flag to activate it. Try this function under GHC 6.2.1, for example: f = \x - if x then (\y - 0) else (\y - 1) *Main ChasingBottoms isBottom (f bottom) False (Using your notation p = g = h = id, foo = const.) I prefer to call this a bug, though. See http://www.haskell.org/pipermail/glasgow-haskell-bugs/2003-November/003735.html and possibly http://www.cs.chalmers.se/~nad/software/ChasingBottoms/docs/index.html for more details. I should add that I think that the Haskell semantics makes proofs of correctness overly complicated. A conservative approximation should suffice in most cases. Hence there could also be a compiler setting which took advantage of such approximations. /NAD ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
[Haskell] ANNOUNCE: Chasing Bottoms
Excerpt from the documentation at http://www.cs.chalmers.se/~nad/software/ChasingBottoms/docs/: Chasing Bottoms === Do you ever feel the need to test code involving bottoms (e.g. calls to the error function), or code involving infinite values? Then this library could be useful for you. It is usually easy to get a grip on bottoms by showing a value and waiting to see how much gets printed before the first exception is encountered. However, that quickly gets tiresome and is hard to automate using e.g. QuickCheck (http://www.cs.chalmers.se/~rjmh/QuickCheck/). With this library you can do the tests as simply as the following examples show. Testing explicitly for bottoms: isBottom (head []) True isBottom bottom True isBottom (\_ - bottom) False isBottom (bottom, bottom) False Comparing finite, partial values: ((bottom, 3) :: (Bool, Int)) ==! (bottom, 2+5-4) True ((bottom, bottom) :: (Bool, Int)) ! (bottom, 8) True Showing partial and infinite values (\/! is join and /\! is meet): approxShow 4 $ (True, bottom) \/! (bottom, b) Just (True, b) approxShow 4 $ (True, bottom) /\! (bottom, b) (_|_, _|_) approxShow 4 $ ([1..] :: [Int]) [1, 2, 3, _ approxShow 4 $ (cycle [bottom] :: [Bool]) [_|_, _|_, _|_, _ Approximately comparing infinite, partial values: approx 100 [2,4..] ==! approx 100 (filter even [1..] :: [Int]) True approx 100 [2,4..] /=! approx 100 (filter even [bottom..] :: [Int]) True The code above relies on the fact that bottom, just as error ..., undefined and pattern match failures, yield exceptions. Sometimes we are dealing with properly non-terminating computations, such as the following example, and then it can be nice to be able to apply a timeout. let primes = unfoldr (\(x:xs) - Just (x, filter ((/= 0) . (`mod` x)) xs)) [2..] timeOutMicro 100 (print $ filter ((== 1) . (`mod` 32)) primes) = print [97,193,257Nothing timeOutMicro 100 (print $ take 5 $ filter ((== 1) . (`mod` 32)) primes) = print [97,193,257,353Nothing timeOutMicro 100 (print $ take 5 $ filter ((== 1) . (`mod` 32)) primes) = print [97,193,257,353,449] Just () All the type annotations above are required. For the underlying theory and a larger example involving use of QuickCheck, see the article Chasing Bottoms, A Case Study in Program Verification in the Presence of Partial and Infinite Values (http://www.cs.chalmers.se/~nad/publications/danielsson-jansson-mpc2004.html). Source code: http://www.cs.chalmers.se/~nad/software/ChasingBottoms/chasing-bottoms.tar.gz. /NAD ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Strictness problem
The following program should, if I'm not completely mistaken, output something involving Correct: module Main where f x = case x of [EMAIL PROTECTED] - \y - x y [EMAIL PROTECTED] - \y - x y main = putStrLn $ f (error Correct) `seq` Error However, whether it does so is a complicated function of the GHC version and optimisation settings: GHC version -O2? Correct? --- 4.08.1 NoYes 4.08.1 Yes No 5.04.2 NoNo 5.04.2 Yes Yes 6.0.1_ No Recent CVS NoNo Recent CVS Yes Yes (Hugs Yes) All tests were run on a Solaris system, except for the CVS one (which I don't have access to, so I don't know the exact date of checkout). Different fs give different behaviour, at least for 6.0.1. Try e.g. f x = case x of True - id False - id with and without -O2. /NAD ___ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
forkProcess + stdin issue
After using forkProcess the child cannot read from stdin (except for data already in the buffer). Using forkProcessAll or foreign importing C's fork makes the problem go away. This applies to Solaris and GHC 6.0, I have not tested other platforms. Example program: module Main where import Monad import IO import System.Posix main = do mPid - forkProcess case mPid of Nothing - -- Child. forwardStdin Just pid - do -- Parent. getProcessStatus True False pid return () forwardStdin = do eof - isEOF when (not eof) $ do c - getChar putChar c forwardStdin Test output: $ echo apa | ./Test apa $ ./Test asdfasdf ^CTest: interrupted $ /NAD ___ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Microseconds in hWaitForInput
From libraries/base/cbits/inputReady.c: tv.tv_sec = msecs / 1000; tv.tv_usec = msecs % 1000; This should be (msecs % 1000) * 1000, right? usec stands for microseconds. See http://www.haskell.org/onlinereport/io.html#sect21.9.1. /NAD ___ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: Arbitrary precision reals?
On Tue, 25 Mar 2003, Tom Pledger wrote: I don't know whether arbitrary precision reals have been done in Haskell, but here's one of the issues... There is a Haskell implementation of exact real arithmetic using Linear Fractional Transformations, see http://www.doc.ic.ac.uk/~ae/exact-computation/ for implementations and a bunch of papers. (The web server does not seem to respond right now, but the pages are cached by Google.) /NAD ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
