| > linear types allow you to express conditions such as this function must not be called with an empty list I don't think that's a particularly enlightening example, mostly because we can implement such a function without any linear or dependent types. Consider that a list (of some element type T) could contain zero Ts, or one T, or two Ts, etc. i.e. List<T> = 1 + T + (T × T) + (T × T × T) + ...
Where:- `1` is a type containing only one value, like 'Unit', 'Null', 'Nil, etc. We use this to represent the empty list. - 'X + Y' is the (tagged) union of types X and Y; AKA a sum type, or an Either - 'X × Y' is the type of tuples containing an X and a Y; AKA a product type, or a Pair Non-empty lists are almost the same, except we don't want to allow the empty list. Hence we need to get rid of the '1' type, to get something like this: NonEmptyList<T> = T + (T × T) + (T × T × T) + ...
Just using the normal rules of arithmetic, we can see that NonEmptyList<T> is the same as List<T>, except everything has been multiplied by T: NonEmptyList<T> = T + (T × T) + (T × T × T) + (T × T × T × T) + ...
= (T × 1) + (T × T) + (T × T × T) + (T × T × T × T) + ...
= T × ( 1 + T + ( T × T) + ( T × T × T) + ...)
= T × List<T>
Hence we can implement NonEmptyList<T> as the type 'T × List<T>', i.e. tuples containing a T and a List<T>. Intuitively, those are the "head" and "tail" of the non-empty list; or equivalently, Cons constructs a tuple, and non-empty lists are those whose outermost constructor is always Cons.Note that we can go the other way too, if our language provided non-empty lists and we want to allow empty ones too: List<T> = 1 + T + (T × T) + (T × T × T) + ...
= 1 + NonEmptyList<T>
This time, we a value of type List<T> is either a unit value (representing the empty list), or a non-empty list. This pattern of "adding one" to a type is usually called 'Maybe' or 'Option': Maybe<T> = 1 + T
Hence simplifying the above to: List<T> = Maybe<NonEmptyList<T>>
|