-
Notifications
You must be signed in to change notification settings - Fork 1
Pure Logic Programming
The concept of pure logic programming has been mentioned in miniKanren among others. For a complete overview,
https://www.metalevel.at/prolog/purity
Since the above provides an in-depth view, we only give a simple definition.
A program that only makes use of pure relations is pure.
Therefore, one way to make a pure relation is simply by not using any impure ones.
They user is free to use and/or
, if
, not
, etc. making sure to type it as rel
. However, they should not use I/O
, throw
, choose
, math.random
, etc.
In summary, all you have to do is avoid using an impure relation. On the other hand, this also means a single impure relation might ruin an attempt to do a pure program.
An user may want at some point to knowingly abandon the notion of a pure program- functions like math.random
are provided explicitly for that reason.
A program that isn't pure in a LP sense is likely to still be pure on a functional sense.
For a given input, a function always returns the same output.
> y = double(3)
| y=6
A pure function double
always returns 6 given the input 3.
As long as the user doesn't use I/O, etc. they can still satisfy the definition of a pure functional program.
Logical purity may be understood as an extension of functional purity. In the case of logical purity, however, multiple outputs may be given. Similarly, different parameters can be used as the input/output parameters.
Few relations provided by the libraries are impure, so that unless the programmer decides to use an obviously extraneous relation like throw, a program will be pure otherwise.
Although not perfect, the user can reasonably try logic programming while only rarely running into an impure construct. It is closer to kanren-style than oldschool style.
However, one or other relation may still fail to be complete when compared to a kanren ideal.
Consider the following program,
t[1] = 2
If t
is not instantiated, the result of evaluating such a program might be,
(1) Complete,
It lists possible values for t such as {1=2} or {1=2|_}.
(2) Sound,
It succeeds but delays any answer.
(3) An error,
It throws an error. The third option is pure on the sense that t cannot be uninstantiated. The program warns such a program would be incorrect and the user will make a program where t is instantiated. It's better than a false
result, for instance.
> y = math.floor(2.3)
| y = 2
> 2 = math.floor(x)
| true
As, unlike kanren, Cosmos is a general-purpose language, not a library, cost-performance benefits might be weighted in. This means that unlike kanren, we do not guarantee a perfect 1 result every time, although 1-2 is preferable.
The above is a good example. Although a kanren-style language may prefer to give a more elaborate answer to the problem, it may be enough for a floor function to use the delay approach.
The language is in-development so that whether we go for either may even change depending on how it develops, or whatever users deem worth it.
As an early high-level experimental language that doesn't need to maintain backward-compatibility with oldschool logic programming, Cosmos has the perfect opportunity to explore pure LP.
We don't guarantee that we will/won't keep pursuing PLP, however, it seems to be the case. Although in the worst case we could switch to an oldschool approach, that would bring its downsides. It's also possible that as advances are made in PLP, we incorporate them into the language if possible.
Ultimately, our intention is to facilitate pure programming more than to forbid impure programming.
Having immutable variables and data structures go a much longer way toward pure programming than whatever benefit there is in "forbidding" a print statement to the point where a simple hello world
program cannot be written in it.
print('hello world')
If the programmer so much as decides to use a graphical interface, the problem disappears.
cut
It may seem odd that constructs like cut are available. Still, consider that a lot of use of LP languages is academical. Not including them would mean our language cannot be used to illustrate such constructs, thus its potential uses decrease.
This is also mixed priorities, and one may compare it to forbidding goto in a procedural language. Whether or not goto is available, its usage in high-level languages would be limited simply because higher-level constructs make goto unnecessary. Whether or not such a construct is provided is similarly unimportant.