Могу ли я использовать нормальную форму значения, чтобы избежать неполных совпадений с образцом в Agda?
В следующей программе Agda я получаю предупреждение об отсутствующем падеже в определении one, несмотря на то, что myList подходит только к cons падежу.
open import Data.Nat
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))
one : ℕ
one with myList
... | (cons x xs) = x
Incomplete pattern matching for .test.with-16. Missing
cases:
one | nil
Я знаю, что это звучит немного запутанно, но есть ли способ определить one с точки зрения myList, не сталкиваясь с ошибками «неполного сопоставления с образцом»?
Этот пример является упрощением моей исходной задачи, взятой из домашнего задания и использующей несколько более сложные типы. В этом случае "myList" — это большое значение, вычисленное умной функцией на основе небольших входных данных. Если я вычислю нормальную форму "myList", используя режим Agda Emacs (C-c C-n), я смогу взять из него значение "one" и вставить его в свою программу. Однако при выводе это значение занимает десятки строк, поэтому я размышлял, есть ли способ напрямую определить "one" в терминах "myList", не сталкиваясь с ошибкой неполного сопоставления с образцом.
Ответы 2
Если вы используете with e, то e абстрагируется (представьте себе лямбда-абстракцию) от цели и контекста, и вас просят продолжить, как если бы у вас была переменная вместо самой e. Таким образом, следующее сопоставление с образцом вообще не учитывает значение myList (что довольно нелогично, но это просто синтаксический сахар для создания вспомогательного определения с одним дополнительным аргументом).
Однако вы можете написать следующее:
open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
myList : List ℕ
myList = 1 ∷ 2 ∷ 3 ∷ []
head : {n : ℕ} {ns : List ℕ} (xs : List ℕ) → n ∷ ns ≡ xs → ℕ
head (x ∷ xs) refl = x
one : ℕ
one = head myList refl
Вы также можете посмотреть шаблон inspect в стандартной библиотеке для более общего решения этой проблемы.
могут быть различия, потому что myList теперь просматривается во время проверки типа, чтобы убедиться, что это _∷_, и извлечь две части при проверке типа определения one
Вы можете отразить значение на уровне типа, а затем сопоставить его с образцом. Выглядит так:
open import Data.Nat
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))
data Sing {α} {A : Set α} : A -> Set where
sing : ∀ x -> Sing x
one : ℕ
one with sing myList
... | sing (cons x (cons _ (cons _ nil))) = x
Эта версия отлично сработала с моей первоначальной проблемой (оценщик лямбда-исчисления)! У вас есть какие-либо идеи, почему это решение было более эффективным, чем решение «refl», предложенное Сайзаном?
@hugomg, извините, не знаю, почему решение refl неэффективно. Я предлагаю попробовать спросить в списке рассылки Agda. Это может оказаться сообщением об ошибке.
Кажется, это помогает! Но знаете ли вы, есть ли разница в производительности между вычислениями
xэтим способом и использованием обычной формы (C-c C-n в Emacs)? В моем более крупном примере нормальная форма может быть вычислена очень быстро, но эта «проверочная» версия потребляет гигабайты ОЗУ и быстро начинает подкачку.