Часто яm в добавлении полей к ADT, которые запоминают только некоторую избыточную информацию. Но у меня нетЯ разобрался полностью, как сделать это красиво и эффективно.

Лучший способ показать проблему - это сделать пример. Предположим, мыработа с нетипизированными лямбда-терминами:

type VSym = String

data Lambda = Var VSym 
            | App Lambda Lambda
            | Abs VSym Lambda

Время от времени нам нужно вычислять множество свободных переменных члена:

fv :: Lambda -> Set VSym
fv (Var v)    = Set.singleton v
fv (App s t)  = (fv s) `Set.union` (fv t)
fv (Abs v t)  = v `Set.delete` (fv t)

Вскоре мы понимаем, что повторные вычисленияfv являются узким местом нашего приложения. Мы бы хотели как-то добавить его к типу данных. Подобно:

data Lambda1 = Var (Set VSym) VSym
             | App (Set VSym) Lambda Lambda
             | Abs (Set VSym) VSym Lambda

Но это делает определение довольно некрасивым. Почти(Set VSym) занимает больше места, чем все остальные. Кроме того, это нарушает сопоставление с образцом во всех функциях, которые используютLambda, И что еще хуже, если позже мы решим добавить какое-нибудь другое поле для запоминания, мыПридется переписать все шаблоны снова.

Как разработать общее решение, позволяющее легко и незаметно добавлять такие поля для запоминания? Я'Я хотел бы достичь следующих целей:

data определение должно выглядеть как можно ближе к оригиналу, чтобы онос легко читаемым и понятным.Шаблонные совпадения тоже должны оставаться простыми и читаемыми.Добавление нового поля запоминания позже не должно нарушать существующий код, в частности:не нарушать существующие шаблоны,не требовать изменений там, где была использована функция, которую мы хотим запомнить (например, код, который использовалfv в этом примере) .I '

опишу мое текущее решение: чтобы сохранитьdata определения и шаблоны соответствуют как можно более загроможденнымs определить:

data Lambda' memo = Var memo VSym 
                  | App memo (Lambda' memo) (Lambda' memo)
                  | Abs memo VSym (Lambda' memo)
type Lambda = Lambda' LambdaMemo

где данные для запоминания определяются отдельно:

data LambdaMemo = LambdaMemo { _fv :: Set VSym, _depth :: Int }

Затем простая функция, которая извлекает запомненную часть:

memo :: Lambda' memo -> memo
memo (Var c _)   = c
memo (App c _ _) = c
memo (Abs c _ _) = c

(Это можно устранить с помощью именованных полей. Но тогда мы быдолжны назвать все остальные поля также.)

Это позволяет нам выбирать конкретные детали из памятки, сохраняя одну и ту же подписьfv как прежде:

fv :: Lambda -> Set VSym
fv = _fv . memo

depth :: Lambda -> Int
depth = _depth . memo

Наконец, мы объявляем эти умные конструкторы:

var :: VSym -> Lambda
var v = Var (LambdaMemo (Set.singleton v) 0) v

app :: Lambda -> Lambda -> Lambda
app s t = App (LambdaMemo (fv s `Set.union` fv t) (max (depth t) (depth s))) s t

abs :: VSym -> Lambda -> Lambda
abs v t = Abs (LambdaMemo (v `Set.delete` fv t) (1 + depth t)) v t

Теперь мы можем эффективно писать вещи, которые сочетают сопоставление с шаблоном с чтением запомненных полей, таких как

canSubstitute :: VSym -> Lambda -> Lambda -> Bool
canSubstitute x s t
  | not (x `Set.member` (fv t))
      = True -- the variable doesn't occur in `t` at all
canSubstitute x s t@(Abs _ u t')
  | u `Set.member` (fv s)
      = False
  | otherwise
      = canSubstitute x s t'
canSubstitute x s (Var _ _)
      = True
canSubstitute x s (App _ t1 t2)
      = canSubstitute x s t1 && canSubstitute x s t2

Это, кажется, решить:

Сопоставление с образцом все еще вполне разумно.Если мы добавим новое поле для запоминания, оно выиграетне нарушать существующий код.Если мы решили запомнить функцию с подписьюLambda -> Something мы можем легко добавить его в качестве нового поля для запоминания.

Что я до сих пор неМне нравится этот дизайн:

data определение нетак плохо, но все ещеmemo везде это сильно загромождает.Нам нужны умные конструкторы для построения значений, но мы используем обычные конструкторы для сопоставления с образцом. Это не так плохо, мы просто добавляем один_, но было бы неплохо иметь одну и ту же сигнатуру для конструирования и деконструкции. Я полагаюПросмотры или жеУзор Синонимы бы решить это.Вычисление запомненных полей (свободные переменные, глубина) тесно связано с умными конструкторами. Как это'Разумно предположить, что эти запомненные функции будут всегдакатаморфизмЯ считаю, что это может быть решено в некоторой степени с помощью таких инструментов, какпакет Fixpoint.

Есть идеи как его улучшить? Или есть лучшие способы решить такую проблему?