[Haskell-cafe] Pure functional and pure logical language at the same time
nickolay.kudasov at gmail.com
Thu Jan 29 20:14:50 UTC 2015
Disclaimer: I have not worked in either of the languages I am talking about
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
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>
>> 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
>>> 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
>>> 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>
>>> > This question was bugging me for quite a long time. Can we have a
>>> > which uses the functional logic while being both pure functional and
>>> > 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
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe