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

Когда представлен следующий код:

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'

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

Источник

2 ответа

Решение

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

Я переписал этот код несколькими другими способами, но не могу заставить Idris распознать его как полный,

Я подумал, что вас может заинтересовать обходной путь. Если вы вручную встроены 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,

Источник

Проблема в том, что Идрис не может этого знать 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 естественно, может быть длина списка ввода.

Источник
Другие вопросы по тегам