Dependent Types
A Dependent Type is one whose members can be described by a predicate depending on other values.
In your case, it is Index (xs: List a) = { i ∈ ℕ | i < |xs| }
.
As you can deduce from the i ∈ ℕ
clause, this is a strict subtype of ℕ
.
Here's an example programme description using it:
List a = enum
Cons: a -> List a -> List a
Empty: List a
length: List a -> Natural
length l = f l 0 where
f (Cons _ xs) n = f xs (n + 1)
f Empty n = n
Index (xs: List a) = (i: Natural) when i < length xs
get: (xs: List a) -> Index xs -> a
get (Cons x _) 0 = x
get (Cons _ xs) n = get xs (n - 1)
main = do
let xs = Cons "h" (Cons "42" Empty)
putStrLn (get xs 0) //ok
putStrLn (get xs 5) //Compiler Error
A question that arises then is that of get
"knowing" it will never get Empty
as input, at which point one will notice that length: List a -> ℕ
has not a descriptive enough type.
Indeed: length
's correct type is (Empty -> 0) & (Cons -> ℕ⁺)
, which explicitates the fact that Index Empty
is not a type existing in the Universe.
(At which point one may notice how Cons
/::
relates to NonEmpty a
).
How smart a language and implementation has to be to automatically understand and report on those problems then is the realm of Automated Theorem Proving.
Naturally, when a value is not literal, one has to prove it indeed inhabits the type at hand.
let n: ℕ = userInput in
get xs n
is not a valid programme, for ℕ
is a supertype of { i ∈ ℕ | i < |xs| }
, meaning explicit type narrowing has to be involved:
let n: ℕ = userInput in
if n < |xs| then
get xs n
else
//deal with error
which should be reminiscent of C++'s dynamic_cast
, and is already existing practice (you don't just use unsanitised user input as-is, do you?).
This also relates to the realm of Automatic Type Narrowing as featured in Kotlin, TypeScript, and, less automatic, Ceylon.
An other example is that of Min
and Max
: ∀(a: Comparable). MinMax (x: a, y: a) = { x, y }
, which may be used to describe functions such as
MinMax = ∀a. Comparable a => (x: a) -> (y: a) -> (x | y)
max: MinMax
max x y = if x > y then x else y
min: MinMax
min x y = if x > y then y else x
where x
and y
are runtime values used as singleton types in a union type, where it is guaranteed that for each pair of x
and y
, min
and max
both will return precisely either that x
or that y
, and nothing else.
Naturally the result of min
and max
is a strict subset of a
by virtue of { x ∈ a | f(x) } <: a
.
Languages implementing those include, among others, Idris, Agda, Coq, F*, and ATS.