Where's formal proof of Haskell's claim to...?

chris glur — 2015-02-11 15:22:34

be able to avoid the need to tell the machine what to do step-by-step,
and just provide it with a <description of the problem>, and allow it
to workout/search for a route to the solution?


Since we've learned to accept compilers that work-in-the-dark,
Haskells claim seems promising.


Is this a theory that can be demonstrated by graduated examples,
hopefully published somewhere?


Is it perhaps related to unification - like prolog?

Michael Haufe — 2015-02-23 18:52:46

On Wed, Feb 11, 2015 at 9:22 AM, chris glur wrote:
> Where's formal proof of Haskell's claim to be able to avoid the need to
> tell the machine what to do step-by-step, and just provide it with a
> <description of the problem>, and allow it to workout/search for a route
> to the solution?
[...]
> Is this a theory that can be demonstrated by graduated examples,
> hopefully published somewhere?

Do you have a specific quote in context for the claim for better
understanding of the question?

The general theory is the Church–Rosser theorem:
<http://en.wikipedia.org/wiki/Church–Rosser_theorem>

If there exists a machine checked proof of this property for Haskell
and to what degree, I am unaware of one. I suspect if it does exists
it is specifically for a targeted subset that Haskell compiles to (System-F like?).

For more information useful to this topic, I suggest taking a glance
through SPJ's book IFPL:

http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/

chris glur — 2015-03-01 07:39:52

]> Where's formal proof of Haskell's claim to be able to avoid the need to
]> tell the machine what to do step-by-step, and just provide it with a
]> <description of the problem>, and allow it to workout/search for a route
]> to the solution?
]
] Do you have a specific quote in context for the claim for better
] understanding of the question?


http://blog.wolfram.com/2015/02/11/qa-with-michael-tiller-
author-of-modelica-by-example/


Modelica is important because, as I mentioned previously, it
captures a representation of people's models in an open way and in a
way that can be reasoned about. This comes from the fact that
= Modelica is a declarative language, not an imperative language. When
you deal with typical programming languages, the imperative
constructs (e.g., do this, now do that, now loop until this is true,
then overwrite that result) make it nearly impossible to actually
extract the high-level intention of the user (at least not without a
tremendous amount of discipline). Modelica is not a language of
statements and operations, it is a language of relationship: how
variables relate to each other through an equation, how the values
of a variable are related to a type (and its physical units), how a
resistor is related to a capacitor through connections in a
schematic diagram. The point is that the structure of the model and
all of these relationships are always preserved in Modelica.


This property has been leveraged extensively to create very fast
simulations by being able to reason about these relationships. We
can see which variables depend on which other variables and use this
to efficiently perform calculations, minimize the number of
variables involved in solving nonlinear systems, recognize which
signals are synchronized with other signals to ensure determinism in
results, and so on.
----------------------------------------
This chant which is apparently based on psychology/cognition is often seen.
The above author is also unable to analyse his own mental processes,
so he's just saying "it's nice" - in many words.


Only recently, decades after grad: CS+Maths have I discovered the
productivety of the composition of functions.
Unfortunately, the syntax of unix piping is an ad hoc mess [as well
criticised by Xhalee], but the economy of effort is remarkable.


My analysis: why "it's nice"; is that it's cost effective of my effort/pain,
because seldom do you need to abandon your invested effort and restart,
[which IMO is M$ secret: DOS users could extend their investment to Win]
because you can confirm the results at each of N stages,
and the original cost of each of the functions is amortised over many jobs,
[which is the tool box metaphor of unix].


The details of <impedance-matching/currying> between stages etc, only comes
after the TOP LEVEL justification has been stated; instead of starting with
examples.
Here's my latest example [to find the smallest *.nb in a big-dir-tree]:-


list the zillion *.nb files in the dir-tree, showing their sizes
+ extract the size-field to the left [most significant] position
+ sort them
+ show me just the first 3.


So there are only 4 concepts to burden the user.
And the whole job can be progressively tested.


A pointer from this forum, to a publication on the <effectiveness of
combinators> which started correctly, by recognising the goal of labour
saving, took as it's example: pretty printing; but unfortunately for
me, is based on haskell tools. So I opened the haskell can-O-worms.


So I want to know UP FRONT haskell's basis of it's claim to superiority
over eg. Pascal.


== Chris Glur.