Return to Answer

where x and y are runtime values used as unit 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.

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.

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 ∈ PositiveInt | i < |xs| }.
As you can deduce from the i ∈ PositiveInt clause, this is a strict subtype of PositiveInt.

List a = enum
    Cons: a -> List a -> List a
    Empty: List a

length: List a -> PositiveInt
length l = f l 0 where
    f (Cons _ xs) n = f xs (n + 1)
    f Empty n = n

Index (xs: List a) = (i: PositiveInt) 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 -> PositiveInt has not a descriptive enough type.
Indeed: length's correct type is (Empty -> 0) & (Cons -> PositiveInt), 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.

let n: Int = userInput in
get xs n

is not a valid programme, for Int is a supertype of { i ∈ Int | i < |xs| }, meaning explicit type narrowing has to be involved:

let n: Int = userInput in
if n < |xs| then
    get xs n
else
    //deal with error

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 ℕ.

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.

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

MinMax = ∀a. Comparable a => (x: a) -> (y: a) -> (x | y)

max: MinMax
max x y = x > y then x else y

min: MinMax
min x y = x > y then y else x

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