Why

To keep the purity of S-Exp and readability in LoLi while giving LoLi the power to express complicated types.

How

The idea came from inflection of natural languages, where we have bound morphemes that don’t have meaning by themselves but express the inflectional changes. Therefore, we can adopt the idea into programming languages design, by defining several ‘morpheme’s, we can then perform type-level combinator programming via combining ‘type morpheme’s.

What

As you know from natural languages, we have three different morphemes here:

Prefix

To be satisfied:
```
!pred
```
This prefix goes in front of a predicate, and keeps going only if the predicate returns true.
To negate:
```
~pred
```
Similar to the previous one, this negates the return value of a predicate.

Infix

Has the type:
```
symbol:type
```
symbol has the type type in the current environment.
Composition:
```
f|g
```
This composites f and g, and gives f \circ g.

Suffix

To refine a type:
```
type^pred
type^prop
```
In the former case, type is refined at term level, while in the latter case, type is refined at propositional level.
To be applied to:
```
f@arg
```
This applies the function / type constructor f to the argument.

Some Example

Singleton

(def singleton
    (-> Bool Type)
    (lambda (x)
        (if x Nat (List Nat))))

(def mkSingle
    (-> x:Bool singleton@x)
    (lambda (x)
        (if x 0 nil)))

Refined

(def nthVect
    (-> n:Nat vct:Vect@(m elem)^(< n m))
    ...)