Строго позитивно в Агде

Я пытаюсь закодировать некоторую денотационную семантику в Agda на основе программы, которую я написал на Haskell.

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

В Agda прямой перевод будет таким:

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ℕ -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

но я получаю сообщение об ошибке, относящееся к FunVal, потому что;

Значение не является строго положительным, поскольку оно встречается слева от стрелки в типе конструктора FunVal в определении Value.

Что это значит? Могу я закодировать это в Agda? Я ошибаюсь?

Спасибо.


types haskell semantics interpreter agda
person Jason Reich    schedule 06.04.2010    source источник
comment
Возможно, вас заинтересует PHOAS, объяснил Chlipala здесь.   -  person danr    schedule 10.02.2012
comment
Спасибо. С тех пор я немного поигрался с этим.   -  person Jason Reich    schedule 22.02.2012

Ответы (1)


arrow_upward
35
arrow_downward

HOAS не работает в Agda по следующим причинам:

apply : Value -> Value -> Value
apply (FunVal f) x = f x
apply _ x = Error "Applying non-function"

w : Value
w = FunVal (\x -> apply x x)

Теперь обратите внимание, что оценка apply w w снова возвращает вам apply w w. Термин apply w w не имеет нормальной формы, которая в агда запрещена. Используя эту идею и тип:

data P : Set where
    MkP : (P -> Set) -> P

Получаем противоречие.

Один из выходов из этих парадоксов - разрешить только строго положительные рекурсивные типы, что и выбрали Agda и Coq. Это означает, что если вы объявите:

data X : Set where
    MkX : F X -> X

Этот F должен быть строго положительным функтором, а это означает, что X никогда не может находиться слева от какой-либо стрелки. Итак, эти типы строго положительны в X:

X * X
Nat -> X
X * (Nat -> X)

Но это не так:

X -> Bool
(X -> Nat) -> Nat  -- this one is "positive", but not strictly
(X * Nat) -> X

Короче говоря, вы не можете представить свой тип данных в Agda. Вы можете использовать кодировку де Брейна, чтобы получить тип термина, с которым вы можете работать, но обычно для функции оценки требуется какой-то «тайм-аут» (обычно называемый «топливо»), например максимальное количество шагов для оценки, потому что Agda требует, чтобы все функции были полными. Вот пример из @gallais, который использует для этого тип коиндуктивного пристрастия.

person luqui    schedule 06.04.2010
comment
Большое спасибо. Я догадывался о чем-то подобном, но не совсем понимал. - person Jason Reich; 06.04.2010
comment
просто типизированное лямбда-исчисление [...] имеет члены без нормальных форм. Это правда? Я думал, что просто типизированное лямбда-исчисление (в отличие от нетипизированного лямбда-исчисления или более сложных типизированных вариантов лямбда-исчисления) всегда сводится к нормальной форме (если вы не добавляете оператор фиксированной точки как встроенный), поэтому он не является полным по Тьюрингу. - person sepp2k; 06.04.2010
comment
@ sepp2k Извините. Все еще пытаюсь понять это. Под встроенной фиксированной точкой вы подразумеваете, что оператор фиксированной точки остается неоцениваемым термином, а не частью функции оценки? - person Jason Reich; 12.04.2010
comment
@Jason: Под встроенным я просто подразумеваю, что вы не можете определить фиксированную точку как функцию в простом типизированном лямбда-исчислении (в то время как вы можете в нетипизированном лямбда-исчислении), поэтому он должен быть встроен в язык как оператор ( т.е. у вас есть ключевое слово fix и специальные правила для оценки выражений с использованием этого ключевого слова). - person sepp2k; 12.04.2010
comment
Стоит добавить, что вы действительно можете встроить нетипизированное лямбда-исчисление в Agda, оценив его в монаде пристрастности, которая моделирует возможное незавершение с, возможно, бесконечным числом дискретных шагов. - person copumpkin; 26.04.2012
comment
@copumpkin Мне бы хотелось, чтобы этот комментарий превратился в отдельный ответ. Как бы вы использовали монаду пристрастности для внедрения нетипизированного лямбда-исчисления? - person Hjulle; 03.10.2017