Здравствуйте, lomeo, Вы писали:

L>>>Есть data Mailslot с определённой функцией sendStateNotification :: Mailslot -> Result. Есть data S, содержащая этот мейлслот, необходимо, чтобы функция queryState :: S -> Result (ну хорошо, SInterface s => s -> Result) можно было определить только единственным образом. Ну так оно и есть!

E>>Если не сложно, тоже самое, только на русском.

L>Смысл такой — с помощью системы типов можно ограничить возможные реализации функции для данного типа (существование единственного доказательства для данной теоремы).

Т.е., грубо говоря, все это дело можно на C++ выразить чем-то вроде:

class Mailslot { public: void sendStateNotification(); };
class NonchangeableMailslotUsedSignal {
  private:
    // Создавать этот объект может только один класс.
    friend class S::NonchangeableMailslotHolder;
    NonchangeableMailslotUsedSignal() {}
};
class SInterface {
  public:
    virtual void NonchangeableMailslotUsedSignal queryState() = 0;
};

class S : public SInterface {
  private :
    class NonchangeableMailslotHolder {
      Mailslot & mailslot_;
    public :
      MonchangeableMailslotHolder( Mailslot & m ) : mailslot_( m ) {}

      NonchangeableMailslotUsedSignal sendStateNotify() {
        // Только здесь можно создать объект, тип которого указывает,
        // что обращение к sendStateNotify произошло.
        mailslot_.sendStateNotify();
        return NonchangeableMailslotUsedSignal();
      };
    };

    NonchangeableMailslotHolder mailslot_;

  public :
    S( Mailslot & m ) : mailslot_( m ) {}

    virtual NonchangeableMailslotUsedSignal
    queryState() { return mailslot_.sendStateNotify(); }
};

Получается, что мы требуем от SInterface.queryState() возвращение объекта такого типа, который производит только операция sendStateNotify() для неизменяемого, лишь однажды проинициализированного объекта Mailslot.

L>Я показал примитивный пример, для подробностей можно посмотреть

За ссылочки спасибо. Но на первый взгляд для меня это overkill.