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.
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.
-- 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.
--- 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.
In the case of lexers and parsers, you could do that, or you could decide that a lexer could work on a potentially infinite stream and works with (lazy) infinite but productive structures.