Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Imperative Haskell

vaibhavsagar.com

Post reply on HN
Print view View original

31–40 of 73 posts

Re: Imperative Haskell

#31

Post by fizixer »

The first code block reads like a definition, or the 'what' of quicksort, which has to be fleshed out using the 'how' of quicksort. And it just so happens that 'what' is declarative, and 'how' is imperative (i.e., do this, do that, that's how).

Speaking of which, there is a definition of, not quicksort, but sort itself, and it goes something like this:

'sort is a map that takes a sequence S of orderable items, to one of its permutations P such that for every two adjacent elements e1, e2 in P, e1 I'm not familiar with Haskell syntax but I'm sure this definition can be encoded in Haskell. Actually imperatively speaking, this is a sort algorithm itself, the very less discussed (probably because of very high complexity) 'permutation sort', i.e. you keep permuting the input sequence and keep checking your e1/e2 condition until it is satisfied.

So we can define sort, but then we can specify a language to not compute based on that definition but instead pick from one of the preferable computation schemes that are also defined in that langauge (quicksort, mergesort, etc, etc). But then we specify not to use the definition of that scheme but instead use an algorithm for it (e.g., the imperative algorithm for quicksort).

I guess this is a form of semantic layering, something that I'm interested in as a topic of study.

Re: Imperative Haskell

#32

Post by heavenlyblue »

fizixer wrote: post #31

The first code block reads like a definition, or the 'what' of quicksort, which has to be fleshed out using the 'how' of quicksort. And it just so happens that 'what' is declarative, and 'how' is imperative (i.e., do this, do that, that's how). Speaking of which, there is a definition of, not quicksort, but sort itself, and it goes something like this: 'sort is a map that takes a sequence S of orderable items, to one…

It would also be interesting to extend this language to the one that also has partial conditions satisfied, e.g.: - We have a set S of tuples (a,b,c) sorted by (a,b) - We would like to sort S by (a,b,c) - Therefore we only need to only sort subsets (a,b,cx)

By the way, permutation sort would be reducing the sorting algorithm to a problem of search in the configuration space of N variables. Speaking generally, you may reduce any problem to a search problem; so this doesn't only work for sorting.

Re: Imperative Haskell

#33

Post by sbergot »

lgas wrote: post #10
lgas wrote: post #8

Earlier quoted context omitted.

I tried to do some quick benchmarks: % make hs Results: [25872791,24253954,21258158] make hs 6.53s user 3.99s system 245% cpu 4.282 total % make py 24029582 25343914 20814678 make py 22.37s user 0.11s system 99% cpu 22.593 total You can see the code as tested here[0]. I am not an expert on either Haskell or Python performance, all I did was use -O for python3 and -O2 for GHC. This was on a 2.8 GHz Core i7 Macbook, FW…

I was playing around a little more and I noticed that stack sets the following ghc-options by default: -threaded -rtsopts -with-rtsopts=-N which I assumed explained some of the speedup, so I disabled them and got a reduction to 99% cpu as expected, but unexpectedly the single threaded version was about twice as fast: % make hs Results: [24605537,25150983,21576960] make hs 3.13s user 0.07s system 99% cpu 3.211 total

Haskell threaded runtime can have poorer performances than the non-threaded one on single threaded programs.

Re: Imperative Haskell

#35

Post by mietek »

cousin_it wrote: post #11
runeks wrote: post #3

As far as I'm concerned, purity is more fundamental than impurity, because we can always emulate impurity using a pure language (as is shown in this article), but it's not possible to emulate purity using an impure language. This only leaves us with the challenge of performance. While we can always describe e.g. x86 assembly in terms of a pure intermediate representation language (e.g. GHC Core), transforming this de…

Purity is tricky to define. For example (stolen from Reddit user gasche), if you can measure how much time a computation takes, then Haskell is impure, because a lazy value takes longer to compute the first time than the second. You could try to patch it up by saying the impurity must be observable via pure code, but that makes the definition circular. And that raises another problem, where printing to standard outpu…

> You'd think that ST itself can be implemented in pure Haskell, maybe with the usual logarithmic slowdown. But unfortunately no one knows how to do it, and there's a strong suspicion that the (pure) type signature of runST has no pure implementation at all ...

This information may be out of date. There are now at least two Agda formalisations of runST (by Andrea Vezzosi and András Kovács), and a paper by Timany et al. on the subject of runST has been submitted to ICFP'17.

http://code.haskell.org/~Saizan/ST/ST.agda

http://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8d...

http://iris-project.org/pdfs/2017-icfp-runST-submission.pdf

Re: Imperative Haskell

#36

Post by cstrahan »

cousin_it wrote: post #25
lmm wrote: post #20

Earlier quoted context omitted.

A pure language is one in which replacing any subexpression of any expression with the evaluation of that subexpression yields an equivalent expression. Of course this means "pure" is not an absolute term but rather relative to a given definition of "equivalent". But this isn't circular and is practically useful: if you're working in a context where precise execution time matters (e.g. cryptography) you really do nee…

I think this is a good take. Is there a natural definition of equivalence that includes standard output effects but excludes time and space effects, short of enumerating all effects and saying which ones are ok?

Maybe something like this:

Equivalence: unification of types (can't make I'll-typed substitutions)

Output only effects: have your language define only one such monad

About to depart on a flight, so can't elaborate further.

Re: Imperative Haskell

#37

Post by cousin_it »

mietek wrote: post #35
cousin_it wrote: post #11

Earlier quoted context omitted.

Purity is tricky to define. For example (stolen from Reddit user gasche), if you can measure how much time a computation takes, then Haskell is impure, because a lazy value takes longer to compute the first time than the second. You could try to patch it up by saying the impurity must be observable via pure code, but that makes the definition circular. And that raises another problem, where printing to standard outpu…

> You'd think that ST itself can be implemented in pure Haskell, maybe with the usual logarithmic slowdown. But unfortunately no one knows how to do it, and there's a strong suspicion that the (pure) type signature of runST has no pure implementation at all ... This information may be out of date. There are now at least two Agda formalisations of runST (by Andrea Vezzosi and András Kovács), and a paper by Timany et a…

AFAIK the Agda implementations use a closed universe of types and cannot be translated to an implementation of runST in Haskell which doesn't have that restriction. Please correct me if I'm wrong. From a quick reading I can't tell if the new paper makes progress on that front, what do you think?

Re: Imperative Haskell

#38

Post by infinisil »

fizixer wrote: post #31

The first code block reads like a definition, or the 'what' of quicksort, which has to be fleshed out using the 'how' of quicksort. And it just so happens that 'what' is declarative, and 'how' is imperative (i.e., do this, do that, that's how). Speaking of which, there is a definition of, not quicksort, but sort itself, and it goes something like this: 'sort is a map that takes a sequence S of orderable items, to one…

That's where formal proofs come into play, because you need to somehow show that the implementation actually does what the definition states. Since Haskell isn't a proof checker you can't use it for this. The newish and very promising looking language Idris [1], which is very similar to Haskell, can actually do this because of having dependent types. Upon a quick search I found this great example [2] of a proof that insertion sort does indeed return the list sorted, all in the type system. I can really recommend Type Driven Development [3], a recently released book on development in Idris.

[1]: https://www.idris-lang.org/

[2]: https://github.com/davidfstr/idris-insertion-sort

[3]: https://www.manning.com/books/type-driven-development-with-i...

Re: Imperative Haskell

#39

Post by lmm »

cousin_it wrote: post #25
lmm wrote: post #20

Earlier quoted context omitted.

A pure language is one in which replacing any subexpression of any expression with the evaluation of that subexpression yields an equivalent expression. Of course this means "pure" is not an absolute term but rather relative to a given definition of "equivalent". But this isn't circular and is practically useful: if you're working in a context where precise execution time matters (e.g. cryptography) you really do nee…

I think this is a good take. Is there a natural definition of equivalence that includes standard output effects but excludes time and space effects, short of enumerating all effects and saying which ones are ok?

From a denotational/lambda-calculus perspective it's very natural to consider all expressions that reduce to the same expression as equivalent, at which point you have that definition of equivalence. Of course in the pure lambda calculus all "programs" are just (equivalent to) values. To get any effects like input/output you have to add extra values, and at that point you decide what the equivalence semantics of these "special" values are. That's kind of the Haskell perspective, and where I think it falls down is in the interaction between sequenced I/O and pure functions; the pure subset of Haskell can be fully evaluated at compile time (if you work in e.g. Idris this becomes true in a very direct sense: your (total) pure functions can be used in types), but as soon as a value depends on user input that obviously ceases to be the case, whereas expect to be able to decompose their program into pure and impure fragments and reason about these separately.

From an operational perspective a good definition of equivalence would be very difficult. E.g. if your language allows making system calls there are dozens or hundreds of those with no real model of how they interact, so it's very hard to say when one sequence of system calls is equivalent to another. Possibly the most natural notion of operational equivalence is to say two programs are equivalent if they execute the same sequence of CPU instructions, but that would mean that nontrivial programs were virtually never equvialent to each other, even if they both just printed the same string.

Re: Imperative Haskell

#40

Post by lmm »

arximboldi wrote: post #26
T-R wrote: post #7

Earlier quoted context omitted.

Impurity is a lack of constraints. You can, with impure code, write an interpreter for a language that constrains code to being pure, and implemented correctly, you can then depend on code written in that langauge to be pure. His point is that there's no lost benefit in calling pure code from impure code - the code is already unconstrained. Calling impure code from pure code, though, means you've lost the purity cons…

Following your argument to the extreme, Haskell is also an impure language: there could be a bug in the compiler, or someone could introduce impurity in it! Even worse, someone could call unsafePerformIO ! You would argue: but that goes against the Haskell specification, that impurity is not proper Haskell! And exactly: the "purity" comes from an abstraction, which is a contract between you and some other developers.…

In theory it would be possible to write a specification for a pure subset of JavaScript. But it's very important to acknowledge that this pure subset doesn't exist, and won't exist unless and until such a specification is written, to the point that it's possible to write an automated tool that can verify whether a given piece of code conforms to this specification. And if such a specification did exist, we would likely call it a "language" in its own right.

Once you write that language and confirm that your library conforms to it you can say your library is pure. Saying your library is pure before you've actually formally checked it is like saying your library doesn't have any bugs in before you've made any attempt to look for them - i.e. almost certainly a false, and so irresponsible to claim that it qualifies as a lie in my book.

Post reply on HN