mafribe

77 ms·

1. 901.▲
   by mafribe 11y ago

   (1) I see no evidence of this. The ECB's flooding the world with Euros clearly inflates away net savers' wealth. (2) I agree that that's the game Greece has been playing. But it's perfectly compatible with what I said.
2. 902.▲
   by mafribe 11y ago

   (1) In what sense is loosing billions to Greece benefiting Germany? (2) Greece can change its exchange rate. Just declare bankruptcy and leave the Euro.
3. 903.▲
   by mafribe 11y ago

   I'm sorry that's misleading. Germany has one vote on the ECB, the same number as Greece, Spain, Portugal, Malta and every other country. Greece was perfectly happy to get cheap money. Instead of investing it in education, improved
4. 904.▲
   by mafribe 11y ago

   If nobody knows what purity means, then what are all those tortured discussions on whether Haskell is pure or not about? ... Anyway, I'm a bit unhappy about the requirement of full evaluation order independence, because even the purest
5. 905.▲
   by mafribe 11y ago

   I don't object to purity, I want to know what it means. I didn't realise that this is not a well-understood concept. (I mentioned Sabry's definition of purity which I found surprising.) The original discussion started becau
6. 906.▲
   by mafribe 11y ago

   SPJ and J Launchbury seem to think ST is pure. Looking over the PLDI paper, I get the impression that the key difference between ST and the usual State monad is (1) the ability to name state, and (2) the use of parametric polymorphism to pr
7. 907.▲
   by mafribe 11y ago

   By ST you mean Haskell's StateT monad transfomer? Are you suggesting to define purity by the inability to define O(1) mutable vector-like operations? That would be an interesting proposal. But I wonder if it captures the conceptual co
8. 908.▲
   by mafribe 11y ago

   Sure, if you use some of the unsafe stuff ... but what about the safe core of Haskell, do you consider that pure?
9. 909.▲
   by mafribe 11y ago

   Lazy is easy: it's call-by-name evaluation, i.e. (lambda x.M)N -> M[N/x] with caching, ie. each argument is evaluated at most once. Purity is more subtle. I don't think there's an agreed upon definition. [1] essential
10. 910.▲
    by mafribe 11y ago

    So you are saying Haskell is not a pure, lazy language?
11. 911.▲
    by mafribe 11y ago

    Calling loosing one's house and children a setback trivialises the matter, as if it happened by random chance. Instead he was the victim of institutionalised sexism/misandry in the UK which more or less automatically gives prefer
12. 912.▲
    by mafribe 11y ago

    C++ is impossible to validate formally. This is incorrect. Any language with a well-defined semantics (such as a compiler or interpreter) can be validated formally. It may just be too time-consuming for people to bother. For exa
13. 913.▲
    by mafribe 11y ago

    My interest is in proving expressivity results. Such proofs are much easier in a sequential setting. Indeed, at this point I don't even have a strong intuition what exactly the expressivity limitations of Haskell's monadic effec
14. 914.▲
    by mafribe 11y ago

    Thanks. I know that "pure" is not thread-safe. I'm quite happy to consider the expressivity of Haskell's monadic approach to effects in a sequential setting first -- much easier to reason about. I wonder if anybody has i
15. 915.▲
    by mafribe 11y ago

    Haskellers have a hard time translating an algorithm that's right in front of them That's no surprise: it is an open problem if this is possible in general. Some time ago Pippenger [1] showed that some programs cannot
16. 916.▲
    by mafribe 11y ago

    I'm not sure this kind of yes-anding makes the speaker appear smart. Isn't the purpose of yes-and to help ego to undercut alter's frame-setting through one-upmanhip? And isn't the purpose of the comic effect to divert th
17. 917.▲
    by mafribe 11y ago

    I'm not totally sure what you mean by "external proofs will ultimately be neglected".
18. 918.▲
    by mafribe 11y ago

    Thanks. This is very interesting, but different from what I used to believe about Haskell (as you can imagine, I'm not an active Haskell programmer). I will have to revisit my ideas. I still wonder how this would work with scope extrus
19. 919.▲
    by mafribe 11y ago

    If this is always possible without cheating, then I have definitely misunderstood something about Haskell. Could you point me towards an explanation how the hiding of stateful expressions works in Haskell in general? Let me clarify my quest
20. 920.▲
    by mafribe 11y ago

    The point of the example was to (1) use mutable state (hence force the state monad to show up in the function's type), but (2) in a way that defines a pure function. The example is intended to point towards an expressivity gap of the m
21. 921.▲
    by mafribe 11y ago

    I meant dependent types a la Agda, Coq etc that you can use for proving essentially arbitrary properties. Scala and Haskell do not have this.
22. 922.▲
    by mafribe 11y ago

    While f x = 0 is extensionally equal to the original program, it doesn't implement the algorithm in question (iteratively counting down a local reference).
23. 923.▲
    by mafribe 11y ago

    Thanks. Do any of these renditions have the target type int -> int?
24. 924.▲
    by mafribe 11y ago

    Thanks for your question. I should have been more careful. I meant Agda used as a prover, not Agda used as a 'conventional' programming language (Indeed in years of usage, I've never executed an Agda program, I've only e
25. 925.▲
    by mafribe 11y ago

    There are very different options. First, approaches like Eff take pure functional computation as a basis and layer effects like call/cc or concurrency on top of that. I think it's better to go the other way and take concurrency, o
26. 926.▲
    by mafribe 11y ago

    I don't fully agree with Pfenning here. The pi-calculus is not that good a proof system for linear logic: pi-calculus imposes sequentiality constraints on proofs that impede parallelism. Take for example the term x!<a> | y
27. 927.▲
    by mafribe 11y ago

    monads are merely an implementation of effect typing/purity. Yes, and the one Haskell has chosen. Is it the right way? Most newer languages are not following Haskell here, instead they have effects like state and exceptions
28. 928.▲
    by mafribe 11y ago

    I find (v) far more subtle than you make it out to be. I don't want to get start or be involved in another static-vs-dynamic typing debate. I have a strong preference for static types, but I appreciate the arguments of the o
29. 929.▲
    by mafribe 11y ago

    I don't think (iv) is open at all ... Function application is just one really well understood semantic foundation. I disagree, see my reply to "discreteevent" above. Parallel computing cannot be reduced to function
30. 930.▲
    by mafribe 11y ago

    Purity is growing more and more day by day. What I meant was this: a language should not be pure by default, rather, it should be possible to say (and get checked by the compiler): this is pure. Quite how to set up a pragmatically