Pure functional and pure logical language at the same time

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

Pure functional and pure logical language at the same time

Timotej Tomandl
This question was bugging me for quite a long time. Can we have a language which uses the functional logic while being both pure functional and pure logical?
Do we get any advantages from maintaining both both of this purities at the same time?

P.S.: I have feeling the answer is no, but I am not sure.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Joe Hillenbrand
What does "pure logical" mean?

On Wed, Jan 28, 2015 at 9:22 AM, Timotej Tomandl <[hidden email]> wrote:
This question was bugging me for quite a long time. Can we have a language which uses the functional logic while being both pure functional and pure logical?
Do we get any advantages from maintaining both both of this purities at the same time?

P.S.: I have feeling the answer is no, but I am not sure.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Simon  Thompson
You need to take a look at curry …


Simon


On 28 Jan 2015, at 17:37, Joe Hillenbrand <[hidden email]> wrote:

What does "pure logical" mean?

On Wed, Jan 28, 2015 at 9:22 AM, Timotej Tomandl <[hidden email]> wrote:
This question was bugging me for quite a long time. Can we have a language which uses the functional logic while being both pure functional and pure logical?
Do we get any advantages from maintaining both both of this purities at the same time?

P.S.: I have feeling the answer is no, but I am not sure.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Simon Thompson | Professor of Logic and Computation 
School of Computing | University of Kent | Canterbury, CT2 7NF, UK
[hidden email] | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Mathieu Boespflug
In reply to this post by Timotej Tomandl
By "pure logical", do you mean "logically consistent"? Or do you mean
a logic language in the style of Prolog but with no non-logical
effects such as programmatic pruning of the search tree?

If the former, there are many languages in that fit the bill (or at
least are believed to be consistent): Coq, Agda, HOL, ... The key
difference between those languages and Haskell is that all functions
must be provably total. See

https://uf-ias-2012.wikispaces.com/file/view/turner.pdf

from the father of a direct ancestor of Haskell, arguing for precisely
this: a total functional programming language (not that I agree that
such a language as proposed in the paper would be particularly
useful).

If you mean the former, there are language that try to combine logical
and functional programming, see e.g. Curry just mentioned in this
thread a few minutes ago.


On 28 January 2015 at 18:22, Timotej Tomandl <[hidden email]> wrote:

> This question was bugging me for quite a long time. Can we have a language
> which uses the functional logic while being both pure functional and pure
> logical?
> Do we get any advantages from maintaining both both of this purities at the
> same time?
>
> P.S.: I have feeling the answer is no, but I am not sure.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Timotej Tomandl
By pure logical I mean having features like in Pure Prolog.
I am not sure if Curry is pure functional or not. Is it?



2015-01-28 19:09 GMT+01:00 Mathieu Boespflug <[hidden email]>:
By "pure logical", do you mean "logically consistent"? Or do you mean
a logic language in the style of Prolog but with no non-logical
effects such as programmatic pruning of the search tree?

If the former, there are many languages in that fit the bill (or at
least are believed to be consistent): Coq, Agda, HOL, ... The key
difference between those languages and Haskell is that all functions
must be provably total. See

https://uf-ias-2012.wikispaces.com/file/view/turner.pdf

from the father of a direct ancestor of Haskell, arguing for precisely
this: a total functional programming language (not that I agree that
such a language as proposed in the paper would be particularly
useful).

If you mean the former, there are language that try to combine logical
and functional programming, see e.g. Curry just mentioned in this
thread a few minutes ago.


On 28 January 2015 at 18:22, Timotej Tomandl <[hidden email]> wrote:
> This question was bugging me for quite a long time. Can we have a language
> which uses the functional logic while being both pure functional and pure
> logical?
> Do we get any advantages from maintaining both both of this purities at the
> same time?
>
> P.S.: I have feeling the answer is no, but I am not sure.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Andy Morris-5
Yes. It has monadic IO exactly like Haskell's.

On 28 Jan 2015, at 19:22, Timotej Tomandl <[hidden email]> wrote:

By pure logical I mean having features like in Pure Prolog.
I am not sure if Curry is pure functional or not. Is it?



2015-01-28 19:09 GMT+01:00 Mathieu Boespflug <[hidden email]>:
By "pure logical", do you mean "logically consistent"? Or do you mean
a logic language in the style of Prolog but with no non-logical
effects such as programmatic pruning of the search tree?

If the former, there are many languages in that fit the bill (or at
least are believed to be consistent): Coq, Agda, HOL, ... The key
difference between those languages and Haskell is that all functions
must be provably total. See

https://uf-ias-2012.wikispaces.com/file/view/turner.pdf

from the father of a direct ancestor of Haskell, arguing for precisely
this: a total functional programming language (not that I agree that
such a language as proposed in the paper would be particularly
useful).

If you mean the former, there are language that try to combine logical
and functional programming, see e.g. Curry just mentioned in this
thread a few minutes ago.


On 28 January 2015 at 18:22, Timotej Tomandl <[hidden email]> wrote:
> This question was bugging me for quite a long time. Can we have a language
> which uses the functional logic while being both pure functional and pure
> logical?
> Do we get any advantages from maintaining both both of this purities at the
> same time?
>
> P.S.: I have feeling the answer is no, but I am not sure.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Timotej Tomandl
Second thing, is it purely logical?
And do we get any advantage when reasoning?

2015-01-28 19:27 GMT+01:00 Andy Morris <[hidden email]>:
Yes. It has monadic IO exactly like Haskell's.

On 28 Jan 2015, at 19:22, Timotej Tomandl <[hidden email]> wrote:

By pure logical I mean having features like in Pure Prolog.
I am not sure if Curry is pure functional or not. Is it?



2015-01-28 19:09 GMT+01:00 Mathieu Boespflug <[hidden email]>:
By "pure logical", do you mean "logically consistent"? Or do you mean
a logic language in the style of Prolog but with no non-logical
effects such as programmatic pruning of the search tree?

If the former, there are many languages in that fit the bill (or at
least are believed to be consistent): Coq, Agda, HOL, ... The key
difference between those languages and Haskell is that all functions
must be provably total. See

https://uf-ias-2012.wikispaces.com/file/view/turner.pdf

from the father of a direct ancestor of Haskell, arguing for precisely
this: a total functional programming language (not that I agree that
such a language as proposed in the paper would be particularly
useful).

If you mean the former, there are language that try to combine logical
and functional programming, see e.g. Curry just mentioned in this
thread a few minutes ago.


On 28 January 2015 at 18:22, Timotej Tomandl <[hidden email]> wrote:
> This question was bugging me for quite a long time. Can we have a language
> which uses the functional logic while being both pure functional and pure
> logical?
> Do we get any advantages from maintaining both both of this purities at the
> same time?
>
> P.S.: I have feeling the answer is no, but I am not sure.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Timotej Tomandl
I think I found the advantage it can give us abbility to combine inductive and deductive reasoning.

2015-01-28 19:37 GMT+01:00 Timotej Tomandl <[hidden email]>:
Second thing, is it purely logical?
And do we get any advantage when reasoning?

2015-01-28 19:27 GMT+01:00 Andy Morris <[hidden email]>:
Yes. It has monadic IO exactly like Haskell's.

On 28 Jan 2015, at 19:22, Timotej Tomandl <[hidden email]> wrote:

By pure logical I mean having features like in Pure Prolog.
I am not sure if Curry is pure functional or not. Is it?



2015-01-28 19:09 GMT+01:00 Mathieu Boespflug <[hidden email]>:
By "pure logical", do you mean "logically consistent"? Or do you mean
a logic language in the style of Prolog but with no non-logical
effects such as programmatic pruning of the search tree?

If the former, there are many languages in that fit the bill (or at
least are believed to be consistent): Coq, Agda, HOL, ... The key
difference between those languages and Haskell is that all functions
must be provably total. See

https://uf-ias-2012.wikispaces.com/file/view/turner.pdf

from the father of a direct ancestor of Haskell, arguing for precisely
this: a total functional programming language (not that I agree that
such a language as proposed in the paper would be particularly
useful).

If you mean the former, there are language that try to combine logical
and functional programming, see e.g. Curry just mentioned in this
thread a few minutes ago.


On 28 January 2015 at 18:22, Timotej Tomandl <[hidden email]> wrote:
> This question was bugging me for quite a long time. Can we have a language
> which uses the functional logic while being both pure functional and pure
> logical?
> Do we get any advantages from maintaining both both of this purities at the
> same time?
>
> P.S.: I have feeling the answer is no, but I am not sure.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe




_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Pure functional and pure logical language at the same time

Nickolay Kudasov
In reply to this post by Timotej Tomandl
Hello!

Disclaimer: I have not worked in either of the languages I am talking about (Curry, Mercury).

Curry is logical, but it uses different logic mechanisms than Prolog.
Curry is using something called "narrowing" which is very different to Prolog's SLD-resolution. AFAICT narrowing (or needed narrowing) corresponds to lazy evaluation while SLD-resolution corresponds to strict evaluation.

Mercury is another language to combine functional and logical features. But while Curry is Haskell-based with added mechanism of narrowing, Mercury is Prolog-based with Haskell-like type system. As Mercury is based on Prolog, there is an interesting part of a type system that corresponds to in/out parameters of a predicate. A predicate may also have multiple type signatures (since a some parameters may be in/out switched). The way Mercury treats IO in a pure way is also interesting (IIRC it uses something called unique parameter for the World).

I see both languages as "pure". Both languages have pure functional parts (deterministic functions in Curry and function signatures in Mercury).

I may be wrong, but it seems that of those two languages Mercury is a bit "more alive".

Best,
Nick

2015-01-28 21:37 GMT+03:00 Timotej Tomandl <[hidden email]>:
Second thing, is it purely logical?
And do we get any advantage when reasoning?

2015-01-28 19:27 GMT+01:00 Andy Morris <[hidden email]>:
Yes. It has monadic IO exactly like Haskell's.

On 28 Jan 2015, at 19:22, Timotej Tomandl <[hidden email]> wrote:

By pure logical I mean having features like in Pure Prolog.
I am not sure if Curry is pure functional or not. Is it?



2015-01-28 19:09 GMT+01:00 Mathieu Boespflug <[hidden email]>:
By "pure logical", do you mean "logically consistent"? Or do you mean
a logic language in the style of Prolog but with no non-logical
effects such as programmatic pruning of the search tree?

If the former, there are many languages in that fit the bill (or at
least are believed to be consistent): Coq, Agda, HOL, ... The key
difference between those languages and Haskell is that all functions
must be provably total. See

https://uf-ias-2012.wikispaces.com/file/view/turner.pdf

from the father of a direct ancestor of Haskell, arguing for precisely
this: a total functional programming language (not that I agree that
such a language as proposed in the paper would be particularly
useful).

If you mean the former, there are language that try to combine logical
and functional programming, see e.g. Curry just mentioned in this
thread a few minutes ago.


On 28 January 2015 at 18:22, Timotej Tomandl <[hidden email]> wrote:
> This question was bugging me for quite a long time. Can we have a language
> which uses the functional logic while being both pure functional and pure
> logical?
> Do we get any advantages from maintaining both both of this purities at the
> same time?
>
> P.S.: I have feeling the answer is no, but I am not sure.
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe