[Haskell-cafe] Pure functional and pure logical language at the same time

[Nickolay Kudasov]

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 <timotej.tomandl at gmail.com>:

> Second thing, is it purely logical?
> And do we get any advantage when reasoning?
>
> 2015-01-28 19:27 GMT+01:00 Andy Morris <andy at adradh.org.uk>:
>
>> Yes. It has monadic IO exactly like Haskell's.
>>
>> On 28 Jan 2015, at 19:22, Timotej Tomandl <timotej.tomandl at gmail.com>
>> 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 <0xbadcode at gmail.com>:
>>
>>> 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 <timotej.tomandl at gmail.com>
>>> 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
>>> > Haskell-Cafe at haskell.org
>>> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>>> >
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150130/358558e8/attachment.html>