MonadTransformer для проверки типа завершенного действия.

Преамбула

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

Вопрос

Я ищу MonadTransformer, который несет в себе идею быть полным или неполным таким образом, что действие стека монады не сможет проверить тип, если оно не завершено.

Моя ситуация

У меня есть стек Monad с состоянием, которое содержит MVar. Невозможность записи в этот MVar вызовет исключение thread blocked indefinitely in an MVar. Я мог бы просто проверить сам MVar, но передача его другому потоку (который следует тем же правилам) также является допустимым способом заполнения MVar (как и выдача ошибки).

Я ищу способ, чтобы средство проверки типов выдавало ошибку, если одно из этих условий не выполняется к моменту запуска монады. Я могу проверить во время выполнения, но я думаю, что может быть способ использовать систему типов.


haskell monads monad-transformers
person John F. Miller    schedule 13.04.2017    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Похоже, может помочь какая-то индексированная монада. Индексированные монады разрешают или запрещают некоторые операции в соответствии с некоторым состоянием уровня типа.

Мы также можем полагаться на полиморфизм:

{-# language RankNTypes #-}
import Control.Monad
import Control.Monad.Trans.State

-- Receives an v and returns a "proof" token
newtype Gulp token v = Gulp (v -> IO token)

-- Computation polymorphic on the token
type EnsuredWrite v r = forall token. StateT (Gulp token v) IO (token,r)

Идея состоит в том, что действия типа EnsuredWrite должны возвращать значение token, но знают, как создать его только путем передачи функции в Gulp. Если они вообще возвращаются, они, должно быть, вызвали эту функцию.

Фактический тип токена не важен, это может быть просто (). Но EnsuredWrite действия не должны этого знать, поэтому forall.

Однако это решение не запрещает повторные записи.

person danidiaz    schedule 13.04.2017