Is this recursive function not total, or is the compiler just unable to prove it? How to rewrite it as total?
When presented with the following code:
module TotalityOrWhat %default total data Instruction = Jump Nat | Return Char | Error parse : List Char -> Instruction parse ('j' :: '1' :: _) = Jump 1 parse ('j' :: '2' :: _) = Jump 2 parse ('j' :: '3' :: _) = Jump 3 parse ('r' :: x :: _) = Return x parse _ = Error parseDriver : String -> Maybe Char parseDriver = parseDriver' . unpack where parseDriver' : List Char -> Maybe Char parseDriver' xs = case parse xs of (Jump j) => parseDriver' $ drop j xs (Return x) => Just x Error => Nothing
Idris gives an error:
TotalityOrWhat.idr:17:3: TotalityOrWhat.parseDriver, parseDriver' is possibly not total due to recursive path TotalityOrWhat.parseDriver, parseDriver' --> TotalityOrWhat.parseDriver, parseDriver' TotalityOrWhat.idr:15:1: TotalityOrWhat.parseDriver is possibly not total due to: TotalityOrWhat.parseDriver, parseDriver'
I have re-written this code in several other ways but cannot get Idris to recognize it as total. Am I wrong about it being total, or is Idris just not able to determine that it is? If it is total in essence, how can I rewrite it so Idris will recognize it as total?Автор: Keith Pinson Источник Размещён: 08.11.2019 11:32
This is not an answer to "why isn't it recognized as total" and not even really an answer to "how do I change it to be recognized as total", but since you mentioned
I have re-written this code in several other ways but cannot get Idris to recognize it as total,
I thought you might be interested in a workaround. If you manually inline
parseDriver', you can get it through the totality checker:
total parseDriver : String -> Maybe Char parseDriver = parseDriver' . unpack where parseDriver' : List Char -> Maybe Char parseDriver' ('j' :: '1' :: xs) = parseDriver' ('1' :: xs) parseDriver' ('j' :: '2' :: xs) = parseDriver' xs parseDriver' ('j' :: '3' :: _ :: xs) = parseDriver' xs parseDriver' ('r' :: x :: _) = Just x parseDriver' _ = Nothing
This works because we are always recursing structurally on some suffix of
The problem here is that Idris can't know that
drop j xs produces a strictly smaller list from its input, since
drop's type isn't expressive enough.
So, another ad-hoc approach would be to use a dummy parameter which makes the totality checker accept the function, by using structurally smaller list
xs' while calling
parseDriver : String -> Maybe Char parseDriver s = parseDriver' chars chars where chars : List Char chars = unpack s -- 2nd parameter is a dummy one (to make totality checker happy) parseDriver' : List Char -> List Char -> Maybe Char parseDriver' _  = Nothing parseDriver' xs (_::xs') = case parse xs of Jump j => parseDriver' (drop j xs) xs' Return x => Just x Error => Nothing
We could've also used some natural parameter
n, which we could decrement at each step, making sure we stop at
0. The initial value of
n could naturally be the length of the input list.