WIP: type annotations docs

README.md

@@ -232,59 +232,8 @@ code.  While at many places the types can be inferred there are
 places, especially in user-defined functions, where we can not guess
 the correct type (we can only infer what we see during runtime).
 
-Users can annotate their `defun` definitions like this:
-
-``` emacs-lisp
-;; (elsa-pluralize :: String -> Int -> String)
-(defun elsa-pluralize (word n)
-  "Return singular or plural of WORD based on N."
-  (if (= n 1)
-      word
-    (concat word "s")))
-```
-
-The `(elsa-pluralise :: ...)` inside a comment form provides
-additional information to the Elsa analysis.  Here we say that the
-function following such a comment takes two arguments, string and int,
-and returns a string.
-
-The syntax of the type annotation is somewhat modeled after Haskell
-but there are some special constructs available to Elsa
-
-Here are general guidelines on how the types are constructed.
-
-- For built-in types with test predicates, drop the `p` or `-p` suffix and PascalCase to get the type:
-    - `stringp` → `String`
-    - `integerp` → `Integer` (`Int` is also accepted)
-    - `markerp` → `Marker`
-    - `hash-table-p` → `HashTable`
-- A type for everything is called `Mixed`.  It accepts anything and is
-  always nullable.  This is the default type for when we lack type
-  information.
-- Sum types can be specified with `|` syntax, so `String | Integer` is
-  a type accepting both strings or integers.
-- Cons types are specified by prefixing wrapping the `car` and `cdr`
-  types with a `Cons` constructor, so `Cons Int Int` is a type where
-  the `car` is an int and `cdr` is also an int, for example `(1 . 3)`.
-- List types are specified by wrapping a type in a vector `[]`
-  constructor, so `[Int]` is a list of integers and `[String | Int]`
-  is a list of items where each item is either a string or an integer.
-  A type constructor `List` is also supported.
-- Function types are created by separating argument types and the
-  return type with `->` token.
-- To make variadic types (for the `&rest` keyword) add three dots
-  `...` after the type, so `String... -> String` is a function taking
-  any number of strings and returning a string, such as `concat`.
-  Note: a variadic type is internally just a list of the same base
-  type but it has a flag that allows the function be of variable
-  arity.  A `Variadic` type constructor is also available to construct
-  complex types.
-- To mark type as nullable you can attach `?` to the end of it, so
-  that `Int?` accepts any integer and also a `nil`.  A `Maybe` type
-  constructor is also available to construct complex types.
-
-Some type constructors have optional arguments, for example writing
-just `Cons` will assume the `car` and `cdr` are of type `Mixed`.
+Read the type annotations [documentation](./docs/type-annotations.org)
+for more information on how to write your own types.
 
 # How can I contribute to this project
 

docs/type-annotations.org

@@ -0,0 +1,238 @@
+* Type annotations
+
+In Elisp users are not required to provide type annotations to their
+code.  While at many places the types can be inferred there are
+places, especially in user-defined functions, where we can not infer
+the correct type.
+
+Therefore Elsa provides users with the option to annotate their
+function definitions.  The annotations are placed in the body of the
+function inside a =declare= form:
+
+#+BEGIN_SRC elisp
+(defun add-one (x)
+  (declare (elsa (int) int))
+  (1+ x))
+#+END_SRC
+
+The =declare= form starts with =elsa= followed by one or two values.  If
+two are provided, first must be a list which is the list of input
+types and the second is the return type.
+
+If only one is provided it is taken to be the return type and the
+function must have no input arguments.
+
+Here are general guidelines on how the types are constructed.
+
+** Built-in types
+
+For built-in types with test predicates, drop the =p= or =-p= suffix to
+get the type:
+
+- =stringp= → =string=
+- =integerp= → =integer= (=int= is also accepted)
+- =markerp= → =marker=
+- =hash-table-p= → =hash-table=
+
+Some additional special types:
+
+- =t= stands for =t= and is always true
+- =nil= stands for =nil= and is always false
+- =bool= is a combination of explicitly =t= or =nil=
+
+** Nullable types
+
+By default types do not accept =nil= values.  This helps preventing
+errors where you would pass =nil= to a function expecting a value.  To
+mark a type nullable you can combine it with =nil= type using the [[id:5a21a68a-4df1-4d44-a854-1d9700858a1a][or]]
+combinator: =(or string nil)= is a type which takes any string but also
+=nil=.
+
+** Most general type
+
+A type for everything is called =mixed=.  It accepts anything and is
+always nullable (that means it accepts =nil=).  This is the default type
+for when we lack type information.
+
+Because a =mixed= type can be anything it itself is only accepted by
+=mixed=, so that the following would not type-check:
+
+#+BEGIN_SRC elisp
+(defun a-goes-in (a) ;; a is mixed
+  (declare (elsa (mixed) int))
+  ;; a *might* be an int, but we don't know for sure
+  (1+ a))
+#+END_SRC
+
+** Composite (higher order) types
+
+Composite or higher-order types are types which take other types as
+arguments.
+
+Composite types usually correspond to data constructors such as =cons=,
+=list=, =vector=...
+
+- =(cons a b)= where =a= is the type of =car= and =b= is the type of =cdr=.  If
+  the =car= and =cdr= can be anything write =(cons mixed mixed)= or simply
+  =cons= for short.
+- =(list a)= where =a= is the type of items in the list.  If the list can
+  hold anything, write =(list mixed)= or simply =list= for short.
+- =(vector a)= where =a= is the type of items in the vector.  If the
+  vector can hold anything, write =(vector mixed)= or simply =vector= for
+  short.
+- =(hash-table k v)= where =k= is the key type and =v= is the value type.
+  If the hash table can hold anything, write =(hash-table mixed mixed)=
+  or simply =hash-table= for short.
+
+** Constant types
+
+A constant type always holds a specific value.  Functions often take
+flags which can be symbols such as ='append= or ='prepend= or constant
+strings.
+
+To specify a constant type wrap the value in a =(const)= constructor, so
+that:
+
+- =(const a)= is the symbol =a= (when used in a lisp program you would
+  pass it around as ='a=),
+- =(const 1)= is the integer =1=,
+- =(const "foo")= is the string ="foo"=.
+
+** Function types
+
+Function types are types of functions.  They have input argument types
+and a return type.
+
+The function =add-one= from the introduction has a function type =(function
+(int) int)= which means it takes in one integer and returns an integer.
+
+A =lambda= form =(lambda (x) (number-to-string x))= has function type
+=(function (number) string)=, it takes in a number and returns a string.
+
+A function can have a function type as one of its input types.  An
+example of such a function is =mapcar= which takes a function and a list
+and applies the function to every item of the list.
+
+#+BEGIN_SRC elisp
+(defun app (fn)
+  "Apply FN to the list (1 2 3 4)"
+  (declare (elsa ((function (number) number)) (list number)))
+  (mapcar fn (list 1 2 3 4)))
+
+(app (lambda (x) (* x x)))
+#+END_SRC
+
+The =app= function requires that we pass in a function which processes a
+number into a number and returns a list of numbers.
+
+** TODO Generic types
+
+Generic types are types where some of the type arguments are variable.
+Both basic and composite types can be turned into generic types.
+
+*** Motivation
+
+An example of a generic function is =identity=.  This function takes
+anything in and anything out.  We could therefore give it a type
+annotation =(elsa (mixed) mixed)=.
+
+However, we can do better!  We know that whatever was passed in will
+be returned and so the type actually must be the same.  The =(elsa
+(mixed) mixed)= signature allows us to pass in an =int= and it can return
+back a =string= no problem and so it would not catch a huge number of
+possible errors.
+
+What we want to express here is "X comes in, X comes out".
+
+*** Syntax
+
+The syntax for generic types is "generic type name" + =*= suffix.  Any
+string can be used for the generic type name, but customarily
+single-letter names are used.
+
+For the above mentioned identity function we therefore write the type
+as =(elsa (a*) a*)= where =a*= stands for a generic type =a=.
+
+A function such as =car= can be typed as follows:
+
+#+BEGIN_SRC elisp
+(elsa ((cons a* b*)) a*)
+#+END_SRC
+
+It takes a cons with =a= in the =car= and =b= in the =cdr= and return the =car=
+which is of type =a= , whatever that happens to be.
+
+** Optional types
+
+If a function can take optional arguments we need to convert them into
+a nullable type =(or type nil)=.
+
+#+BEGIN_SRC elisp
+(defun drop-items (list &optional n)
+  "Drop first item of LIST or N items if N is provided."
+  (declare (elsa ((list a*) (or int nil)) (list a*)))
+  (setq n (or n 1))
+  (dotimes (_ n list)
+    (setq list (cdr list))))
+#+END_SRC
+
+** Variadic types
+
+If a function can take arbitrary number of arguments we preceed the
+last variadic argument with =&rest= marker just as we do in the argument
+list.
+
+#+BEGIN_SRC elisp
+(defun join (separator &rest strings)
+  "Join STRINGS with SEPARATOR."
+  (declare (elsa (string &rest string) string))
+  (mapconcat 'identity strings separator))
+#+END_SRC
+
+** Type combinators
+*** Sum types
+:PROPERTIES:
+:ID:       5a21a68a-4df1-4d44-a854-1d9700858a1a
+:END:
+
+Sum types can be specified as a list form starting with =or=, so =(or
+string int)= is a type accepting strings or integers.
+
+A sum type is useful if the function internally checks the passed
+value and decides what processing to do:
+
+#+BEGIN_SRC elisp
+(defun to-number (x)
+  (declare (elsa ((or int string)) int))
+  (cond
+   ((numberp x) x)
+   ((stringp x) (string-to-number x))))
+#+END_SRC
+
+*** Intersection types
+
+Intersection types can be specified as list form starting with =and=, so
+=(and string float)= is a type which is at the same time string and
+float (such a type has empty domain, nothing can be string and float
+at the same time).  Intersection types are used to track impossible
+assignments.
+
+#+BEGIN_SRC elisp
+;; Such a condition can never evaluate to true
+(if (and (stringp x) (integerp x))
+    "X is both string and int which is impossible, this branch never executes"
+  "This branch always executes")
+#+END_SRC
+
+*** Difference types
+
+Difference types can be specified as list form starting with =diff= so =(diff
+mixed string)= is a type which can be anything except a string.
+
+Difference types are useful in narrowing the possible values of variables after conditional checks.
+
+#+BEGIN_SRC elisp
+(if (stringp x)
+    "X is definitely string here"
+  "X is anything but string here")
+#+END_SRC

elsa-analyser.el

@@ -11,7 +11,7 @@
 
 (require 'elsa-typed-builtin)
 
-;; (elsa--arglist-to-arity :: List Symbol | T | String -> Cons Int (Int | Symbol))
+;; (elsa--arglist-to-arity :: (function ((or (list symbol) t string)) (cons int (or int symbol))))
 (defun elsa--arglist-to-arity (arglist)
   "Return minimal and maximal number of arguments ARGLIST supports.
 
@@ -39,7 +39,7 @@ number by symbol 'many."
         (setq max 'many))
       (cons min max)))))
 
-;; (elsa-fn-arity :: Symbol -> Cons Int (Int | Symbol))
+;; (elsa-fn-arity :: (function (symbol) (cons int (or int symbol))))
 (defun elsa-fn-arity (fn)
   (elsa--arglist-to-arity (help-function-arglist fn)))
 
@@ -55,12 +55,12 @@ number by symbol 'many."
 (defun elsa--analyse-symbol (form scope _state)
   (let* ((name (oref form name))
          (type (cond
-                ((eq name t) (elsa-make-type T))
-                ((eq name nil) (elsa-make-type Nil))
+                ((eq name t) (elsa-make-type t))
+                ((eq name nil) (elsa-make-type nil))
                 ((-when-let (var (elsa-scope-get-var scope form))
                    (clone (oref var type))))
                 ((get name 'elsa-type-var))
-                (t (elsa-make-type Unbound)))))
+                (t (elsa-make-type unbound)))))
     (oset form type type)
     (unless (memq name '(t nil))
       (oset form narrow-types
@@ -395,9 +395,9 @@ collects all the arguments, turns &optional arguments into
 nullables and the &rest argument into a variadic."
   (-let (((min . max) (elsa--arglist-to-arity args)))
     (if (eq max 'many)
-        (-snoc (-repeat min (elsa-make-type Mixed))
-               (elsa-make-type Variadic Mixed))
-      (-repeat max (elsa-make-type Mixed)))))
+        (-snoc (-repeat min (elsa-make-type mixed))
+               (elsa-make-type &rest mixed))
+      (-repeat max (elsa-make-type mixed)))))
 
 (defun elsa--analyse-defun-like-form (name args body form scope state)
   (let* (;; TODO: there should be an api for `(get name
@@ -462,7 +462,7 @@ make it explicit and precise."
           (progn
             (elsa--analyse-form value scope state)
             (put var-name 'elsa-type-var (oref value type)))
-        (put var-name 'elsa-type-var (elsa-make-type Unbound))))))
+        (put var-name 'elsa-type-var (elsa-make-type unbound))))))
 
 (defun elsa--analyse:defcustom (form scope state)
   "Analyze `defcustom'.
@@ -481,7 +481,7 @@ automatically deriving the type."
             ;; TODO: check the `:type' form here and also compare if we
             ;; are doing a valid assignment.
             (put var-name 'elsa-type-var (oref value type)))
-        (put var-name 'elsa-type-var (elsa-make-type Unbound))))))
+        (put var-name 'elsa-type-var (elsa-make-type unbound))))))
 
 (defun elsa--analyse:defconst (form scope state)
   "Analyze `defconst'.
@@ -503,7 +503,7 @@ If no type annotation is provided, find the value type through
          (body (nthcdr 2 sequence))
          ;; TODO: this should use `elsa--get-default-function-types'
          (arg-types (-repeat (length (elsa-form-sequence args))
-                             (elsa-make-type Mixed)))
+                             (elsa-make-type mixed)))
          (vars))
     (when (elsa-form-list-p args)
       (-each-indexed (elsa-form-sequence args)
@@ -580,7 +580,7 @@ If no type annotation is provided, find the value type through
        (not (oref arg quote-type))
        (elsa-get-name arg)))
 
-;; (elsa--analyse-normalize-spec :: Bool | List Bool -> Mixed -> List Bool)
+;; (elsa--analyse-normalize-spec :: (function ((or bool (list bool)) mixed) (list bool)))
 (defun elsa--analyse-normalize-spec (spec form)
   "Normalize evaluation SPEC for FORM."
   (cond
@@ -595,7 +595,7 @@ If no type annotation is provided, find the value type through
                       t)))
    (t spec)))
 
-;; (elsa--analyse-macro :: Mixed -> Bool | List Bool -> Mixed -> Mixed -> Mixed)
+;; (elsa--analyse-macro :: (function (mixed (or bool (or list bool)) mixed mixed) mixed))
 (defun elsa--analyse-macro (form spec scope state)
   (setq spec (elsa--analyse-normalize-spec spec form))
   (let* ((head (elsa-car form))

elsa-check.el

@@ -1,4 +1,4 @@
-;; (elsa-checks :: [Mixed])
+;; (elsa-checks :: (list mixed))
 (defvar elsa-checks nil)
 
 (defun elsa-check-add (check)