To keep the purity of S-Exp and readability in LoLi while giving LoLi the power to express complicated types.
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.
As you know from natural languages, we have three different morphemes here:
- To be satisfied:
This prefix goes in front of a predicate, and keeps going only if the predicate returns true.
- To negate:
Similar to the previous one, this negates the return value of a predicate.
- Has the type:
symbolhas the type
typein the current environment.
g, and gives
f \circ g.
- To refine a type:
In the former case,
typeis refined at term level, while in the latter case,
typeis refined at propositional level.
- To be applied to:
This applies the function / type constructor
fto the argument.
(def singleton (-> Bool Type) (lambda (x) (if x Nat (List Nat)))) (def mkSingle (-> x:Bool singleton@x) (lambda (x) (if x 0 nil)))
(def nthVect (-> n:Nat vct:Vect@(m elem)^(< n m)) ...)