Является ли эта рекурсивная функция не полной, или компилятор просто не может это доказать? Как переписать его как итог?

Question

Сталкиваясь со следующим кодом:

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 

Идриса выдает ошибку:

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' 

Я переписал этот код несколько других способов, но не могу получить Идрис признать ее общей. Я ошибаюсь в том, что это тотал, или Идрис просто не может определить, что это такое? Если это по существу, то как я могу переписать его, чтобы Идрис узнал его как итог?

Answer 1

Это не ответ на вопрос «почему он не признается общей» и даже не на самом деле ответ на «как я могу изменить его, чтобы быть признанным в качестве общего», но так как вы упомянули

I have re-written this code in several other ways but cannot get Idris to recognize it as total,

Я думал, вам может быть интересно обходное решение. Если вручную встраивать parse в parseDriver', вы можете получить его через совокупность проверки:

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 

Это работает, потому что мы всегда рекурсии структурно на некотором суффиксом xs.

Answer 2

Проблема заключается в том, что Идрис не может знать, что drop j xs производит строгий список со своего ввода, так как тип drop недостаточно выразителен.

Так, еще одноранговые подхода будет использовать фиктивный параметр, который делает совокупность проверки принимает функцию, используя структурно меньший список xs' при вызове parseDriver' рекурсивно.

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 

Мы могли бы также использоваться некоторый естественный параметр n, который мы могли бы декремента на каждом шагу, убедившись, что мы останавливаемся на 0. Исходным значением n может быть, естественно, длина входного списка.