Narrowing examples

For loops and array length

Narrowing in recursive continuations should be sufficient to know that the array field access is safe.

let sum a =
  let s = ref 0 in
  for i = 0 to Array.length - 1 do
    s := a.(i) + !s
  done;
  !s

Loop invariants

type t = A of int * int | B

let stuff a =
  let s = ref (A (a, a)) in
  for i = 0 to a do
    match !s with
    | B -> assert false
    | A (x, y) ->
      let n = x + y in
      s := A (n, n)
  done;
  !s

In that case narrowing is sufficient to know that we are in the tuple (A) case of s.

Note that it would not be the case for this one:

let stuff a =
  let s = ref (A (a, a)) in
  for i = 0 to a do
    match !s with
    | B -> assert false
    | A (x, y) ->
      let n = x + y in
      if Random.bool () then
        s := A (n, n)
  done;
  !s

Seq (ncourant)

external (+) : int -> int -> int = "%addint"
external ( * ) : int -> int -> int = "%mulint"
external (>) : 'a -> 'a -> bool = "%greaterthan"

module Seq = struct
  type ('a, 's) node = Empty of unit | Cons of 'a * 's
  type _ t = State : ('s * ('s -> ('a, 's) node)) -> 'a t

  let[@inline] fold_left f acc (State (s, next)) =
    let[@inline][@loop always] rec aux acc s =
      match (next[@inlined hint]) s with
      | Empty _ -> acc
      | Cons (x, s') -> aux (f acc x) s'
    in
    aux acc s

  let[@inline] map f (State (s, next)) =
    State (s, fun s ->
      match (next[@inlined hint]) s with
      | Empty _ -> Empty ()
      | Cons (x, s') -> Cons (f x, s'))

  let[@inline] mapi f (State (s, next)) =
    State ((s, 0), fun (s, i) ->
      match (next[@inlined hint]) s with
      | Empty _ -> Empty ()
      | Cons (x, s') -> Cons (f i x, (s', i + 1)))

  let[@inline] filter f (State (s, next)) =
    let[@inline][@loop always] rec aux s =
      match (next[@inlined hint]) s with
      | Empty _ -> Empty ()
      | Cons (x, s') ->
        if f x then Cons (x, s') else aux s'
    in
    State (s, aux)

  let[@inline] unfold f acc =
    State (acc, f)

end

let[@inline] square x = x * x

let[@inline] ints lo hi =
  Seq.unfold (fun i -> if i > hi then Seq.Empty () else Seq.Cons (i, i + 1)) lo

let[@inline] sum s =
  Seq.fold_left (+) 0 s

let foo () =
  sum (Seq.map square (Seq.filter (fun i -> i > 5) (ints 0 11)))

let bar () =
  sum (Seq.mapi (fun[@inline] i x -> i * x) (ints 0 11))

Currently, with -O3, foo does not contain any allocations, but bar does.