Этот ответ дает больше интуиции о том, как получить контейнеры из функторов, чем мой предыдущий.Я придерживаюсь совершенно другого подхода, поэтому я делаю новый ответ вместо того, чтобы пересматривать старый.
Простые рекурсивные типы
Давайте сначала рассмотрим простой рекурсивный тип, чтобы понять непараметрические контейнеры и для сравнения с параметризованным обобщением.Лямбда-исчисление, не заботясь об объемах, дается следующим функтором:
Inductive LC_F (t : Type) : Type :=
| App : t -> t -> LC_F t
| Lam : t -> LC_F t
.
Из этого типа мы можем извлечь две информации:
shape сообщает нам о конструкторах (App, Lam) и, возможно, также вспомогательных данных, не относящихся к рекурсивной природе синтаксиса (здесь нет).Существует два конструктора, поэтому форма имеет два значения.Shape := App_S | Lam_S (bool также работает, но объявление форм в качестве автономных индуктивных типов обходится дешево, а именованные конструкторы также удваиваются в качестве документации.)
Для каждой фигуры (то есть конструктора), позиция говорит нам о рекурсивных вхождениях синтаксиса в этом конструкторе.App содержит две подтермы, поэтому мы можем определить их две позиции как логические;Lam содержит одну подтерму, поэтому его позиция является единицей.Можно также сделать Pos (s : Shape) индексированным индуктивным типом, но программировать с ним очень сложно (просто попробуйте).
(* Lambda calculus *)
Inductive ShapeLC :=
| App_S (* The shape App _ _ *)
| Lam_S (* The shape Lam _ *)
.
Definition PosLC s :=
match s with
| App_S => bool
| Lam_S => unit
end.
Параметризованные рекурсивные типы
Сейчаслямбда-исчисление с правильной областью действия:
Inductive LC_F (f : Type -> Type) (a : Type) : Type :=
| App : f a -> f a -> LC_F a
| Lam : f (unit + a) -> LC_F a
.
В этом случае мы все еще можем повторно использовать данные Shape и Pos из ранее.Но этот функтор кодирует еще одну часть информации: как каждая позиция изменяет параметр типа a.Я называю этот параметр контекстом (Ctx).
Definition CtxLC (s : ShapeLC) : PosLC s -> Type -> Type :=
match s with
| App_S => fun _ a => a (* subterms of App reuse the same context *)
| Lam_S => fun _ a => unit + a (* Lam introduces one variable in the context of its subterm *)
end.
Этот контейнер (ShapeLC, PosLC, CtxLC) связан с функтором LC_F изоморфизмом: между сигмой { s : ShapeLC & forall p : PosLC s, f (CtxLC s p a) } и LC_F a.В частности, обратите внимание, как функция y : forall p, f (CtxLC s p) говорит вам, как именно заполнить форму s = App_S или s = Lam_S, чтобы построить значение App (y true) (y false) : LC_F a или Lam (y tt) : LC_F a.
Мое предыдущее представление закодировано Ctxв некоторых дополнительных типовых индексах Pos.Представления эквивалентны, но это выглядит здесь более аккуратно.
Исчисление обработчика исключений
Мы рассмотрим только конструктор Catch.Он имеет четыре поля: тип X, основное вычисление (которое возвращает X), обработчик исключений (который также восстанавливает X) и продолжение (потребляющее X).
Inductive Exc_F (E : Type) (F : Type -> Type) (A : Type) :=
| ccatch : forall X, F X -> (E -> F X) -> (X -> F A) -> Exc_F E F A.
Форма представляет собой один конструктор, но вы должны включить X.По сути, посмотрите на все поля (возможно, разворачивая вложенные индуктивные типы) и сохраните все данные, которые не включают F, это ваша форма.
Inductive ShapeExc :=
| ccatch_S (X : Type) (* The shape ccatch X _ (fun e => _) (fun x => _) *)
.
(* equivalently, Definition ShapeExc := Type. *)
Тип позиции перечисляет все способыполучить F из Exc_F соответствующей формы.В частности, позиция содержит аргументы для применения функций и, возможно, любые данные для разрешения ветвления любого другого вида.В частности, вам нужно знать тип исключения для хранения исключений для обработчика.
Inductive PosExc (E : Type) (s : ShapeExc) : Type :=
| main_pos (* F X *)
| handle_pos (e : E) (* E -> F X *)
| continue_pos (x : getX s) (* X -> F A *)
.
(* The function getX takes the type X contained in a ShapeExc value, by pattern-matching: getX (ccatch_S X) := X. *)
Наконец, для каждой позиции вам нужно решить, как меняется контекст, т.е.X или A:
Definition Ctx (E : Type) (s : ShapeExc) (p : PosExc E s) : Type -> Type :=
match p with
| main_pos | handle_pos _ => fun _ => getX s
| continue_pos _ => fun A => A
end.
Используя условные обозначения ваш код , вы можете затем закодировать конструктор Catch следующим образом:
Definition Catch' {E X A}
(m : Free (C__Exc E) X)
(h : E -> Free (C__Exc E) X)
(k : X -> Free (C__Exc E) A) : Free (C__Exc E) A :=
impure (@ext (C__Exc E) (Free (C__Exc E)) A (ccatch_S X) (fun p =>
match p with
| main_pos => m
| handle_pos e => h e
| continue_pos x => k x
end)).
(* I had problems with type inference for some reason, hence @ext is explicitly applied *)
Полная суть https://gist.github.com/Lysxia/6e7fb880c14207eda5fc6a5c06ef3522