Блог

Главная - Вопросы по программированию - состояние монады в поле записи

состояние монады в поле записи

#monads #coq

Вопрос:

У меня есть два типа Foo и Bar , такие, которые Bar имеют a Foo в качестве поля.

 Inductive Foo := ...
Record Bar := { f : Foo }.

И у меня есть операция «с сохранением состояния» на Foo 

 Definition useFoo : state Foo nat := ...

Теперь я хочу применить это useFoo к a Bar , чтобы получить a useBar : state Bar nat , но я не могу понять, как составить эту монаду состояния. Я бы предположил, что есть какой-то стандартный объектив, который позволяет мне фокусировать поле, но я не могу его найти.

  1. Как мне правильно составить a useFoo : state Foo nat с чем-то, чтобы я получил useBar : state Bar nat
  2. Есть ли простой способ сделать это в обычной монадной нотации?
  3. Как обычно пишутся функции «с сохранением состояния» для подобъектов?

Некоторая дополнительная информация, которую я забыл включить в начале:

Откуда взялось понятие монады состояния?

Я использую MonadState из coq ext lib.

 Class MonadState@{s d c} (T : Type@{s}) (m : Type@{d} -> Type@{c}) : Type :=
{ get : m T
; put : T -> m unit
}.

Где было определено состояние функции?

Это запись в файле StateMonad из ext-lib.

 Record state (t : Type) : Type := mkState { runState : S -> t * S }.

На какой литературе вы основываетесь?

На самом деле я не основываю это на какой-либо литературе, я просто пытаюсь использовать то, что дает мне coq-ext-lib.

Комментарии:

1. Такое ощущение, что у вопроса слишком мало контекста. Откуда взялось понятие монады состояния ? Где была state определена функция? На какой литературе вы основываетесь?

2. Я обновил вопрос с некоторым контекстом

3. Отлично, я думаю, что указатель на ext-lib здесь играет важную роль.

4. Возможно, стоит покопаться в стандартной библиотеке Haskell / packages / stack overflow для ответа на этот вопрос, поскольку ваш вопрос на самом деле не зависит от Coq. (Вопросы, относящиеся к Coq, будут включать «как мне закодировать эту конкретную конструкцию из Haskell / math в Coq?» и «поддерживает ли эта библиотека Coq эту монадическую функцию, которая является общей в Haskell?»). Морально, все, что вам нужно для фокусировки монады состояния, — это getter ( Foo -> Bar ), который создается после get , и setter ( Foo -> Bar -> Foo ), который объединяется с getter для настройки функции обновления.

Метки: