Re: [Haskell-cafe] Limits of deduction
Andrew, Jules wrote: It's computationally impossible, in general. I can write something silly like f (x:xs) = x : (UniversalTuringMachine(x) `seq` xs) and it reduces to the halting problem. However, it might be tractable for a large class of sensible programs. Someone around here might be aware of some relevant research? 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. 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. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
Neil, de Bruijn indicies look quite nice, and seem to eliminate a lot of complexity when dealing with free variables: http://en.wikipedia.org/wiki/De_Bruijn_index So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core? I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start. De Bruijn indices are used within Epigram, or at least they used to be. Maybe the Epigram people can inform you about their experiences. 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. Cheers, Stefan [1] Conor McBride and James McKinna. Functional pearl: I am not a number—I am a free variable. In Proceedings of the 2004 ACM SIGPLAN Haskell Workshop, Snowbird, Utah, USA, September 22, 2004, pages 1–-9. ACM Press, 2004. http://portal.acm.org/citation.cfm?id=1017472.1017477___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
Apfelmus, Types like () or Int do not have a logical counterpart in propositional logic, although they can be viewed as a constant denoting truth. In other words, they may be thought of as being short-hand for the type expression (a,a) (where a is a fresh variable). Could you explain this? I can see () corresponding to True; but you're not suggesting that True = (a, a), are you? System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?). Not propositional of course, but second-order indeed. Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
Apfelmus, System F is closest to Haskell and corresponds to a second order intuitionistic propositional logic (?). Not propositional of course, but second-order indeed. Not sure, what I meant there :-S. Please ignore it. You're right of course: second-order intuitionistic propositional logic it is :-). (Sorry for adding confusion.) Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Higher order types via the Curry-Howard correspondence
Stefan Holdermans wrote: Apfelmus, Types like () or Int do not have a logical counterpart in propositional logic, although they can be viewed as a constant denoting truth. In other words, they may be thought of as being short-hand for the type expression (a,a) (where a is a fresh variable). Could you explain this? I can see () corresponding to True; but you're not suggesting that True = (a, a), are you? Oh, what a mistake .. . Of course, a /\ a = a /= True. But there are real tautologies like (a - a) that can be used instead. I just wanted to avoid introducing a primitive constant ⊤ denoting truth when it already can be expressed in the logic. From now on, let's say ⊤ := (a-a). What I wanted to say is that the Curry-Howards correspondence of first order propositional logic does not assign a meaning to types like () or Int that are not built from type variables and the logical connectives. But I think it can be adapted to assign them the proposition ⊤. The translation of lambda-terms to proofs would then replace every primitive constant like 1 or 2 or () with the proof (id :: ⊤) and eradicate pattern matches and conditionals. From a computational point of view, this correspondence is not very interesting then. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ambiguous type variables at MPTC
If f2 is legal, why if f3 illegal? For some usage site of f3, the constraint C String b might allow b to be resolved given whatever instances of C are in effect. Is there a motivation for these behaviors? Are these sorts of cases discussed in the CHR/FD paper that motivated the coverage condition (which I have yet to read)? It should be possible to resolve the constraints from the types in the signature. That rules out f1 and f3. For f2, given a type for a, say Int, not just any odd instance for b will do, say instance C Int Bool GHC says: No instance for (C Int b) arising from use of `f2' at Q.hs:30:6-9 Possible fix: add an instance declaration for (C Int b) In the expression: f2 x In the definition of `f': f x = f2 x No, it has to be an instance for all possible types b: instance C Int b So, you can only call f2 with types a for which the instance C a b is completely independent of b. There is no ambiguity. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Disadvantages of de Bruijn indicies?
Hi Thanks for all the responses, I'm busy reading through them. I'm still trying to decide whether I should use them or not. They complicate things, are less intuitive than names. But on the other hand, the language I'm working in is untyped and has only letrec. These things make binding errors easier to occur, and harder to detect. Thanks for the helpful throughts, Neil On 5/13/07, Stefan Holdermans [EMAIL PROTECTED] wrote: Neil, de Bruijn indicies look quite nice, and seem to eliminate a lot of complexity when dealing with free variables: http://en.wikipedia.org/wiki/De_Bruijn_index So I was wondering, are they suitable for use in a compiler? If so, what are their disadvantages/advantages? Is there any particular reason that GHC (as an example) doesn't use them in its Core? I'm trying to decide if I should use them in my compilers data type - and would like some recommendations before I start. De Bruijn indices are used within Epigram, or at least they used to be. Maybe the Epigram people can inform you about their experiences. 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. Cheers, Stefan [1] Conor McBride and James McKinna. Functional pearl: I am not a number—I am a free variable. In Proceedings of the 2004 ACM SIGPLAN Haskell Workshop, Snowbird, Utah, USA, September 22, 2004, pages 1–-9. ACM Press, 2004. http://portal.acm.org/citation.cfm?id=1017472.1017477 ___ 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 13/05/2007, at 12:44, Neil Mitchell wrote: Hi Thanks for all the responses, I'm busy reading through them. I'm still trying to decide whether I should use them or not. They complicate things, are less intuitive than names. But on the other hand, the language I'm working in is untyped and has only letrec. These things make binding errors easier to occur, and harder to detect. Thanks for the helpful throughts, Neil The Calculus of Indexed Names and Named Indices (CINNI) [1] looks really neat: The Calculus of Indexed Names and Named Indices (CINNI) is a new calculus of explicit substitutions that combines names and indices in a uniform way. It contains the standard named notation used in logics and programming languages as well as de'Bruijn's indexed notation as sublanguages. Disclaimer: I haven't read the Epigram paper nor Berkling, so I don't know how it compares. And I can't really talk from my own experience, since I have not played myself with CINNI yet. I wish I had a build-a- language assignment, just so that I could put CINNI to work... [1] - http://formal.cs.uiuc.edu/stehr/cinni_eng.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Mathematica
Andrew Coppin [EMAIL PROTECTED] wrote in article [EMAIL PROTECTED] in gmane.comp.lang.haskell.cafe: The absurdly efficient number crunching is obviously not implementable in Haskell - or indeed virtually any language except assembly. [...] The pretty user interface is obviously not implementable in Haskell. [...] It seems it would be a fairly difficult task to implement the pattern matching engine properly. Why? -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig 2007-05-15 International Conscientious Objection Day http://wri-irg.org/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Mathematica
Chung-chieh Shan wrote: Andrew Coppin [EMAIL PROTECTED] wrote in article [EMAIL PROTECTED] in gmane.comp.lang.haskell.cafe: The absurdly efficient number crunching is obviously not implementable in Haskell - or indeed virtually any language except assembly. [...] The pretty user interface is obviously not implementable in Haskell. [...] It seems it would be a fairly difficult task to implement the pattern matching engine properly. Why? Writing *insanely* efficient number chrunking software requires a deep understanding of the target architecture, and lots of playing with very low-level constructs. Assembly is really the only language you can do it with; even C is probably too high-level. The notebook interface is very sophisticated and clearly beyond the capabilities of any current GUI toolkit for Haskell. (Implementing this would be approximately as hard as writing a full web browser in Haskell.) The pattern matching engine could be implemented, but it's not a trivial task. Mathematica's pattern matching is quite sophisticated. It would take someone a while to do, that's all. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] hash of a lazy bytestring?
I was just contemplating hashes, and it occurred to me that it would be nice to be able to compute the hash of a lazily constructed bytestring and lazily consume its output without requiring the whole string to ever be in memory. Or in general, it'd be nice to be able to perform two simultaneous consumptions of a lazy list without requiring that the entire list be stored. Another example would be computing the length of an ordinary list: do l - readFile foo let len = length l writeFile bar l putStrLn $ Length is ++ show l It would be nice if one could write length such that the above function doesn't require the entire file be stored in memory. Are there any approaches that would make this possible? The only approach I can imagine would involve something like weak pointers and finalizers. It seems like it'd be a useful paradigm, if it's possible. Basically to be able to write a lazy consumer that doesn't hold onto its input, but instead is computed as the garbage collector frees the input. Something like: length' :: [a] - Integer length' !xs = l' 0 `safeInterleave` xs where l' n [] = n l' !n (y:ys) = l' (n+1) `safeInterleave` ys safeInterleave :: (a - b) - a - b safeInterleave f !x = -- create weak reference to x, associate finalizer, -- so that if x is GCed, then we'll immediately -- evaluate f x before we lose the value of x. Is this possible? Would it be reasonable? I imagine we'd run into trouble with laziness keeping safeInterleave from being called, with the result that we'd hang onto x even though the safeInterleave would have hoped to allow x to be GCed. -- David Roundy http://www.darcs.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Compilling GHC on Vista
Hi all, I've solved the problem by adding the correct paths to the system's PATH variable. I don't know why, but it seems that just putting SET PATH=... in cygwin.bat doesn't work... Now I get the following message in the compilation itself (make): utils/Outputable.lhs:54: Failed to load interface for `Name': Bad interface file: stage1/basicTypes/Name.hi-boot-6 stage1/basicTypes/Name.hi-boot-6: openBinaryFile: permission denied (Permission denied) utils/Outputable.lhs:54: Module `Name' (hi-boot interface) does not export `Name' ghc: 20124240 bytes, 4 GCs, 47644/47644 avg/max bytes residency (1 samples), 1 6M in use, 0.00 INIT (0.00 elapsed), 0.11 MUT (0.23 elapsed), 0.01 GC (0.01 elap sed) :ghc make[2]: *** [stage1/utils/Outputable.o] Error 1 make[1]: *** [all] Error 1 make[1]: Leaving directory `/cygdrive/c/ghc-6.2.2-src/ghc-6.2.2/ghc' make: *** [build] Error 1 I used Run as Administrator to run Cygwin and I've disabled Vista's user account control. I also set GHC's foder and subfolders to not read-only. Has anyone any idea about what may be happening? Monique On 4/28/07, Claus Reinke [EMAIL PROTECTED] wrote: pps. ah, silly me. i finally understand that ghc ticket #1280 is not a ghc issue at all. if gcc depends on that same call, it will not see the mingw ld as executable, so might fall back on defaults later in the PATH, right? but that would make me wonder how anyone could have a vista build of ghc? perhaps they are using a newer mingw/gcc, with some workaround for the issue? well, i'll stop guessing here. there we go: http://sourceforge.net/forum/forum.php?forum_id=679462 .. * include/io.h (__mingw_access): New static inline wrapper to restore pre-Vista 'access (fname, X_OK)' behaviour. (__USE_MINGW_ACCESS): Use to map access() to __mingw_access(). .. that looks promising, doesn't it? claus -- __ Monique Monteiro, MSc MCP .NET Framework 2.0 / SCJP / IBM OOAD Project Manager Recife Microsoft Innovation Center +55 81 34198137 http://www.cin.ufpe.br/~mlbm http://thespoke.net/blogs/moniquelouise/default.aspx [EMAIL PROTECTED] MSN: [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] hash of a lazy bytestring?
On Sun, May 13, 2007 at 08:30:41AM -0700, David Roundy wrote: do l - readFile foo let len = length l writeFile bar l putStrLn $ Length is ++ show l Oops, of course this should have been show len in the last line. -- David Roundy http://www.darcs.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Compilling GHC on Vista
I've solved the problem by adding the correct paths to the system's PATH variable. I don't know why, but it seems that just putting SET PATH=... in cygwin.bat doesn't work... cygwin.bat is read before bash is started; bash later reads profile and bashrc files that tend to redefine PATH. for instance, '/etc/profile' puts '/usr/local/bin' and others at the front of PATH. claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] hash of a lazy bytestring?
On Sun, 13 May 2007, David Roundy wrote: I was just contemplating hashes, and it occurred to me that it would be nice to be able to compute the hash of a lazily constructed bytestring and lazily consume its output without requiring the whole string to ever be in memory. Or in general, it'd be nice to be able to perform two simultaneous consumptions of a lazy list without requiring that the entire list be stored. How about reading the same file twice? do l1 - readFile foo l2 - readFile foo let len = length l1 writeFile bar l2 ... Another solution would be loop fusion: do l - readFile foo len - writeFileAndComputeLength bar l ... A compiler might be able to do that for you. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
I think both Benja's and David's answers are terrific. Let me just add a reference. The person who's given these issues most thought is probably Per Martin-Löf. If you want to know more about the meaning of local connectives you should read his On the Meanings of the Logical Constants and the Justifications of the Logical Laws [1]. It consists of three lectures which I think are quite readable although I can recommend skipping the first lecture, at least on a first read-through since it's pretty heavy going. In the beginning of the third lecture you will find the classic quote: the meaning of a proposition is determined by what it is to verify it, or what counts as a verification of it This is essentially what both Benja and David said. hth, Josef [1] http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html On 5/11/07, Benja Fallenstein [EMAIL PROTECTED] wrote: Adding some thoughts to what David said (although I don't understand the issues deeply enough to be sure that these ideas don't lead to ugly things like paradoxes)-- 2007/5/10, Gaal Yahas [EMAIL PROTECTED]: Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead: data Stream a = SHead a (Stream a) sMap :: (a - b) - Stream a - Stream b What is the object Stream a in logic? It's not that much more interesting than list. The 'data' declaration can be read as, To prove the proposition (Stream a), you must prove the proposition 'a' and the proposition 'Stream a.' In ordinary logic this would mean that you couldn't prove (Stream a), of course, but that just corresponds to strict languages in which you couldn't construct an object of type Stream a (because it would have to be infinite). To make sense of this, we need to assume a logic in which we can have similar 'infinite proofs.' (This is the part where I'm not sure it's really possible to do. I haven't read the Pierce chapter David refers to.) With that reading, (Stream a) is basically the same proposition as (a) -- as evidenced by f x = SHead x (f x) -- f :: a - Stream a g (SHead x) = x -- g :: Stream a - a We can find more interesting propositions, though. Here's an example (perhaps not useful, but I find it interesting :-)): data Foo a b = A a | Fn (Foo a b - b) We can prove this proposition if we can prove one of these propositions: a a - b (a - b) - b ((a - b) - b) - b ... Each of these is weaker than the previous one; if x is a proof of proposition n, then (\f - f x) is a proof of proposition n+1. The fourth one is a tautology in classical logic, but not in intuitionistic logic. - Benja ___ 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] Higher order types via the Curry-Howard correspondence
2007/5/12, Derek Elkins [EMAIL PROTECTED]:
In Haskell codata and data coincide, but if you want consistency, that cannot be
the case.
For fun and to see what you have to avoid, here's the proof of Curry's
paradox, using weird infinite data types. We'll construct an
expression that inhabits any type a. (Of course, you could just write
(let x=x in x). If you want consistency, you have to outlaw that one,
too. :-))
I'll follow the proof on Wikipedia: http://en.wikipedia.org/wiki/Curry's_paradox
data Curry a = Curry { unCurry :: Curry a - a }
id :: Curry a - Curry a
f :: Curry a - (Curry a - a)
f = unCurry . id
g :: Curry a - a
g x = f x x
c :: Curry a
c = Curry g
paradox :: a
paradox = g c
Modulo the constructor and destructor invocation, this is just the
familiar non-terminating ((\x - x x) (\x - x x)), of course.
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
2007/5/13, Benja Fallenstein [EMAIL PROTECTED]: Modulo the constructor and destructor invocation, this is just the familiar non-terminating ((\x - x x) (\x - x x)), of course. The same technique also gives us data Y a = Y (Y a - a) y :: (a - a) - a y f = (\(Y x) - f $ x $ Y x) $ Y $ (\(Y x) - f $ x $ Y x) or y :: (a - a) - a y f = g (Y g) where g (Y x) = f $ x $ Y x as well as these formulations, which make GHC loop forever on my system: y :: (a - a) - a y f = (\(Y x) - f (x (Y x))) (Y (\(Y x) - f (x (Y x y :: (a - a) - a y f = g (Y g) where g (Y x) = f (x (Y x)) (Aaah, the power of the almighty dollar. Even type inference isn't safe from it.) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
On 5/13/07, Josef Svenningsson [EMAIL PROTECTED] wrote: I think both Benja's and David's answers are terrific. Let me just add a reference. Yes, this entire thread has been quite illuminating. Thanks all! The person who's given these issues most thought is probably Per Martin-Löf. [...] In the beginning of the third lecture you will find the classic quote: the meaning of a proposition is determined by what it is to verify it, or what counts as a verification of it I like how this is reminiscent of Quine's ideas in On What There Is. Another reference to add is Simon Thompson, _Type Theory and Functional Programming_, which I stumbled upon online here: http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ . -- Gaal Yahas [EMAIL PROTECTED] http://gaal.livejournal.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] hash of a lazy bytestring?
On Sun, 13 May 2007, David Roundy wrote: I was just contemplating hashes, and it occurred to me that it would be nice to be able to compute the hash of a lazily constructed bytestring and lazily consume its output without requiring the whole string to ever be in memory. Or in general, it'd be nice to be able to perform two simultaneous consumptions of a lazy list without requiring that the entire list be stored. Another example would be computing the length of an ordinary list: do l - readFile foo let len = length l writeFile bar l putStrLn $ Length is ++ show l An elegant implementation of 'wc' is another example. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
