Static Checks

Static Checking

Cosmos is statically-typed.

Before the language is run, programs are to be checked for errors in the compiling stage. This is different from runtime errors that happen when the program is running.

Types

What should happen when we compare values of different types?

1='b'

A possible solution is to make the comparison yield false. This is not wrong as 1 and 'b' are different values.

More often than not, though, comparing different types is a symptom of an error and not what the programmer wants. As such, you may get,

> x=1 and x='b'
| CosmosError: cannot unify types 'Number' and 'String'

The same can happen with relations.

double(2,'y')
| CosmosError: calling relation "double" of type 'Relation Number Number' as 'Relation Number String'

Once you understand that Relation Number Number is a relation that takes two numbers, this error is actually very readable.

Thanks to latest advances in FP, the compiler is able to detect types even when not explicitly typed by the user.

This allows for a very free style. The programmer may write very simple code, e.g. x=1, and the compiler can infer that x is a number. It would be more verbose to write Number x=1.

Composite Types

You may freely make what we call a composite type with functors.

Functor String Number f2 = F('apple', 2)

Or,

functor(F, Functor String Number)
f2 = F('apple', 2)

As previously shown, relations are no different. Relation Number Number is written as a composite type.

Types	Data
Functor	a functor
Functor Any Any	a functor with two unspecified arguments
Relation Number String	a relation with number and string arguments
Number	a number, e.g. 1
Table	a table, e.g. {x=1 and y='2'}

Note that Functor Any Any refers to a functor with two parameters, while Functor is any functor whatsoever.

This is intuitive, though. If someone were to say, "I need a functor!" it clearly might be any functor, while if someone bothers to say "I need a 'functor number number'" they're making such an oddly specific statement that we may assume a 'functor number number number' will not suffice.

Custom Types

...

Modes

Modes are like types for logic programming. Cosmos™ provides two modes, rel and function (or fun). The latter essentially lets the user make a function.

This is simplified compared to modes in other LP languages as there's an intuitive and practical focus. It's based on the assumption that the programmer will either follow a pure logical style (in which case they may use rel) or needs to fall back from that (in which case function is enough). For simplicity, it ignores other, more specific cases, although more modes can be added if the need arises.

In Cosmos, a function is essentially a relation that's constrained and has limited behavior. A relation built with rel is unconstrained.

This is designed so that you may at any time switch a function to a relation or vice versa by simply switching modes. Simply having the rel mode should mean it's a pure relation with a logical interpretation, although you may need to check if it's the one intended.

The function mode

A function,

• Only yields one answer.[1]
• Doesn't yield false, i.e. no answer.

The main change in using the function mode is that the conditional itself changes. A function is meant only to receive input parameters and produce output from them, so that even a procedural if-else suffices. It takes the first answer and moves to the body, or if the condition fails move to the else clause.

[1] Note: This is not completely enforced by the Cosmos™ compiler, as of yet. As such, we ask to have some caution when using the function mode. If used incorrectly, it can lead to unsound code.

Mixing functions with relations

Having a main function as the entry point to your program is often beneficial.

rel multiple(x,y)
	y=x or multiple(x+x,y)

rel odd(x)
	x%1=0

function main()
	print('type a number')
	io.write('> ')
	io.read(x)
	if(multiple(x,y) and odd(y))
		io.write('An odd multiple of '+x+'is: ')
		io.write(y)
main()

A program typically should not fail or return multiple results. This is ensured by having main as the entry point.

Because it is inside a function, the conditional will pick only one answer for the program.

Regardless, multiple and odd are relations. There may be many odd multiples of a given number. As such, the program exhibits relational behavior.

The function main picks the first number that's an odd multiple of x.

It's thus perfectly possible to have a program that mixes functions and relations.