Built-in Types
We can use the check statement to make assertion about an expression's type.
Don't forget that code blocks on our website are interactive, hovering over them to see a menu button.
We use double-quoted String.
We can use the let statement to do assignment.
We can use the compute statement to compute the value of a expression.
Trivial is a Type, and sole is its only element.
let can be nested in { ...; return ... }.
Pair taken two Types, is a Type.
We can use cons to construct Pair.
And using car to get a Pair's first element, using cdr to get a Pair's second element.
Yes, that's Lisp's DNA, dancing in our cells.
Thanks, John McCarthy (1927 - 2011).
We use Both as another name of Pair, because we read Pair(A, C) as
The following two expressions are the same Type.
We can write nested Pair.
We write sigma type as exists (x: A) C, where x might occur in C, or say, C depends on x.
This is why sigma type is also called dependent pair type.
We read exists (x: A) C as
There exists x in A, such that C is true.
For Pair the second type is fixed, while for sigma type, when the first expression is different, the second type can change,
Pair is actually a special form of sigma type. The following two types are the same.
We can use same_as_chart to assert that many expressions of a given type are the same.
We write function type as (A) -> R, where A is the argument type, and R is the return type.
We use (x) => ... to construct anonymous function, which is also famously called lambda.
When using the let statement, we can give a type.
We can also use function to define a function.
We write pi type as (x: A) -> R, just like function type, A is the argument type, and R is the return type, but this time, x might occur in R, or say, R depends on x.
This is why pi type is also called dependent function type.
Another way of writing (x: A) -> R is forall (x: A) R.
And we read it forall (x: A) R as
For all x in A, R is true.
For function type the return type is fixed, while for pi type, when the argument expression is different, the return type can change.
The return type of the above pi type is (T) -> T, it depends on the argument expression T.
We have a built-in function of the above type, and we call this function the.
It is defined as the following:
Absurd is a very special Type, because it has no elements.
We have a built-in function called from_falsehood_anything,
If you have a element of type Absurd, you can use it to prove anything.
When we want to express a proposition is not true, we say that proposition leads to absurd.
Given a Type, and two expressions of that Type, we can create a new Type to express the two expressions are the same.
We can use the_same to construct elements of this type.
If we want to omit the first argument, we can use same.
If we want to omit all arguments, we can use refl, which means "reflection".
We can omit all arguments, because after all, all the informations are already in the type.
If the two elements are actually not the same, we can still use Equal to create a Type, but we will not be able to construct any elements of this type.
By the way, we use // ... to write comments in code, just like the two lines above.
Above are all the built-in types of cicada language!
Beside them, we will use datatype and class to construct new compound types.
But before that, let's see how to view a file as a module, and use import to import published works.