stepancheg/smaller.md

## smaller.md

      
    Raw
  

              smaller.md
            
          
    The problem

Idris termination detection on values to be structurally smaller when calling function recursively. For example in this case the compiler understands that xs is smaller than x :: xs:
foo : List a -> ()
foo (x :: xs) = foo xs
foo [] = ()

However, when value is passed to recursive call is produced by another function, the compiler does not understand it. Consider this very inefficient reverse implementation:
total
removeLast2 : (xs : List a) -> NonEmpty xs -> (List a, a)
removeLast2 (x :: y :: xs) _ =
    let (withoutLast, last) = removeLast2 (y :: xs) IsNonEmpty in
    (x :: withoutLast, last)
removeLast2 (x :: []) _ = ([], x)

total
reverse2 : List Nat -> List Nat
reverse2 [] = []
reverse2 (x :: xs) =
    let (withoutLast, last) = (removeLast2 (x :: xs) IsNonEmpty) in
    last :: reverse2 withoutLast

When typechecking this code the compiler produces error:
Error: reverse2 is not total, possibly not terminating due to recursive
path Aa.reverse2 -> Aa.reverse2 -> Aa.reverse2

Aa.idr:45:1--46:32
 45 | total
 46 | reverse2 : List Nat -> List Nat

withoutLast returned from removeLast2 is smaller than x :: xs  passed to removeLast2, thus when passed to reverse2 function terminates, but the compiler does not understand that.
This problem in real life

Suppose we want to write a lexer. The obvious way to write it is this:
-- parse one token; return the rest of the input
oneToken : (input : List Char) -> NonEmpty -> (Token, List Char)
...

tokens : List Char -> List Token
tokens [] = []
tokens xs =
  let (token, rem) = token xs IsNotEmpty in
  token :: tokens rem

To make it work we need to tell the compiler the list returned by oneToken is smaller than the input list. AFAIU there's no way to tell the compiler that.
The proposal: Smaller builtin and check_smaller statement

-- This is a builtin type, cannot be instantiated directly
data Smaller : (x : a) -> (y : a) -> Type where

-- This is a STATEMENT, not a function.
-- It can be called only if compiler can prove
-- that `x` is smaller than `y`.
-- It returns `Smaller` object.
check_smaller : (x : a) -> (y : a) -> Smaller x y

Finally, when compiler typechecks recursive call, it looks up for Smaller objects in the context. If it finds some, it can use it to confirm the termination.
Examples of check_small

--- This should obviously work
check_smaller [] (x :: xs)

-- Utility function
smallerPrependElement : {x, y : a}
    -> {xs, ys : List a}
    -> Smaller xs ys
    -> Smaller (x :: xs) (y :: ys)
smallerPrependElement {x, y, xs, ys} xsSmallerYs =
    -- Here the compiler understands that prepending
    -- one element to `xs` which is smaller than `ys`
    -- makes `x :: xs` smaller than `y :: ys`
    check_smaller (x :: xs) (y :: ys)

And finally our original problem can be written this way:
total
removeLast : (xs : List a)
    -> NonEmpty xs
    -> ((l ** Smaller l xs), a)
removeLast (x :: y :: xs) _ =
    let ((withoutLast ** withoutLastSmallerYXs), last)
        = removeLast (y :: xs) IsNonEmpty in
    (
        (x :: withoutLast ** smallerPrependElement withoutLastSmallerYXs),
        last
    )
removeLast (x :: []) _ = (([] ** check_smaller [] [x]), x)

total
reverse1 : List Nat -> List Nat
reverse1 [] = []
reverse1 (x :: xs) =
    let ((withoutLast ** smaller), last) = (removeLast (x :: xs) IsNonEmpty) in
    last :: reverse1 withoutLast

reverse1 function has smaller object in scope. The type of the object is Smaller withoutLast (x :: xs), which is used for the termination proof of reverse1.