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] Disadvantages of de Bruijn indicies?
Nils, 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. Indeed: it is. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Stefan Holdermans wrote: This is rather typical in the field of program analysis. Getting the analysis precise is impossible and reduces to solving the halting problem. So, the next best thing is to get an approximate answer. An import design guideline to such an analysis is to err on the safe side. That means you'll end up either - with an analysis that tells you that a given function *is guaranteed to* inspect all elements of its argument list or else that the function *may* inspect less elements; or - with an analysis that tells you that a given function *is guaranteed to* not inspect all elements of its argument list or else that the function *may* inspect all elements. Of course, it depends on your needs which of these modalities suits you best. Right. So what you're saying is that for most program properties, you can partition the set of all possible problems into the set for which X is true, the set for which X is false, and a final set for programs where we can't actually determine the truth of X. Is that about right? I find it interesting that one quite hard looking property - this program is well-typed - can always be deduced. Perhaps that's because the language is specifically designed to constrain the set of possible programs in such a way that this is possible? Or perhaps it's just that the set of programs which can't be proved well-typed are simply rejected as if they were provel ill-typed? *shrugs* Can somebody explain to me exactly what the halting problem says? As I understand it, it doesn't say you can't tell if this program halts, it says you cannot write an algorithm which can tell whether *every* program halts or not. (Similar to the way that Galios dude didn't say you can't solve high-order polynomials, he said you can't solve all possible Nth order polynomials *with one formula* [involving only a specific set of mathematical operators]. As in, you *can* solve high-order polynomials - just not with a single formula for all of them. Or not just with the specified operators.) I am not aware of any work on exactly this type of analysis, but you may want to have a look at strictness analysis first; I think there's quite some overlap with what you are trying to achieve. I was actually thinking about having a chain of functions, and wondering whether you can remove the intermediate lists, and/or optimise them into some other data structure. But that would depend on how much of the list is consumed - which, as I suspected, is tricky to determine. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] More mystery with existentials and fundeps
Hi,
{-# OPTIONS_GHC -fglasgow-exts #-}
class F a b | b - a where
data G :: * - * where
GC :: (F a b) = a - G b
foo :: (F a b) = G b - a
foo g = case g of
(GC a) - a
I may be being dumb, but I think this should work. Any value of G
using the GC constructor will be able to define a from G b given F a b
due to the functional dependency.
In the above 'case' statement version I get:
Couldn't match expected type `a' (a rigid variable)
against inferred type `a1' (a rigid variable)
`a' is bound by the type signature for `foo' at Test.lhs:10:11
`a1' is bound by the pattern for `GC' at Test.lhs:12:12-15
In the expression: a
In a case alternative: (GC a) - a
In the expression: case g of (GC a) - a
foo2 :: (F a b) = G b - a
foo2 g = let (GC a) = g in a
And this 'let' statement version explodes with:
My brain just exploded.
I can't handle pattern bindings for existentially-quantified constructors.
In the binding group for
(GC a)
In a pattern binding: (GC a) = g
In the expression: let (GC a) = g in a
In the definition of `foo2': foo2 g = let (GC a) = g in a
So is this a missing feature of GHC or am I (more likely) utterly
mistaken about what should be possible here?
Many thanks,
Matthew
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Andrew, Right. So what you're saying is that for most program properties, you can partition the set of all possible problems into the set for which X is true, the set for which X is false, and a final set for programs where we can't actually determine the truth of X. Is that about right? Yes, you can. (Although, as far as I know, one typically partitions into (a) the set for which is true (respectively false) and (b) the union of the set for which X is false (true) and the set for which we cannot determine X. But, of course, being able to do so implies that you can apply the partitioning that you suggest.) I find it interesting that one quite hard looking property - this program is well-typed - can always be deduced. Perhaps that's because the language is specifically designed to constrain the set of possible programs in such a way that this is possible? Or perhaps it's just that the set of programs which can't be proved well-typed are simply rejected as if they were provel ill-typed? *shrugs* That's exactly it. A prototypical example is the Haskell program (if True then 2 else 'x') + 3 Of course, this is a type-safe program in the sense that it will never actually result in adding a character and a number; but still, for a large class of statically typed languages, such a program will be rejected. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CUFP website
I noticed recently that the website of CUFP conference (Commercial Uses of Function Programming), which used to be at http://www.galois.com/cufp, is not accessible anymore. Does anybody know where it moved? Cyril ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
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. what is sometimes forgotten is that de Bruijn introduced not one, but two numbering schemes. it is interesting that those who actually do the implementations tend to emphasise the importance of both schemes (Berkling was keen on pointing them out, and [1] mentions both on page 2). the better known de Bruijn indices (counting binders from the inside) are useful for local naming in subexpressions, where binders tend to move around, commute, and disappear during reductions. the less known de Bruijn levels (counting binders from the outside) are useful for constant prefixes in contexts, where binders tend to remain stable during reduction of subexpressions. indices are useful for reducing scoping issues to arithmetic, levels are useful for avoiding some of the scoping issues alltogether. if you are implementing transformations without any stable context, indices (or lambda bars) are your friend, if you are implementing transformations within some stable context, you can take references to binders within such context out of the numbers game. McBride and McKinney suggest a nested name scheme for such locally free variables, corresponding to de Bruijn levels; some of Berkling's and Kluge's reduction systems simply ignored such locally free variables during reduction, treating them as constants - if a variable is bound to a binder in the stable context, it will still be bound to the same binder after reductions- and reestablishing the correct presentation during postprocessing, which is straightforward. consider reduction in lambda bodies as an example: \x-(\x-\x-(/x //x)) x - \x-\x-(/x /x) here, we have three binders for 'x', the first of which is part of a stable context (it will not change during reductions), the second disappears during beta-reduction, and the third is currently part of the active subexpression, but will become part of the stable prefix after reduction. in Haskell, such an expression would have been subject to renaming obfuscation already: \x-(\z0-\q32-(z0 x)) x - \x-\q32-(x x) the nice thing about de Bruijn indices or Berkling's lambda bars (protection keys) is that they are a local referencing scheme [*], independent of the context in which the subexpression is placed. but if there is a stable binding context, indices involve unnecessary index computations (here the '0' and '2' refer to the same binder in the stable context, but would be updated again and again during reductions): /\.(/\/\(1 2)) 0 - /\./\(1 1) the nice thing about de Bruijn levels is that references to binders in stable contexts do not involve any computation at all, but for the more common case of binders in the subexpressions being transformed, levels are awkward to use (here, the number used to represent '1' depends not only on the subexpression under reduction, but on the context in which it is situated, so the same subexpression in another context would have a different representation): /\.(/\/\(1 0)) 0 - /\./\(0 0) the common approach is to use indices or lambda bars as the default, and levels as an optimisation for stable contexts (i'll use '[x]' to represent a locally free variable): \x-(\x-\x-(/x //x)) x - -- pre-processing \x-(\x-\x-(/x [x])) [x] - -- reduction/transformation \x-\x-([x] [x]) - -- post-processing \x-\x-(/x /x) as you can see, neither of the '[x]' needs to take part in the index calculations during reduction/transformation - they are taken out of the game during pre-processing, and put back into the common notation during post-processing. that is because the context they refer to remains stable, and as long as we know they refer to it, we can prevent accidental shadowing in the user-level representation through simple post-processing. hth, claus [*] this was essential for Berkling because he was working on a hardware implementation of lambda calculus reductions, based on a system of three or more stacks, where the three main stacks provided a hardware representation of what is nowadays known as a zipper, enabling the hardware reduction machine to navigate through reduction contexts and to perform reductions locally. some of those old works are now online - see, for instance: Reduction languages for reduction machines, KJ Berkling, International Conference on Computer Architecture Year of Publication: 1974 http://portal.acm.org/citation.cfm?id=642112 Computer employing reduction language, Klaus Berkling, 1978 http://www.google.com/patents?hl=enlr=vid=USPAT4075689id=vOwAEBAJoi=fnddq=%22K.+Berkling%22 ___
Re: [Haskell-cafe] Limits of deduction
Andrew Coppin wrote: Right. So what you're saying is that for most program properties, you can partition the set of all possible problems into the set for which X is true, the set for which X is false, and a final set for programs where we can't actually determine the truth of X. Is that about right? If X is true/false is replaced by X can be determined to be true/false, then: yes, roughly. I say roughly because the set of programs where we can't actually determine the truth of X depends on the program analysis algorithm, i.e. is not uniquely determined by X. For instance, you can approximate the halting problem with: Procedure A(n): 1) run program for n steps 2) if it halts, return Halts, I'm sure 3) otherwise, return Don't know Each algorithm A(n) partitions programs into halting and ???. Each A(n) is better than A(n-1), i.e. more halting programs are recognised. Also, for each halting program P, there exists some n such that A(n) recognises P. So, the set of programs where we can't actually determine termination has no meaning unless you specify the actual algorithm. However, for any algorithm A you choose, you will indeed partition programs into the three classes Yes/No/??? you mentioned. Also, a better algorithm than A surely exists (i.e. with a smaller ??? class), so you can keep on improving your program analysis techniques forever. (a.k.a. Eternal Employment Theorem ;-)) I find it interesting that one quite hard looking property - this program is well-typed - can always be deduced. This is not true, in general. The naive polymorphic type system for the lambda calculus is undecidable. For some tricky cases, you might want to look up polymorphic recursion. More practically, in some cases you need type signatures in your Haskell programs, since inference can not provide them (in general). Here's a simple one (involving rank-N): (\(x :: forall a . a-a) - x x) (\x - x) 3 Intuition: ... = (id id) 3 = id 3 = 3 . Also, using only rank-1: polyf :: Int - a - Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) 3 Here passing both 3 and (\z-z) as y confuses the type inference. Perhaps that's because the language is specifically designed to constrain the set of possible programs in such a way that this is possible? Well, I would say the naive polymorphic type system is restricted so to achieve decidability without rejecting too many good programs. (See e.g. Hindley-Milner) (And when designing a type system, decidability is a main concern) Examples as those above are arguably contrived, and rarely show up in actual code. And when it happens, adding a type signature is not too hard. Or perhaps it's just that the set of programs which can't be proved well-typed are simply rejected as if they were provel ill-typed? *shrugs* Yes, this is the case, as for the programs above. Also, one might argue that (if True then 42 else a) is well-typed, and this is hard to check statically. Can somebody explain to me exactly what the halting problem says? As I understand it, it doesn't say you can't tell if this program halts, it says you cannot write an algorithm which can tell whether *every* program halts or not. Your formulation of the halting problem is undecidable seems rather precise to me. Regards, Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy HTML parsing with HXT, HaXML/polyparse, what else?
On Fri, 11 May 2007, Malcolm Wallace wrote: *Text.ParserCombinators.PolyLazy runParser (exactly 4 (satisfy Char.isAlpha)) (abc104++undefined) (*** Exception: Parse.satisfy: failed This output is exactly correct. You asked for the first four characters provided that they were alphabetic, but in fact only the first three were alphabetic. Hence, 'satisfy' failed and threw an exception. If you ask for only the first three characters, then the parse succeeds: The problem is obviously that a later wrong character can make the whole parse fail. Thus successful generated data is not returned until the whole input is parsed and checked. How can I suppress checking the whole input? How can I tell the parser that everything it parsed so far will not be invalidated by further input? How can I rewrite the above example that it returns (abc*** Exception: Parse.satisfy: failed ? I wondered whether 'commit' helps, but it didn't. (I thought it would convert a global 'fail' to a local 'error'.) *Text.ParserCombinators.PolyLazy runParser (exactly 4 (commit (satisfy Char.isAlpha))) (abc104++undefined) *** Exception: Parse.satisfy: failed ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
On 5/14/07, Roberto Zunino [EMAIL PROTECTED] wrote: Also, using only rank-1: polyf :: Int - a - Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) 3 Here passing both 3 and (\z-z) as y confuses the type inference. Actually, I tried this in ghci... Should this work? polyf.hs: polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) 3 NOTE: no type signature Prelude :l polyf [1 of 1] Compiling Main ( polyf.hs, interpreted ) Ok, modules loaded: Main. *Main :t polyf polyf :: forall a t1 t. (Num (t1 - t1), Num a, Num t) = a - (t1 - t1) - t The inference assigns y the type (t1 - t1) even though it is assigned the value 3? Regards, Chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Code layout in Emacs' haskell-mode
I am new to Haskell---and also to languages with the off-side rule--and working my way through Hal Daume's tutorial. I'm a little confused by the support for code layout in Emacs' haskell-mode. Is it buggy, or am I doing something wrong. For example, here's the Hello, world example from the tutorial, with the indentation induced by pounding Tab in haskell-mode. test.hs: module Test where import IO main = do putStrLn Hello, world Prelude :l test [1 of 1] Compiling Test ( test.hs, interpreted ) test.hs:12:0: parse error on input `main' In emacs, every line but the one with where reports Sole indentation. With where, I have the option of having it flush left or indented four spaces; import wants to be two spaces in from where. Moving where doesn't change the error. But if I manually move import flush left (which is the way it's shown in the tutorial, BTW): module Test where import IO main = do putStrLn Hello, world Prelude :l test [1 of 1] Compiling Test ( test.hs, interpreted ) Ok, modules loaded: Test. I have a similar problem with the layout of if-then-else... num.hs: module Num where import IO main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero Prelude :l num [1 of 1] Compiling Num ( num.hs, interpreted ) num.hs:11:2: parse error (possibly incorrect indentation) Again, if I hit tab on the then or else lines, emacs reports Sole indentation. But if I manually change the indentation, it works. module Num where import IO main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero Prelude :l num [1 of 1] Compiling Num ( num.hs, interpreted ) Ok, modules loaded: Num. This is particularly weird because if-then-else doesn't always act this way: exp.hs: module Exp where my_exponent a n = if n == 0 then 1 else a * my_exponent a (n-1) Prelude :l exp [1 of 1] Compiling Exp ( exp.hs, interpreted ) Ok, modules loaded: Exp. I suppose this might have something to do with the do-notation... Does haskell-mode support code layout? Are there conventions I need to know about to make it behave properly? I have haskell-mode version 2.1-1 installed from the Ubuntu feisty repository. Thanks, Chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy HTML parsing with HXT, HaXML/polyparse, what else?
Henning Thielemann [EMAIL PROTECTED] wrote: *Text.ParserCombinators.PolyLazy runParser (exactly 4 (satisfy Char.isAlpha)) (abc104++undefined) (*** Exception: Parse.satisfy: failed How can I rewrite the above example that it returns (abc*** Exception: Parse.satisfy: failed The problem in your example is that the 'exactly' combinator forces parsing of 'n' items before returning any of them. If you roll your own, then you can return partial results: let one = return (:) `apply` satisfy (Char.isAlpha) in runParser (one `apply` (one `apply` (one `apply` (one `apply` return [] (abc104++undefined) (abc*** Exception: Parse.satisfy: failed Equivalently: let one f = ((return (:)) `apply` satisfy (Char.isAlpha)) `apply` f in runParser (one (one (one (one (return []) (abc104++undefined) (abc*** Exception: Parse.satisfy: failed Perhaps I should just rewrite the 'exactly' combinator to have the behaviour you desire? Its current definition is: exactly 0 p = return [] exactly n p = do x - p xs - exactly (n-1) p return (x:xs) and a lazier definition would be: exactly 0 p = return [] exactly n p = return (:) `apply` p `apply` exactly (n-1) p How can I tell the parser that everything it parsed so far will not be invalidated by further input? Essentially, you need to return a constructor as soon as you know that the initial portion of parsed data is correct. Often the only sensible way to do that is to use the 'apply' combinator (as shown in the examples above), returning a constructor _function_ which is lazily applied to the remainder of the parsing task. I wondered whether 'commit' helps, but it didn't. (I thought it would convert a global 'fail' to a local 'error'.) The 'commit' combinator is intended for early abortion of a parse attempt that it is known can no longer succeed. That's the opposite of what you want. By contrast, the 'apply' combinator causes a parse attempt to succeed early, even though it may turn out to fail later. Regards, Malcolm ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: More mystery with existentials and fundeps
On Mon, May 14, 2007 at 12:47:02PM +0100, Matthew Sackman wrote:
{-# OPTIONS_GHC -fglasgow-exts #-}
class F a b | b - a where
data G :: * - * where
GC :: (F a b) = a - G b
foo :: (F a b) = G b - a
foo g = case g of
(GC a) - a
And just to confirm, this is both with ghc 6.6 and with today's HEAD.
Matthew
--
Matthew Sackman
http://www.wellquite.org/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Christopher L Conway wrote: The inference assigns y the type (t1 - t1) even though it is assigned the value 3? Yes, because type classes are open, and maybe you will demonstrate some way to make t1-t1 an instance of Num. Note the Num (t1 - t1) constraint in the type... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy HTML parsing with HXT, HaXML/polyparse, what else?
On Mon, 14 May 2007, Malcolm Wallace wrote: Perhaps I should just rewrite the 'exactly' combinator to have the behaviour you desire? Its current definition is: exactly 0 p = return [] exactly n p = do x - p xs - exactly (n-1) p return (x:xs) Is there a difference between 'exactly' and 'replicateM' ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Roberto Zunino:
Here passing both 3 and (\z-z) as y confuses the type inference.
Christopher L Conway:
polyf :: forall a t1 t.
(Num (t1 - t1), Num a, Num t) =
a - (t1 - t1) - t
The inference assigns y the type (t1 - t1) even though it is assigned
the value 3?
Almost. It assigns y the type (Num (t1 - t1) = t1 - t1). If you're
wondering where the Num context came from, note that the literal 3 is
read as fromInteger 3, which has type (Num a = a). Unifying (t1 -
t1) with (Num a = a) gives (Num (t1 - t1) = t1 - t1).
So the type inference is not really confused at all. It just gives a
not-very-useful type. To demonstrate the perfectly logical behaviour of
the typechecker, we just need a little more absurd code:
{-# OPTIONS_GHC -fglasgow-exts #-}
-- ^ Extensions are needed for relaxed instances only,
-- no rank-n polymorphism here.
instance Show (t - t) where
show _ = function
instance Eq (t - t) where
_ == _ = False
instance Num (t - t) where
_ + _ = id
_ - _ = id
_ * _ = id
abs _ = id
signum _ = id
fromInteger _ = id
Et, voila:
*PolyF :t polyf
polyf :: (Num a, Num t) = a - (t1 - t1) - t
*PolyF polyf 3 3
0
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Christopher L Conway wrote: On 5/14/07, Roberto Zunino [EMAIL PROTECTED] wrote: Also, using only rank-1: polyf :: Int - a - Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) 3 Here passing both 3 and (\z-z) as y confuses the type inference. Actually, I tried this in ghci... Should this work? polyf.hs: polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) 3 NOTE: no type signature I forgot to mention a *use* of that as in test = polyf 1 2 Then:No instance for (Num (t - t)) (see also below) Also, we can avoid type classes and _still_ have inference problems: using (3 :: Int) in polyf yields: Couldn't match expected type `Int' against inferred type `t - t' which is actually the type mismatch error I had in mind. So, even in Haskell - type classes, we need signatures in some cases. Prelude :l polyf [1 of 1] Compiling Main ( polyf.hs, interpreted ) Ok, modules loaded: Main. *Main :t polyf polyf :: forall a t1 t. (Num (t1 - t1), Num a, Num t) = a - (t1 - t1) - t The inference assigns y the type (t1 - t1) even though it is assigned the value 3? Yes, because Haskell natural literals are overloaded: 3 :: forall a. Num a = a So 3 :: (t1 - t1) is fine provided you supply a Num instance for that. Alas, only trivial instances exists (0=1=2=..=id). Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy HTML parsing with HXT, HaXML/polyparse, what else?
On Mon, 14 May 2007, Malcolm Wallace wrote: Essentially, you need to return a constructor as soon as you know that the initial portion of parsed data is correct. Often the only sensible way to do that is to use the 'apply' combinator (as shown in the examples above), returning a constructor _function_ which is lazily applied to the remainder of the parsing task. Great, 'apply' is the solution! I admit that I couldn't derive its power from its documentation which simply states Apply a parsed function to a parsed value. :-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] CUFP
The CUFP website is working again now. http://cufp.galois.com/ Thanks for pointing it out. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Matthew Brecknell wrote: Roberto Zunino: Here passing both 3 and (\z-z) as y confuses the type inference. So the type inference is not really confused at all. It just gives a not-very-useful type. Yes, you are right, I didn't want to involve type classes and assumed 3::Int. A better example would be: polyf :: Int - a - Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) () Here, passing both () and (\z-z) _does_ make inference fail. Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: How to decrease ghc link time
Georg Sauthoff wrote: Simon Marlow [EMAIL PROTECTED] wrote: Hi, Georg Sauthoff wrote: I am a bit unhappy with the link time of the project (i.e. the time ghc needs to link everyting). The project consinst of ~60 Haskell and ~25 foreign files. [..] Make sure everything being linked is on the local file system (or use remote filesystems that can be cached locally). thanks for the advice! Currently I am using NFS ... GHC itself links in 2-3 seconds here on an x86_64/Linux machine, which I think is pretty reasonable. Windows is much slower though. Yes, that sounds ok, currently the project needs 6-7 seconds over NFS (under Solaris) ... If you're using NFS v2, you might want to switch to v3 which has asyncronous writes (IIRC, Sun always stuck to the letter of the NFS spec and did synchronous writes where they were supposed to, whereas Linux has traditionally been a bit more relaxed with the standard). Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lazy HTML parsing with HXT, HaXML/polyparse, what else?
Henning Thielemann [EMAIL PROTECTED] wrote: exactly 0 p = return [] exactly n p = do x - p xs - exactly (n-1) p return (x:xs) Is there a difference between 'exactly' and 'replicateM' ? With this definition, clearly not. But when rewritten to use lazy application, there is certainly a pragmatic difference in where the bottoms (if any) are located in the result. Regards, Malcolm ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Code layout in Emacs' haskell-mode
Hi Christopher, I have also noticed that haskell-mode (and indeed Haskell) can be finicky sometimes. I usually put module [Name] where all on the same line and leave imports on the left margin, so I hadn't experienced the first problem you mentioned. However, I do notice that if I re-arrange your second example so that do and the first putStrLn are on the same line, emacs offers the following indentation: module Num where import IO main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero (that's with all the expressions in the do block lining up vertically, if that doesn't show up in a fixed-width font), it works! I would think that your original indentation gave an error in that GHC would see then and else and assume they were new expressions, but then I would expect that this would have the same problem. If anyone can shed some light on this, that would be nice. Thanks, Nick Meyer [EMAIL PROTECTED] On 5/14/07, Christopher L Conway [EMAIL PROTECTED] wrote: I am new to Haskell---and also to languages with the off-side rule--and working my way through Hal Daume's tutorial. I'm a little confused by the support for code layout in Emacs' haskell-mode. Is it buggy, or am I doing something wrong. For example, here's the Hello, world example from the tutorial, with the indentation induced by pounding Tab in haskell-mode. test.hs: module Test where import IO main = do putStrLn Hello, world Prelude :l test [1 of 1] Compiling Test ( test.hs, interpreted ) test.hs:12:0: parse error on input `main' In emacs, every line but the one with where reports Sole indentation. With where, I have the option of having it flush left or indented four spaces; import wants to be two spaces in from where. Moving where doesn't change the error. But if I manually move import flush left (which is the way it's shown in the tutorial, BTW): module Test where import IO main = do putStrLn Hello, world Prelude :l test [1 of 1] Compiling Test ( test.hs, interpreted ) Ok, modules loaded: Test. I have a similar problem with the layout of if-then-else... num.hs: module Num where import IO main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero Prelude :l num [1 of 1] Compiling Num ( num.hs, interpreted ) num.hs:11:2: parse error (possibly incorrect indentation) Again, if I hit tab on the then or else lines, emacs reports Sole indentation. But if I manually change the indentation, it works. module Num where import IO main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero Prelude :l num [1 of 1] Compiling Num ( num.hs, interpreted ) Ok, modules loaded: Num. This is particularly weird because if-then-else doesn't always act this way: exp.hs: module Exp where my_exponent a n = if n == 0 then 1 else a * my_exponent a (n-1) Prelude :l exp [1 of 1] Compiling Exp ( exp.hs, interpreted ) Ok, modules loaded: Exp. I suppose this might have something to do with the do-notation... Does haskell-mode support code layout? Are there conventions I need to know about to make it behave properly? I have haskell-mode version 2.1-1 installed from the Ubuntu feisty repository. Thanks, Chris ___ 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] Code layout in Emacs' haskell-mode
On 14/05/07, Christopher L Conway [EMAIL PROTECTED] wrote: For example, here's the Hello, world example from the tutorial, with the indentation induced by pounding Tab in haskell-mode. test.hs: module Test where import IO main = do putStrLn Hello, world Prelude :l test [1 of 1] Compiling Test ( test.hs, interpreted ) Are you learning from YAHT, by any chance? That's the only place I've seen the weird convention of placing the 'where' of the 'module X' bit on a separate line. By far the most common convention in normal Haskell is to do as follows: module X where [rest of module] Things should work better if you follow this convention. What you describe still sounds like a bug, though. Again, if I hit tab on the then or else lines, emacs reports Sole indentation. But if I manually change the indentation, it works. This too looks like a bug. As you remark, if statements within do-blocks have different indentation to everywhere else, confusingly. Does haskell-mode support code layout? Are there conventions I need to know about to make it behave properly? I have haskell-mode version 2.1-1 installed from the Ubuntu feisty repository. You should install 2.3 from the haskell-mode page [1]. Isaac Jones, maintainer of the Debian haskell-mode package has been contacted in order to get the latest version in the Debian repository, so it should happen soon, but in the mean time you could download and install the latest version yourself. It features quite a few bugfixes and new features that I imagine are documented on the aforementioned page. haskell-mode's indentation engine is still one thing I'm yet to get my head around, and its being written in Emacs Lisp doesn't help the matter! Still, it's on my todo list. [1]: http://haskell.org/haskell-mode -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Code layout in Emacs' haskell-mode
On 5/14/07, David House [EMAIL PROTECTED] wrote: You should install 2.3 from the haskell-mode page [1]. Isaac Jones, maintainer of the Debian haskell-mode package has been contacted in order to get the latest version in the Debian repository, so it should happen soon, but in the mean time you could download and install the latest version yourself. It features quite a few bugfixes and new features that I imagine are documented on the aforementioned page. I've installed 2.3 and it exhibits the same indentation behavior: any entity appearing on a new line immediately after module X where wants to be indented 4 spaces, including function definitions and variable bindings. if-then-else want to be lined up with one another, although both GHC and Hugs reject this layout. Here's the result of indent-region on the prior example: module Num where import IO main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero This is distressing, because I've gotten rather used to letting Emacs worry about indentation for me. (This works well in tuareg-mode for OCaml. But, as I said earlier, I am a layout-sensitive-language newbie.) Chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Code layout in Emacs' haskell-mode
Nick Meyer wrote: main = do putStrLn Enter a number: inp - getLine let n = read inp if n == 0 then putStrLn Zero else putStrLn NotZero (that's with all the expressions in the do block lining up vertically, if that doesn't show up in a fixed-width font), it works! I would think that your original indentation gave an error in that GHC would see then and else and assume they were new expressions, but then I would expect that this would have the same problem. If anyone can shed some light on this, that would be nice. http://hackage.haskell.org/trac/haskell-prime/wiki/DoAndIfThenElse says already implemented in GHC and Hugs. Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: ANNOUNCE: Harpy -- run-time code generation library
[Relocated to haskell-cafe] Dirk Kleeblatt wrote: apfelmus wrote: Note that even currently, your operations cannot be strict in the address a label refers to because this may be determined later than the first use of the label. In other words, your example code fac = do [...] (1) jmp loopTest [...] (2) loopTest @@ cmp ecx (0 :: Word32) [...] already shows that the function jmp that generates a jmp-instruction may not be strict in the position it jumps to as the address behind loopTest is only known later at line (2). When generating code for (1), the label loopTest is used as an index into a map, to see whether there's a code position associated with it. If it is, the code position is used to compute the jump offset for the jmp instruction, if not (as in this example), a dummy value is placed in the code buffer, and Harpy remembers this position to be patched later on. At (2), the label is defined, and this leads to patching all instructions that have been emitted before this definition. So, yes, the code position is only used after the definition of the label. But the look up in a map-part makes the jmp operation strict in the label parameter. Ah, I slowly get what you mean. In short, the point is that you're reinventing lazy evaluation because you're writing directly to a memory buffer and writing a raw _|_ is impossible. So, you invent a scheme to delay the evaluation of the _|_ until they are defined. With raw writing, we indeed have the strictness writeByte buf _|_ = _|_ which implies jmp _|_ = _|_ I thought that you'd simply store the instructions in a list/monoid like the Builder-Monoid from Data.Binary with the effect that jmp _|_ /= _|_ as monadic action although it stores _|_ as instruction. Lazy evaluation then takes care of filling the _|_-instructions with content in times of need. Here's an illustration with a fictional robodog toy assembly language import Control.Monad.RWS type Address = Int data Dogcode = Bark | Bite | Jump Address data CodeGen a = RWS () [Dogcode] Address a emitDogcode :: Dogcode - CodeGen Address emitDogcode c = x - get tell c put (x+1) return x jump :: Label - CodeGen Address jump = emitDogcode . Jump bark, bite :: CodeGen Address bark = emitDogcode Bark bite = emitDogcode Bite generateDogCode :: CodeGen a - CodeBuffer generateDogCode c = let (_,instructionCount, code) = runRWST c () 0 in ... whatever to do with a list of instructions ... Now, you magically get recursive do-notation without lifting a finger because RWS is already an instance of MonadFix. For example, the following works out of the box pluto :: CodeGen Address pluto = mdo bark jump loop bite loop - bark bark jump loop (The return value of type Address encapsulated in the monad is the line number of the last instruction of pluto.) If you really want to directly write to a memory buffer, I think that you can still use lazy evaluation to fill in the _|_ by emitting a jump PATCHME dummy instruction and build a stack (f.i. of type [Address]) of addresses. The stack takes the role of the map you currently use, I think that a stack is enough. The addresses therein may well be _|_. After having written all instructions into the buffer, all the _|_ are resolved and you can patch the PATCHMEs in a second pass over the buffer. However, because of omnipresent lazy evaluation, it is unclear whether directly writing to a buffer instead of first building a monoid does give a speed/space advantage. So, your current approach may well be slower than a naïve first (difference) list, then raw memory approach. We could omit the map, and just remember where to patch the code, but then we'd need to call explicitly some function after code generation that does the patching. We had implemented this, but found the current solution easier to use, since backpatching is completely automatic and hidden from the user. Huh, I thought that runCodeGen would do an additional backpatch pass as transparently? I also think that having liftIO in the CodeGen-monad is plain wrong. I mean, CodeGen is a monad that generates code without any execution taking place. The execution part is already handled by runCodeGen. Having liftIO means that arbitrary Haskell programs can be intertwined with assembly generation and I doubt that you want that. Feel free to doubt, but this is exactly what we want. :-) Also, note that runCodeGen runs the code _generation_, executing the generated code is done _within_ the CodeGen monad via the functions generated by callDecl (or the predefined functions in the Harpy.Call module). This is even more intertwined, but intentional. Huh? That means that code gets executed during it's own generation? But why do you mix separate concerns? I don't see what use this is besides being an opportunity to mess up. Of course, again a different
[Haskell-cafe] instance monad problem
Hello,
I am trying to learn haskell , but i am struggling with types , its
been around 7 days , it will be very kind if some explain it why this
error , i think this is the only stumbling block . I am looking for
the comparison on why similar code works , while other code not .
I get this error on ghci :
{-
`a' is not applied to enough type arguments
Expected kind `*', but `a' has kind `* - *'
In the type `SS a'
In the type `(Monad a) = {Monad (SS a)}'
In the instance declaration for `Monad (SS a)'
-}
Here is the very small code with comments:
data SS a = SS a Int
data Maybe1 a = Nothing1 | Just1 a
instance Monad Maybe1 where
(Just1 x) = f = f x
--^^ this loads fine in ghci
-- where as this
instance (Monad a)= Monad (SS a) where
(SS x y) = f = f (x y)
--^^ does not work , so whats the difference , both have type parameters
-- something similar works like this :
instance (Eq a)=Eq (SS a) where
(SS x y) == (SS b c) = (y == c) (x == b)
Thanks
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance monad problem
Hi
On 5/14/07, Veer Singh [EMAIL PROTECTED] wrote:
Hello,
I am trying to learn haskell , but i am struggling with types , its
been around 7 days , it will be very kind if some explain it why this
error , i think this is the only stumbling block . I am looking for
the comparison on why similar code works , while other code not .
I get this error on ghci :
{-
`a' is not applied to enough type arguments
Expected kind `*', but `a' has kind `* - *'
In the type `SS a'
In the type `(Monad a) = {Monad (SS a)}'
In the instance declaration for `Monad (SS a)'
-}
Here is the very small code with comments:
data SS a = SS a Int
data Maybe1 a = Nothing1 | Just1 a
instance Monad Maybe1 where
(Just1 x) = f = f x
--^^ this loads fine in ghci
-- where as this
instance (Monad a)= Monad (SS a) where
(SS x y) = f = f (x y)
--^^ does not work , so whats the difference , both have type parameters
-- something similar works like this :
instance (Eq a)=Eq (SS a) where
(SS x y) == (SS b c) = (y == c) (x == b)
The problem is that you've overspecified the monad SS.
Notice that you only had to write
instance Monad Maybe1
not
instance Monad (Maybe1 a)
That's because you declared Maybe1 to only take in one type parameter. SS
also takes in only one type parameter, so you're actually telling it that it
should make SS a b into a monad, but there is no SS a b.
It might help to look at the definition of the State monad in All About
Monads
http://www.haskell.org/all_about_monads/html/
You'll see that state is defined as
newtype State s a =...
and they declare
instance Monad (State s)
not
instance Monad (State s a)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Limits of deduction
Roberto Zunino: Yes, you are right, I didn't want to involve type classes and assumed 3::Int. A better example would be: polyf :: Int - a - Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z-z) else polyf (x-2) () Here, passing both () and (\z-z) _does_ make inference fail. Alternatively, type inference succeeds in rejecting an illegal program [1,2]. :-) So I think we need to be a little more precise about exactly what is undecideable in this example. Yes, the explicit type signature you've given is valid, and the Hindley-Milner type inference algorithm is not able to assign that type without an explicit signature. But that doesn't make Hindley-Milner type inference undecideable. On the contrary, Hindley-Milner type inference is deliberately designed to be decideable. To achieve that, it assumes monomorphic types in certain identifiable contexts, and therefore rejects some functions for which valid types exist. So I think the point you were making is that the problem of inferring the types of all functions for which valid types exist is, in general, undecideable. Hindley-Milner inference ensures decideability by choosing a somewhat less general (but still useful) problem. For what it's worth (not much), it might be possible to invent a decideable type inference which could infer types for a slightly larger set of functions (including polyf), by automatically generalising the types of arguments which are not inspected. Of course, doing so would presuppose the decideability of the subproblem of identifying unused arguments, and achieving that would undoubtedly require certain restrictions on the subproblem definition, analogous to the ones employed by Hindley-Milner. [1] http://haskell.org/onlinereport/decls.html#sect4.1.4 [2] http://haskell.org/onlinereport/decls.html#sect4.5 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] instance monad problem
Veer,
I get this error on ghci :
{-
`a' is not applied to enough type arguments
Expected kind `*', but `a' has kind `* - *'
In the type `SS a'
In the type `(Monad a) = {Monad (SS a)}'
In the instance declaration for `Monad (SS a)'
-}
So, what you are running into is not as much a type error; it's a
kind error. Kinds give structure to types, in the same way as types
give structure to values. For instance,
[Int]
and
[Maybe Int]
are both well-formed types, but
[Maybe]
is not: Maybe still expects a type argument. Now, let's have a look
at kinds.
Int is a well-formed type in its own right; we say that it has kind
*. (* is pronounced as 'type' or sometimes as 'star'). The type of
lists, however, [], is to be applied to a type argument in order to
form a well-formed type: so [] has kind * - *. The same holds for
Maybe: it requires a type argument and so it has kind * - *.
Summarizing:
Int :: *
[]:: * - *
Maybe :: * - *
Now, why is [Maybe] not well-formed? Recall: [] has kind * - *, so
it expects a type argument of kind *. Here, we have supplied as type
argument Maybe, which has kind * - *. (Indeed, [Maybe] is just sugar
for [] Maybe.) So, the kind do not match and we are confronted with a
kind error.
Over to your code snippet.
data SS a = SS a Int
Your type constructor SS expects a single type argument, so we have
SS :: * - *
Instances of the Monad type class are to have kind * - * (for
instance, [], Maybe, IO, ...); so, in terms of kinds, SS is a good
candidate instance of Monad. But then:
instance (Monad a)= Monad (SS a) where
Let's see. SS had kind * - *. This implies that, for SS a to be well-
kinded, the type argument a is to be of kind *. But instances of
Monad are of kind * - * and you writing Monad a in the instance
head, implies that the type variable a had kind * - *. Of course,
the variable a cannot be of both kind * and kind * - *. Hence, GHCi
nicely presents you a kind error.
How to get out of this misery? I'd say, just get rid of the instance
head:
instance Monad SS where
return x = SS x 0
SS x m = f = let ~(SS y n) = f x in SS y (m + n)
or
instance Monad SS where
return x = SS x 1
SS x m = f = let ~(SS y n) = f x in SS y (m * n)
HTH,
Stefan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
