результат с шаблоном не виден

Я пытаюсь понять, как перейти к «безопасно набранному» коду. Например, ниже предполагается вызывать tail только на безопасном пути, т.е. если список на входе непуст. Конечно, был бы простой способ просто сопоставить список с образцом, но идея состоит в том, чтобы согласовать результат функции (null) и ее использование в правой части:

data Void : Set where

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

data Bool : Set where
  True : Bool
  False : Bool

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

null : forall {A} -> List A -> Bool
null nil         = True
null (x :: xs)   = False

non-null : forall {A} -> List A -> Set
non-null nil = Void
non-null (x :: xs) = (x :: xs) == (x :: xs)

tail : forall {A} -> (xs : List A) -> {p : non-null xs} -> List A
tail (_ :: xs) = xs
tail nil      {p = ()}

prove-non-null : forall {A} -> (xs : List A) -> (null xs == False) -> non-null xs
prove-non-null nil         ()
prove-non-null (x :: xs)   refl = refl

compileme : forall {A} -> List A -> List A
compileme xs with null xs
...             | True    = xs
...             | False   = tail xs {prove-non-null xs refl}

В последней строке agda жалуется, что нельзя доказать, что refl относится к типу null xs == False. Почему он не видит, что предложение with только что стало свидетелем того, что null xs является False?

Как правильно это сделать? Как "извлечь" зависимость из вроде бы независимых результатов, типа Bool тип не зависит от списка xs, но в контексте он есть?


agda
person Sassa NF    schedule 01.05.2015    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Речь идет об идиоме inspect. Проверьте исходную ветку и этот вопрос stackoverflow. Текущая версия inspect в стандартной библиотеке: из этой ветки (есть также несколько объяснения).

Если вы удалите определение _==_, вы сможете определить compileme как

open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

...

compileme : forall {A} -> List A -> List A
compileme xs with null xs | inspect null xs
...             | True    | [ _ ] = xs
...             | False   | [ p ] = tail xs {prove-non-null xs p}

Кстати, что означает (x :: xs) == (x :: xs)? Это просто

open import Data.Unit
...
non-null (x :: xs) = ⊤

BTW2, вы можете определить безопасный тип tail, как я определил безопасный тип pred в этом ответе.

person user3237465    schedule 02.05.2015
comment
ну, сначала non-null должен был каким-то образом выражать тип (x :: xs) == ys, если ys не нулевой, но потом я уменьшил требования, отчего это выглядело глупо. - person Sassa NF; 02.05.2015