Bool is not...safe?!

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
26 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: Bool is not...safe?!

Olaf Klinke
>
>> true = return ()
>> (&&) = liftM2 const
>> (||) = mplus
>> false = mzero
>
> I don't think it's by definition yet, but surely by convention, that
> this is a restricted form of
>
> true  = pure ()
> (&&)  = (<*)
> (||)  = (<|>)
> false = empty
>
> All of these functions require only an Applicative or an Alternative,
> and except for "true", they're all in the library.

True, and after sending I realized I should have used exaclty the definitions you gave. It's just that I don't know whether there exists the concept of "commutative applicative". It is equired for (&&) to be commutative. How could one even state it without the monad bind? The following definitions are from a category theory paper [1] by Anders Kock.

import Control.Monad
-- tensorial strengths
t'' :: (Functor m) => a -> m b -> m (a,b)
t'' a mb = fmap (\b -> (a,b)) mb

t' :: (Functor m) => m a -> b -> m (a,b)
t' ma b = fmap (\a -> (a,b)) ma

-- so-called linear extensions in the first and second argument
linearext1 :: Functor m => (m c -> c) -> (a -> b -> c) -> m a -> b -> c
linearext1 struct f ma b = struct $ (fmap $ uncurry f) $ t' ma b

linearext2 :: Functor m => (m c -> c) -> (a -> b -> c) -> a -> m b -> c
linearext2 struct f a mb = struct $ (fmap $ uncurry f) $ t'' a mb

The first argument to linearext1 and linearext2 is called a "structure map" in the context of [1]. Such structure maps exist when m is a monad. Indeed, we have

linearext1 join t'' :: (Monad m) => m a -> m b -> m (a, b)
linearext2 join t'  :: (Monad m) => m a -> m b -> m (a, b)

Now m is called commutative if the above two maps are the same [*]. But join does not exist for applicative functors, it is interdefinable with (>>=).

Olaf

[1] Anders Kock: "Commutative Monads as a Theory of Distributions".
Theory and Applications of Categories, Vol. 26 No. 4 (2012).
[*] They are called Fubini maps because a special case is Fubini's theorem about integration by parts.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Bool is not...safe?!

Olaf Klinke
In reply to this post by Paul
>But in Prolog every piece of code is evaluated to TRUTH or to FALSE. Each sentence is a goal which can be achieved and becomes a fact >or can not be – and becomes lie. So, if you inverse semantic in Haskell – program is compiled although with strange behaviour but in >Prolog program become lie. Prolog evaluation model has clean definition in run-time too, not only at compile-time. Execution of >Prolog program is a CHECK: is it truth or lie?

I have only very limited Prolog pratice. But what you state about Prolog's semantics is only true for very simple cases, isn't it? As soon as I/O is involved, things get messier. Also, there are actually three outcomes as far as I know: provably true, provably false and "could not be proved" which is different from "false".

When I anticipate an exception in an application where the condition prohibits the program from fulfilling its purpose, I simply call error. A common pattern I use is a library function that has return type (Either SomeErr Value), and the application takes it and wraps the result in either (error.show) return, transforming (Either SomeErr Value) into (IO Value). For libraries, one should be more careful, as we don't know what kind of environment the function might be called in - see Joachim Durchholz's post.

Olaf
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Bool is not...safe?!

Paul
In reply to this post by Joachim Durchholz

@Olaf Hello, you are right. Prolog allows side-effects, which means that you has predicates which is not “pure”. Today, after “pure” functional programming fashion, there is fashion of pure declarative programming too 😊 You define nature of predicates with determinism categories but “variables” nature with +/- notation (if variable is “output” only then it’s not pure predicate, for example, “X is Y + 5” is not pure because it’s functional but not declarative, ie, it’s evaluation but not relation). Mercury has “!” annotation, which is close to linear types I suppose (am I right?). Idea was side-effects is coded as input-output variable which is changing (state of external world). Unfortunately, I learned Prolog when I was student... 

 

When we are talking about truth, probably truth, etc, I think we mean https://www.mercurylang.org/information/doc-latest/mercury_ref/Determinism-categories.html. In Prolog we apply restrictions/relations to answer to get more strict answer. It’s linked with declarative nature: no evaluation but some kind of DSL to barrier answers. Sure, it’s not strict definition or something like this 😊 My intuition is like Prolog evaluation can be imagine in Haskell terms like some logic monad on top level instead of IO monad (main :: SomeLogic (), for example). Btw, how works Curry? And another my intuition is that it’s possible in Haskell with some (new?) monad. I will observe your examples, thanks a lot!

 

@Joachim.

Hello again. Let’s talk about Haskell and not persons. I suppose that my not good English may lead to misunderstanding. Excuse me, in this case. If you allow me, I would like to show reasons why I said “imperative” and not declarative.

 

In Haskell I can write:

 

factorial 0 = 1

factorial n = n * factorial (n - 1)

 

I can call it: factorial 5 => 120.

 

And often I meet in Web similar examples with note: “You see – Haskell is declarative language, it really looks declaratively”. IMHO it looks only (you can check Erlang syntax, which is similar to Prolog even, but Erlang is not declarative language). Let’s try the same in Prolog.

 

factorial(0, 1).

factorial(N, F) :-

        N #> 0,

        N1 #= N - 1,

        F #= N * F1,

        factorial(N1, F1).

 

I can call it: factorial(5, X) => X=120.

But also: factorial(X, 120) => X=5.

 

We see principal difference:

  1. In Haskell we map inputs (arguments) to result. In Prolog we define not mapping but relation, which is bi-directional while Haskell is one-directional, like C, Java, etc. We can find also arguments from result in Prolog.
  2. In Haskell like in any imperative language we describe exact algorithm/solution. We define HOW. In declarative language we define WHAT: we restrict result and don’t know actually how it will be evaluated.
  3. In Haskell all is evaluated as you wrote code. Exactly. No magic. But in Prolog we restrict some solver to find answer (or answers). In the example this solver is called CLP(FD). Sure, there are other solvers. Modern Prolog systems contain a lot of solvers, expert system engines, etc, etc. So, Haskell has not solvers/engines. Prolog has. Prolog is DSL for solvers. Interesting analogue is SQL as DSL for RDBMS😊

 

If we want to achieve the same magic in Haskell, we must write such solver explicitly (ie. “how”).

 

Another interesting speculation about real nature of Haskell is List monad. We often see “Haskell is declarative because it has backtracking” with attached some example of List monad/do/guard. But we can say that Python is declarative because it has permutations in its itertools module which allows to solve similar tasks. We understand that List monad is not backtracking, and “guard” is similar to Smalltalk “ifTrue” – no magic, no real backtracking. But like Python itertools can be used to solve some logic tasks in bruteforce/permutations style (as many other modern languages with sequences, F#, for example).

 

You said that “imperative” term is based on term of side-effects. May be I’m seriously wrong, but please, correct me in this case. IMHO side-effects are totally unrelated to imperative/declarative “dichotomy”. For example,

 

int sum(int a, int b) { return (a + b); }

 

I don’t see here side-effects. I have not problems to write all my C code in such style. Without any side-effects. Also I find “pure” functions in D language, “function” keyword in Pascal and Basic. But also I see

 

main :: IO ()

 

in Haskell. So, I don’t think side-effects are relative to declarative/imperative dichotomy at whole. When I was student, criteria of declarative/imperative was: functional, procedural, OOP languages are imperative, due to one-directional evaluation/execution and you code HOW to be evaluated, but declarative is bi-directional, you code relations (WHAT), between predicates and apply some restrictions.

 

I am surprised that there is another classification: based on side-effects. Please, correct me, where I’m wrong and if you can do it without such emotion – I will be very glad to get new knowledge.

 

PS. Out of scope is declarative DSLs written in imperative languages: like Scons Python build system. Sure, there are a lot of similar Haskell libraries/tools. IMHO more correct is to say “Scons has declarative Python-based DSL, but not Python is declarative itself”.

 

From: [hidden email]
Sent: 7 июля 2018 г. 11:17
To: [hidden email]
Subject: Re: [Haskell-cafe] Bool is not...safe?!

 

Am 07.07.2018 um 07:15 schrieb Paul:

> By the way, there are a lot of articles why checked exceptions are bad

> design (more problems than benefit).

 

That's because exceptions disrupt control flow.

If they're used as an alternative to pattern matching, i.e. thrown only

in tail position and always either fully handled or rethrown unchanged,

then they're fine.

 

I.e. checked exceptions are bad because they make it easy to construct

bad design. Unchecked exceptions can be abused in the same way but there

seem to be psychological reasons why this isn't done so often.

 

> More interesting for me is this snippet:

>

> case (action :: Either err a) of

>     Right result -> ...

>     Left err -> deal_with err

>

> Somebody says me that to use Bool in such way is “not safe” because no

> way to know what does “True” returning from “action” mean. Success or

> failure? But with some ADT (Success|Failure) code is more Haskellish and

> safe.

 

Terminology N.B.: (Success|Failure) is not an abstract data type (ADT).

It's pretty much the opposite of abstract.

 

> But is it true? We are talking about semantics, not type-safety because

> type-checker passes both cases (positive branch under False/Failure,

> negative branch under True/Success). But the same with Right/Left:

> nothing says you to use Right for positive and Left for error case. Is

> it true?

 

There's no good way to use Bool as the type of action, so the point is moot.

Of course you can reconstruct action's type to be a struct consisting of

a Bool, a SuccessResult, and a FailureResult, but that's just awkward so

nobody is doing this.

 

> Bool is algebra <1, 0, +, *>

 

Let me repeat: the algebraic and mathematical properties of Bool are

irrelevant.

 

> Problem with Haskell is that it’s imperative and not declarative

> language.

 

Haskell isn't imperative.

I.e. it matches almost none of the definitions for "imperative" that I

have ever seen.

It matches a substantial percentage of the definitions for "declarative"

actually, but not enough of them that I'd instinctively say it is really

declarative - others with a different set of definitions encountered may

feel differently.

 

> The root of the problem is that imperative nature of Haskell leads to

> missing term “evaluation to something”.

 

The most compact definition of "imperative" that I have seen is

"computation progresses by applying side effects".

By that definition, the ability to distinguish evaluated and unevaluated

expressions is irrelevant.

 

> Haskell program is not evaluated

> expression and in the same as in Java or C: it is IO action. But in

> Prolog every piece of code is evaluated to TRUTH or to FALSE. Each

> sentence is a goal which can be achieved and becomes a fact or can not

> be – and becomes lie.

 

Wrong terminology. Nothing in a computer is a lie.

 

Prolog works by turning stuff into either tautologies or contradictions.

A lie is something entirely different: a statement that intentionally

contradicts reality. Programming language semantics does not have

intention; programs may have state that matches or contradicts reality,

but take this message which isn't a lie but still does not match any

reality because no sheet of paper with these glyphs ever existed (there

may be in the future if somebody prints this message, but that doesn't

turn this message from a lie into a truth).

 

Please, get your terminology right. If you keep working with "almost

right" terminology in your head, you will continuously "almost

misunderstand" whatever you read, leading you to conclusions which are

almost right but take a huge amount of effort to clean up. People who

know the concepts and the terminology will find it too tiresome to talk

with you because it is all about educating you (which is not the right

level to talk with a person anyway), and will eventually drop out of

discussions with you; the only persons who talk to you will be those who

happen to have similarly vague ideas, placing you in an echo chamber of

ideas that lead nowhere because everything is subtly wrong.

Just saying. I'm not going to force anything on you - but I find that

this message is entirely about terminology correction and almost nothing

about the topics that really interest you, which means it's been mostly

a waste of time of both of us.

 

Regards,

Jo

_______________________________________________

Haskell-Cafe mailing list

To (un)subscribe, modify options or view archives go to:

http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

Only members subscribed via the mailman list are allowed to post.

 


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Bool is not...safe?!

Joachim Durchholz
Am 08.07.2018 um 09:43 schrieb Paul:
> @Joachim.
>
> Hello again. Let’s talk about Haskell and not persons. I suppose that my
> not good English may lead to misunderstanding. Excuse me, in this case.

Nah, you are mixing up terminology that is easily looked up.

> If you allow me, I would like to show reasons why I said “imperative”
> and not declarative.
>
> In Haskell I can write:
>
> factorial 0 = 1
>
> factorial n = n * factorial (n - 1)
>
> I can call it: factorial 5 => 120.
>
> And often I meet in Web similar examples with note: “You see – Haskell
> is declarative language, it really looks declaratively”.

"It's declarative because it looks declarative" is a circular argument,
and misses whatever definition of "declarative" was actually used.

BTW you don't define it either. Arguing around an undefined term is
pointless.

> We see principal difference:
>
>  1. In Haskell we map inputs (arguments) to result. In Prolog we define
>     not mapping but *relation*, which is *bi-directional* while Haskell
>     is *one-directional*, like C, Java, etc. We can find also arguments
>     from result in Prolog.

Yeah, that's the defining feature of Prolog-style languages.
And where the pure subset of Prolog is conceptually different from the
pure subset of Haskell.

>  2. In Haskell like in any imperative language we describe exact
>     algorithm/solution. We define *HOW*. In declarative language we
>     define *WHAT*: we *restrict result* and don’t know actually how it
>     will be evaluated.
>  3. In Haskell all is evaluated as you wrote code. Exactly. No magic.

Just as much or little magic as in Prolog.
Hey, FORTRAN's expression sublanguage was considered magic at the time
FORTRAN was written in all upper-case letters: You just write down the
expression, and the compiler magically determines what data to move
where to make it all happen.

So... "no magic" is not suitable as a criterion, because what's magic
and what's not is in the eye of the beholder.
Having written a Prolog interpreter, Prolog is as non-magical as C or
C++ to me; in fact I find Haskell's implementation slightly "more magic"
simply because I have not yet written a run-time for a lazy language,
but not *much* "more magic" because I happen to know the essential
algorithms. Still, Haskell's type system and the possibilities it offers
are pretty baffling.

>     But in Prolog we restrict some *solver* to find answer (or answers).

Except in cases where the solver is too slow or goes into an endless
loop. At which point we start to mentally trace the solver's mechanisms
so whe know where to place the cut, and suddenly that magic thing turns
into a complex-but-mundane machinery.

>     In the example this solver is called CLP(FD). Sure, there are other
>     solvers. Modern Prolog systems contain a lot of solvers, expert
>     system engines, etc, etc. So, Haskell has not solvers/engines.
>     Prolog has. Prolog is DSL for solvers. Interesting analogue is SQL
>     as DSL for RDBMS😊

Agreed.

> If we want to achieve the same magic in Haskell, we must write such
> solver explicitly (ie. “how”).

I got pretty disillusioned about Prolog when I tried to use it for
real-world problems. So I don't consider it much of a loss if you have
to code a solver if you want a solver.

> Another interesting speculation about real nature of Haskell is List
> monad. We often see “Haskell is declarative because it has backtracking”

Where did you see that claim?
Because at face value, this claim is hogwash. Haskell's semantics does
not have backtracking at all, and I doubt you'll find any runtime that
uses backtracking even as a mere implementation strategy.

> with attached some example of List monad/do/guard.

Which is unrelated to backtracking.

 > But we can say that
> Python is declarative because it has permutations in its itertools
> module which allows to solve similar tasks.

Python is a language where even class and function "declarations" are
executable statements (making it really hard to work with
mutually-referencing declarations so this isn't a mere theoretical
quibble but a hard, real-life problem), and that's as non-declarative as
you can get without becoming totally useless.

I'm awfully sorry, but this is the most ridiculous claim I heard in a
long time.
I am even more sorry but I do have to talk about humans: Please get your
definitions right. It's easy, even if English isn't your native language
(it isn't mine either).

 >
  We understand that List
> monad is not backtracking, and “guard” is similar to Smalltalk “ifTrue”
> – no magic, no real backtracking.

Well if that example was hogwash, why did you bring it up?

 >
  But like Python itertools can be used
> to solve some logic tasks in bruteforce/permutations style (as many
> other modern languages with sequences, F#, for example).

Sure. You can to functional, pure, declarative, context-free etc. stuff
in imperative languages no problem. You can even do that in assembler -
large systems have been built using such approaches.

That doesn't make the languages themselves functional/pure/etc.; the
definition for that is that the language does not allow doing anything
that is not functional/pure/whatever.
Very few languages are really one of these properties, it's almost
always just a subset of a language; still we say that Haskell "is pure"
because the pure subset is very useful and in fact most programmers
avoid going outside that subset. (People rarely use UnsafeIO. Whether
_|_, or equality under lazy evaluation, are compatible with purity
depends on details of your definition of pure, some people would say
yes, some would say no.)

> You said that “imperative” term is based on term of side-effects. May be
> I’m seriously wrong, but please, correct me in this case. IMHO
> side-effects are totally unrelated to imperative/declarative
> “dichotomy”.

That depends on what you consider declarative.
I am not aware of any widely-agreed-upon definition, so you have to
provide one before we can talk.

 >
  But
> also I see
>
> main :: IO ()
>
> in Haskell.

As far as I know, the IO monad does not execute any IO. It merely
constructs descriptions of what effects to invoke given what descriptions.
The actual execution happens outside the program, in the runtime.

That's why UnsafeIO is unsafe: It triggers IO execution inside the pure
Haskell world, possibly creating impurities where the language semantics
assumes purity (IOW you may find that compiler optimizations may change
the behaviour of the program).

> When I was student, criteria
> of declarative/imperative was: functional, procedural, OOP languages are
> imperative, due to one-directional evaluation/execution and you code HOW
> to be evaluated, but declarative is bi-directional, you code relations
> (WHAT), between predicates and apply some restrictions.

That's Prolog's idea of "declarative".
HTML, CSS, and most Turing-incomplete languages are considered
declarative, too.
Some people define "declarative" to be exactly the opposite of "imperative".

It's really a matter of definition.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Bool is not...safe?!

Paul
In reply to this post by Paul

Hello, Dušan!

> This is not Prolog, it is a Prolog with CLP extension over integers.

as well as Haskell has a lot of extensions. I mentioned CLP as solver but modern Prologs is not ISO only and has a lot of solvers (CHR, different CLP, FuzzyLogic, Tabulating, etc). Actually CLP(x) in included in most modern implementations.


09.07.2018 10:58, Dušan Kolář wrote:

Hello PY/Paul,

 

You are using misleading arguments!

 

This is not Prolog, it is a Prolog with CLP extension over integers.

 

>

> factorial(0, 1).

> factorial(N, F) :-

> N #> 0,

> N1 #= N - 1,

> F #= N * F1,

> factorial(N1, F1).

>

> I can call it: factorial(5, X) => X=120.

> But also: factorial(X, 120) => X=5.

>

 

Pure Prolog is:

 

factorial(0, 1) :- !.

factorial(N, F) :-

NN is N - 1,

factorial(NN, FF),

F is FF * N.

 

which is a function, not a relation, as you write.

 

 

 

Dušan Kolář

 



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Bool is not...safe?!

Paul
09.07.2018 11:50, Dušan Kolář wrote:

Hmm, but CLP has completely different way of evaluation and program construction than Prolog has. Moreover, stating it is a Prolog is not so much true then. That's the point as I can see it.

 

I got you. And this was my point, "declarative" for me, means some declarations/restrictions about answer/answers. No exact algorithm: you can even don't know how this is evaluated/executed. You only find some relations and declare them. And set of solvers tries to find solutions. So, modern Prolog/Logic systems are Prolog as DSL and set of solvers, right. For example, to find factorial as well as it's argument, you need to implement CLP library in Haskell explicitly (if you want to use CLP way). This is the Haskell tradition. Sure, you can do it in Python, in C (sure, such libraries already exist). But it's not declarative tradition: predicates calculus is based on backtracking and variables unification. Haskell, like Scheme is based on lambda calculus. So, evaluation is totally different.

But more interesting here (regarding to Bool subj)  is that Haskell can return to you 120 as factorial result, but Prolog will answer you (if it finds several results) "do you need next one?" and result in Prolog is "Yes.". This is important. Which can be imagine in terms of Haskell like you have not top-level `IO ()` but some `LogicMonad ()`. And all evaluations in Haskell will lead to Boolean (OK, truth/lie/yes/no) result. Evaluated (integers/floats/etc) result must be returned as output variables (your factorial is: `factorial(+N, -F)` i.e. it's one-directional only, so all functions in such Haskell also can return results in some reference/output var and evaluated to Bool). I can imagine this. Also if result is "No.", output variables unifications (bindings - in Haskell terms) will be dropped out. Unfortunately I dont know Curry and absolutely can not say: is it implemented in such way. But I'm sure that it's possible :)

Joachim pointed out "cut" operation which leads to more effective code, but eliminates pure logic constructs. There are "green cuts" (does not change semantic) and "red cuts" and this shows that practical real world languages mostly are not pure functional/pure logical.

But there is another point: it makes sense to have pure logical application which can be driven from C# or Java application (there are such puzzles and other games, on Android, Windows, tables/plane schedulers, expert systems, etc), but I can not imagine why I'll call for example, Haskell from the Java, because their area mostly are intersected in contrast with Java/Prolog, for example. This is some marker too, about which languages have similar "nature".

I have already agreed that are possible another classifications coordinates as well as it's difficult to classify some languages because they are totally hybrid (I remember yet another such: Racket, Oz/Mozart).

PS. I'm application developer only, not researcher, but I'm absolutely sure: there are people in the list which are totally in the subject, even may be some of them are devs of Curry or Mercury for example, and maybe they are laughing at me and my naive intuitions now :)


And it has nothing to do with Haskell extensions. In Haskell, the principle remains the same, though.

 

 

Dušan

 

On pondělí 9. července 2018 10:22:15 CEST you wrote:

> Hello, Dušan!

>

> > This is not Prolog, it is a Prolog with CLP extension over integers.

>

> as well as Haskell has a lot of extensions. I mentioned CLP as solver

> but modern Prologs is not ISO only and has a lot of solvers (CHR,

> different CLP, FuzzyLogic, Tabulating, etc). Actually CLP(x) in included

> in most modern implementations.

>

> 09.07.2018 10:58, Dušan Kolář wrote:

> > Hello PY/Paul,

> >

> > You are using misleading arguments!

> >

> > This is not Prolog, it is a Prolog with CLP extension over integers.

> >

> > > factorial(0, 1).

> > >

> > > factorial(N, F) :-

> > >

> > > N #> 0,

> > >

> > > N1 #= N - 1,

> > >

> > > F #= N * F1,

> > >

> > > factorial(N1, F1).

> > >

> > >

> > >

> > > I can call it: factorial(5, X) => X=120.

> > >

> > > But also: factorial(X, 120) => X=5.

> >

> > Pure Prolog is:

> >

> > factorial(0, 1) :- !.

> >

> > factorial(N, F) :-

> >

> > NN is N - 1,

> >

> > factorial(NN, FF),

> >

> > F is FF * N.

> >

> > which is a function, not a relation, as you write.

> >

> > Dušan Kolář

 



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
12