Murat Kasimov

More about me

Я language (β)

/Я language (β)/Snippets/Initialising data-structures/

Term initialising usually refers to languages with manual memory management, but here it's used in context of definig it standalone.

For some emptiable primitives it's possible to define, well... empty ones:

> empty = Same `hv'he` Empty : Maybe i > empty = List `hv'he` Empty : List i

The easiest way to define a singletone is to use a special Kleisli morphism:

> intro `hv'he` A = Exist `hv'he` A : Maybe i > intro `hv'he` A = Build `ha` Fixed `ha` T'TT'I `ha` Along `ha__` Empty `lo` A `hv__` Unit : Nonempty List i

If you want to define some datastructure expression with many elements, you can use Limit Objective:

> empty @Maybe `lu` B Unit `yi` Exist `lu` A Unit `yi` Build : Nonempty List Latin

Another approach is to add elements using push morphism:

> empty `yi` push `hv'he` B `ho` that `yi` push `hv'he` A `ho` that : List Latin

But the easiest way is to use literal package:

> [ A , B , C , D , E ] : List Latin > [ A , B , C , D , E ] : Nonempty List Latin