Narrowing

A common pattern in lisp is using predicates to handle a value differently based on its runtime type.

(et-defun my-repeat (repeat: Integer obj: Integer|String) String
  (if (stringp obj)
      (s-repeat repeat obj)
    (make-string repeat obj)))

Within the then branch of the if-statement, we want the type of obj to be narrowed to just String, and likewise to just Integer in the else branch.
To solve this, we introduce narrow-binding. Narrow-binds allow a type to contain internal information about variables in scope.

(stringp obj)
;; >> True{obj : String} | Nil{obj : Integer}

This type describes that when it is true, obj has type String, and when it is nil, obj has type Integer. Utilizing this, conditional macros such as if can type-check each branch with the correct narrowed variable types.
In order for this to work, the type returned by a variable must not only contain the type of the value, but also encode that the type represents the value currently stored in obj.

obj
;; >> Integer|String {= obj}

This type describes that it is an Integer or String, and also that whatever value it holds is equal to the value stored in the variable obj. This allows for narrowing not just on predicate outputs, but on variables themselves:

(et-defun my-negative (val: Number?) Number
  (if val
      ;; val narrowed to Number
      (- val)
    ;; val narrowed to Nil
    0))

Defining predicate functions

To define a function which narrows an argument, the value being narrowed must be assigned to a generic type parameter. Then, the is? type operation can be used in the return:

(et-defun my-stringp (s: [S]) (is? S String)
  (stringp s))

Then, suppose you type-check the expression

(stringp obj)

As discussed, obj will evaluate to the type String|Integer {= obj}. When type-checking the call to my-stringp, this type will get assigned to S. The is? type-utility then does the following conversion:

(is? String|Integer{=obj} String)
-> True{obj : String} | Nil{obj : Integer}

Now, consider the behavior of a not-like function:

(et-defun my-not (bool: [T]) (is? T Nil)
  (not bool))

If we evaluate (my-not (my-stringp obj)), then we will get the conversion

(is? {True{obj : String} | Nil{obj : Integer}} Nil)
-> True{obj : Integer} | Nil{obj: String}

This is exactly the behavior we would want out of this expression, and we get it nearly for free.

Additional narrowing operations

Not all predicates exhaustively classify an entire type. For example, evenp returns t only for integers, but not for all integers. For predicates like this, use the is-a? operation.

(et-defun my-evenp (val: [T]) (is-a? T Integer)
  (and (integerp val) (evenp val)))

Then, if we evaluate (my-evenp obj), we get the following conversion

(is-a? String|Integer{= obj} Integer)
-> True{obj : Integer} | Nil{obj: String|Integer}

If (my-evenp obj) returns t, the typesystem can conclude that its input was definitely an integer, but if it returns nil, it cannot make a similar conclusion in the reverse direction.

The isnt? operation is the opposite of is?.

(et-defun my-atom (val: [T]) (isnt? T &Cons<Any_Any>)
  (atom val))