index.hs

index :: l <: [a] - ([]) -> i <: { n <- Int | n < length l; n >= 0 } -> { -- notice the shortcutting,
                                                      -- using the l type as an argument to length instead
                                                      -- of having to bind l to a name as a foreach.
  case (l, i) of -- similar shortcutting
    (x:xs, 0) = x
    (x:xs, n) = index xs (n - 1)
}