Паттерн Model-Update-View и зависимые типы

в 12:21, , рубрики: c++, dependent type, elm, haskell, idris, Model-Updater-View, scala, зависимые типы, интерфейсы, функциональное программирование

Паттерн Model-Update-View и зависимые типы - 1

Model-Updater-View — функциональный паттерн, успешно применяемый в языке Elm в основном для разработки пользовательских интерфейсов. Что бы им воспользоваться надо создать тип Model, представляющий полное состояние программы, тип Message, описывающий события внешней среды, на которые программа должна реагировать, меняя свое состояние, функцию updater, которая из старого состояния и сообщения создает новое состояние прораммы и функции view, которая вычисляет по состоянию программы требуемые воздействия на внешнюю среду, которые порождают события типа Message. Паттерн очень удобный, но у него есть маленький недостаток — он не позволяет описать какие собятия имеют смысл для конкретных состояний программы.

Схожая проблема возникает (и решается) и при использовании ОО-паттерна State.

Язык Elm простой, но очень строгий — он проверяет, что функция updater хоть как-то обрабатывает все возможные сочетания модели-состояние и сообщения-события. По этому приходится писать лишний, пусть и тривиальный — как правило оставляющий модель без изменений, код. Я хочу продемонстрировать, как этого можно избежать в более сложных языках — Idris, Scala, C++ и Haskell.

Весь приведенный здесь код доступен на GitHub для экспериментов. Рассмотрим наиболее интересные места.

Idris

Idris — язык, поддерживающий зависимые типы. То есть в нем компилятор может следить за правильностью типизации, хотя тип одной переменной может зависить от значения другой. Типы в Idris похожи на обобщенные алгебраические типы в Haskell. Он описывается списком параметров типа и набором конструкторов — функций, создающих объекты данного типа. В отличие от Haskell, параметрами типа могут быть не только другие типы и классы типов, но и значения, в том числе функции.

Опишем на нем тип простого приложения, использующего паттерн Model-Updater-View.

data Application : (model:Type) ->
                         (msg: model -> Type) ->
                         (vtype : Type -> Type) ->
                         Type
   where
      MUV : model ->
               (updater : (m:model) -> (msg m) -> model) ->
               (view : (m:model) -> vtype (msg m)) ->
               Application model msg vtype

Здесь описан параметризированный тип данных Application. Его параметрами является тип model, функция msg, преобразующая значение типа model в тип события, которое может произойти в данном состоянии прораммы, и тип view, который будет параметризован типом события — его можно трактовать как функцию из типа-параметра в простой тип.

Лирическое отступление о High Kind Types

Это единственное место, в котором используется параметр типа, который сам имеет параметры-типы. Такая возможность предоставляется не всеми языками — нее нет в том числе в Elm. Но в этом примере view вынесен в параметры типа приложения больше «для красоты» — что бы показать, что он является составляющей паттерна. Можно поступить как в Elm — использовать в качестве View фиксированный парамтеризованный тип (в Elm это Html msg).

Я хочу отметить, что HKT не являются необходимыми для использования зависимых типов — это разные ребра лямбда-куба

Функция msg необычна — она возвращает не значение, а тип. Во время исполнения про типы значений ни чего не известно — компилятор выполняет стирание всей лишней информации. То есть такая функция может быть вызвана только на этапе компиляции.

MUV — это конструктор. Он принимает параметры: model — начальное состояние программы, updater — функция обновления состояния при внешнем событии, и view — функция создания внешнего представления. Заметьте что тип функций updater и view зависит от значения модели (с помощью функции msg из параметров типа).

Теперь посмотрим, как это приложение запустить

muvRun : (Application modelType msgType IO) -> IO a
muvRun (MUV model updater view) =
  do
    msg <- view model
    muvRun (MUV (updater model msg) updater view)

В качестве внешнего представления (view) мы выбрали операцию ввода/вывода (в Idris, как и в Haskell, операции ввода/вывода — first class values, что бы они выполнились надо предпринять дополнительные действия, обычно вернуть такую операцию из функции main).

Кратко об IO

При выполнении операции типа (IO a) происходит некоторое воздействие на внешний мир, возможно пустое, и в программу возвращается значение типа a, но функции стандартной библиотеки устроены так, что обработать его можно только порождая новое значение типа IO b. Таким образом чистые функции отделены от функций с побочными эффектами. Это непривычно многим программистам, но помогает писать более надежный код.

Так как функция muvRun порождает ввод/вывод, она должна вернуть IO, но так как она ни когда не завершиться, тип операции может быть любой — IO a.

Теперь опишем типы сущностей, с которыми мы собираемся работать

data Model = Logouted | Logined String

data MsgOuted = Login String
data MsgIned  = Logout | Greet

total
msgType : Model -> Type
msgType Logouted = MsgOuted
msgType (Logined _) = MsgIned

Здесь описан тип модели, отражающий наличие двух состояний интерфейса — пользователь не залогинен, и залогинен пользователь с именем типа String.

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

И наконец функция, задающая соответствие значения модели типу сообщения.

Функция объявлена тотальной — то есть она не должна упасть или зависнуть, компилятор постарается за этим проследить. msgType вызывается на этапе компиляции, а значит ее тотальность означает, что компиляция не зависнит из-за нашей ошибки, хотя и не может гарантировать, что выполнение этой функции приведет к исчерпанию ресурсов системы.
Так же гарантировано, что она не выполнит «rm -rf /», потому что в ее сигнатуре нет IO.

Опишем updater:

total
updater : (m:Model) -> (msgType m) -> Model
updater Logouted (Login name) = Logined name
updater (Logined name) Logout = Logouted
updater (Logined name) Greet = Logined name

Думаю логика этой функции понятна. Хочу еще раз отметить тотальность — она означает что компилятор Idris проверит, что мы рассмотрели все разрешенные системой типов альтернативы. Elm тоже осуществляет такую проверку, но он не может знать, что мы не можем разлогиниться, если еще не залогинены, и потребует явную обработку условия

updater Logouted Logout = ???

Idris же в лишней проверки найдет несоотвествие типов.

Теперь приступим к view — как обычно в UI это будет самой сложной частью кода.

total
loginPage : IO MsgOuted
loginPage = do
           putStr "Login: "
           map Login getLine

total
genMsg : String -> MsgIned
genMsg "" = Logout
genMsg _ = Greet

total
workPage : String -> IO MsgIned
workPage name = do
           putStr ("Hello, " ++ name ++ "n")
           putStr "Input empty string for logout or nonempty for greetingn"
           map genMsg getLine

total
view : (m: Model) -> IO (msgType m)
view Logouted = loginPage
view (Logined name) = workPage name

view должна создавать операцию ввода/вывода, которая возвращает сообщения, тип которого снова зависит от значения модели. У нас есть два варианта: loginPage, который выводит сообщение «Login:», читает строку с клавиатуры и заворачивает ее в сообщение Login и workPage с параметром именем пользователя, который выводит приветсвие и возвращает различные сообщения (но одинакового типа — MsgIned) в зависимости от того, введет пользоваль пустую или не пустую строку. view возвращает одну из этих операций в зависимости от значения модели, и компилятор проверяет их тип, несмотря на то, что он разный.

Теперь мы можем создать и запустить наше приложение

app : Application Model Main.msgType IO
app = MUV Logouted updater view

main : IO ()
main = muvRun app

Здесь надо отметить тонкий момент — функция muvRun возврящает IO a, где a не было специфицировано, а значение main имеет тип IO (), где () — это имя типа, обычно называемого Unit, у которого есть единственное значение, тоже записываемое как пустой тупл (). Но компилятор с этим легко справляется. подставив вместо a ().

Scala и зависимые от пути типы

В Scala нет полноценной поддержки зависимых типов, но есть типы, зависимые от экземпляра объекта, через который на него ссылаются (path dependent types). В теории зависимых типов их можно описать как вариант сигма-типа. Зависимые от пути типы позволяют запретить складывать вектора из разных векторных пространств, или описать кому с кем можно целоваться. Но мы их применим для более простых задач.

sealed abstract class MsgLogouted
case class Login(name: String) extends MsgLogouted

sealed abstract class MsgLogined
case class Logout() extends MsgLogined
case class Greet() extends MsgLogined

abstract class View[Msg] {
  def run() : Msg
}

sealed abstract class Model {
  type Message
  def view() : View[Message]
}

case class Logouted() extends Model {
  type Message = MsgLogouted
  override def view() : View[Message]
  ....
}

case class Logined(name: String) extends Model {
  type Message = MsgLogined
  override def view() : View[Message]
  ....
}

Алгебраические типы в Scala моделируются через наследование. Типу соотвествует некоторый sealed abstract class, а каждому конструктору унаследованный от него case class. Мы будем стараться их использовать именно как алгебраические типы, описывая все переменные как принадлежащие к родительскому sealed abstract class.

Классы MsgLogined и MsgLogouted в рамках нашей программы не имеют общего предка. Функцию view пришлось размазать по разным классам модели, что бы иметь доступ к конкретному типу сообщений. В этом есть свои плюсы, которые оценят сторонники ОО — код получается сгруппирован в соотвествии с бизнес-логикой, все что связано с одним use case оказывается рядом. Но мне бы больше понравилось выделить view в отдельную функцию, разработку которой можно было бы передать другому человеку.

Теперь реализуем updater

object Updater {
  def update(model: Model)(msg: model.Message) : Model = {
    model match {
      case Logouted() => msg match {
        case Login(name) => Logined(name)
      }
      case Logined(name) => msg match {
        case Logout() => Logouted()
        case Greet() => model
      }
    }
  }
}

Здесь мы, используя зависимые от пути типы, описываем тип второго аргумента от значения первого. Что бы Scala воспринимала подобные зависимости, функции приходится описывать в карррированном виде, то есть в виде функции от первого аргумента, которая возвращает функцию от второго аргумента. К сожалению, Scala в этом месте не осуществляет многих проверок типов, для которых у компилятора достаточно информации.

Теперь дадим полную реализацию модели и view

case class Logouted() extends Model {
  type Message = MsgLogouted
  override def view() : View[Message] = new View[Message] {
   override def run() = {
     println("Enter name ")
     val name = scala.io.StdIn.readLine()
     Login(name)
   }
  }
}

case class Logined(name: String) extends Model {
  type Message = MsgLogined
  override def view() : View[Message] = new View[Message] {
   override def run() = {
     println(s"Hello, $name")
     println("Empty string for logout, nonempy for greeting.")
     scala.io.StdIn.readLine() match {
       case "" => Logout()
       case _ => Greet()
     }
   }
  }
}

abstract class View[Msg] {
  def run() : Msg
}

object Viewer {
  def view(model: Model): View[model.Message] = {
    model.view()
  }
}

Тип возвращаемого функцией view зависит от экземпляра ее аргумента. Но за реализацией она обращается в модель.

Запускается созданное так приложение так

object Main {
  import scala.annotation.tailrec

  @tailrec def process(m: Model) {
    val msg = Viewer.view(m).run()
    process(Updater.update(m)(msg))
  }

  def main(args: Array[String]) = {
    process(Logouted())
  }
}

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

Здесь нам понадобились не все возможности, продоставляемые зависимыми от пути типами. Интересные свойства проявятся, если мы будем параллельно работать с неколькими экземплярами систем Model-Updater-View, например при симуляции многоагентного мира (view тогда бы представлял из себя воздействие агента на мир и получение обратной связи). В этом случае компилятор проверял, что сообщение обрабатывается именно тем агентом, для которого преднозначено, несмотря на то, что все агенты имеют одинаковый тип.

С++

С++ до сих пор чувствителен к порядку определений, даже если они все сделаны в одном файле. Это создает некоторые неудобства. Я буду приводить код в удобной для демонстрации идей последовательнсоти. Упорядоченную для компилируемости версию можно посмотреть на GitHub.

Алгебраические типы могут быть реализованы так же, как в Scala — абстрактный класс соответствует типу, а конкретные наследники — конструкторам (назовем их «классами-конструкторами», что бы не путать с обычными конструкторами C++) алгебраического типа.

В C++ есть поддержка зависимых от пути типов, но компилятор не может использовать этот тип абстрактно, не зная реального типа, с которым он связан. По этому реализовать Model-Updater-View с их помощью не получается.

Но C++ располагает мощной системой шаблонов. Зависимость типа от значения модели можно спрятав его в шаблонный параметр специализированной версии исполнительной системы.

struct Processor {
        virtual const Processor *next() const = 0;
};

template <typename CurModel> struct ProcessorImpl : public Processor {
        const CurModel * model;
        ProcessorImpl<CurModel>(const CurModel* m) : model(m) { };
        const Processor *next() const {
                const View<typename CurModel::Message> * view = model->view();
                const typename CurModel::Message * msg = view->run();
                delete view;
                const Model * newModel = msg->process(model);
                delete msg;
                return newModel->processor();
        }
};

Мы описываем абстрактную исполнительную систему, с единственным методом — выполнить все, что требуется, и вернуть новую исполнительную систему, подходящую для следующей итерации. Конкреная версия имеет шаблонный параметр и будет специализирована для каждого «класса-конструктора» модели. Здесь важно, что все свойства типа CurModel будут проверены во время специализации шаблона конкретным параметром-типом, а на момент компиляции самого шаблона их описывать не требуется (хотя и возможно с помощью концептов или других способов реализации классов типов). Scala тоже имеет достаточно мощную систему параметризованных типов, но проверки свойств типов-параметров она осуществляет во время компиляции параметризованного типа. Там реализация такого паттерна затруднена, но возможна, благодоря поддержке классов типов.

Опишем модель.

struct Model {
        virtual ~Model() {};
        virtual const Processor *processor() const = 0;
};

struct Logined : public Model {
        struct Message {
                const virtual Model * process(const Logined * m) const = 0;
                virtual ~Message() {};
        };
        struct Logout : public Message {
                const Model * process(const Logined * m) const;
        };
        struct Greet : public Message {
                const Model * process(const Logined * m) const;
        };

        const std::string name;
        Logined(std::string lname) : name(lname) { };

        struct LoginedView : public View<Message> {
           ...
        };

        const View<Message> * view() const {
                return new LoginedView(name);
        };

        const Processor *processor() const {
                return new ProcessorImpl<Logined>(this);
        };
};

struct Logouted : public Model {
        struct Message {
                const virtual Model * process(const Logouted * m) const = 0;
                virtual ~Message() {};
        };
        struct Login : public Message {
                const std::string name;
                Login(std::string lname) : name(lname) { };
                const Model * process(const Logouted * m) const;
        };

        struct LogoutedView : public View<Message> {
           ...
        };

        const View<Message> * view() const {
                return new LogoutedView();
        };

        const Processor *processor() const {
                return new ProcessorImpl<Logouted>(this);
        };
};

«Классы-конструкторы» модели «все свое носят с собой» — то есть содержат спициализированные для них классы сообщений и view, а так же умеют создавать исполнительную систему под себя. Собственные типы View имеют общего для всех моделей предка, что может оказаться полезно при разработке более сложных исполнительных систем. Принципиально что типы сообщений полностью изолированы и не имеют общего предка.

Реализация updater отделена от модели, поскольку требует что бы тип модели был уже полностью описан.

const Model * Logouted::Login::process(const Logouted * m) const {
        delete m;
        return new Logined(name);
};

const Model * Logined::Logout::process(const Logined * m) const {
        delete m;
        return new Logouted();
};

const Model * Logined::Greet::process(const Logined * m) const {
        return m;
};

Теперь соберем вместе все, что относится к view, включая внутренние сущности моделей

template <typename Message> struct View {
        virtual const Message * run() const = 0;
        virtual ~View<Message>() {};
};

struct Logined : public Model {
        struct LoginedView : public View<Message> {
                const std::string name;
                LoginedView(std::string lname) : name(lname) {};
                virtual const Message * run() const {
                        char buf[16];
                        printf("Hello %s", name.c_str());
                        fgets(buf, 15, stdin);
                        return (*buf == 0 || *buf == 'n' || *buf == 'r')
                             ? static_cast<const Message*>(new Logout())
                             : static_cast<const Message *>(new Greet);
                };
        };

        const View<Message> * view() const {
                return new LoginedView(name);
        };
};

struct Logouted : public Model {
        struct LogoutedView : public View<Message> {
                virtual const Message * run() const {
                        char buf[16];
                        printf("Login: ");
                        fgets(buf, 15, stdin);
                        return new Login(buf);
                };
        };

        const View<Message> * view() const {
                return new LogoutedView();
        };
};

И, наконец, напишем main

int main(int argc, char ** argv) {
        const Processor * p = new ProcessorImpl<Logouted>(new Logouted());
        while(true) {
                const Processor * pnew = p->next();
                delete p;
                p = pnew;
        }
        return 0;
}

И снова Scala, уже с классами типов

По структуре эта реализация почти полностью повторяет версию на C++.

Аналогичная часть кода


abstract class View[Message] {
  def run(): Message
}

abstract class Processor {
  def next(): Processor;
}

sealed abstract class Model {
  def processor(): Processor
}
sealed abstract class LoginedMessage
case class Logout() extends LoginedMessage
case class Greet() extends LoginedMessage

case class Logined(val name: String) extends Model {
  override def processor(): Processor = new ProcessorImpl[Logined, LoginedMessage](this)
}

sealed abstract class LogoutedMessage
case class Login(name: String) extends LogoutedMessage

case class Logouted() extends Model {
  override def processor(): Processor = new ProcessorImpl[Logouted, LogoutedMessage](this)
}

object Main {
  import scala.annotation.tailrec

  @tailrec def process(p: Processor) {
    process(p.next())
  }

  def main(args: Array[String]) = {
    process(new ProcessorImpl[Logouted, LogoutedMessage](Logouted()))
  }
}

А вот в реализации среды исполнения возникают тонкости.

class ProcessorImpl[M <: Model, Message](model: M)(
          implicit updater: (M, Message) => Model,
                    view: M => View[Message]
         ) extends Processor {
  def next(): Processor = {
    val v = view(model)
    val msg = v.run()
    val newModel = updater(model,msg)
    newModel.processor()
  }
}

Здесь мы видим новые таинственные параметры (implicit updater: (M, Message) => Model, view: M => View[Message]). Ключевое слово implicit означает что компилятор при вызове этой функции (точнее конструктора класса) будет искать в контексте помечанные как implicit объекты подходящих типов и передавать их в качестве соответствующих параметров. Это достаточно сложная концепция, одно их применений которой — реализация классов типов. Здесь они обещают компилятору, что для конкретных реализаций модели и сообщения все необходимые функции нами будут предоставлены. Теперь выполним это обещание.

object updaters {
  implicit def logoutedUpdater(model: Logouted, msg: LogoutedMessage): Model = {
    (model, msg) match {
      case (Logouted(), Login(name)) => Logined(name)
    }
  }
  implicit def viewLogouted(model: Logouted) = new View[LogoutedMessage] {
    override def run() : LogoutedMessage = {
     println("Enter name ")
     val name = scala.io.StdIn.readLine()
     Login(name)
    }
  }

  implicit def loginedUpdater(model: Logined, msg: LoginedMessage): Model = {
    (model, msg) match {
      case (Logined(name), Logout()) => Logouted()
      case (Logined(name), Greet()) => model
    }
  }
  implicit def viewLogined(model: Logined) = new View[LoginedMessage] {
    val name = model.name
    override def run() : LoginedMessage = {
     println(s"Hello, $name")
     println("Empty string for logout, nonempy for greeting.")
     scala.io.StdIn.readLine() match {
       case "" => Logout()
       case _ => Greet()
     }
    }
  }
}

import updaters._

Haskell

В мейнстримовом Haskell нет зависимых типов. В нем так же отсутствиет наследование, которое мы существенно применяли при реализации паттерна в Scala и C++. Но одноуровневое наследование (с элементами зависимых типов) может быть смоделировано с помощью более-менее стандандартных расширений языка -TypeFamilies и ExistentialQuantification. Для общего интерфейса дочерних ООП-классов заводится класс типов, в котором присутствует зависимый «семейный» тип, сами дочерние классы представляются отдельным типом, а потом заворачиваются в «экзистенциональный» тип с единственным конструктором.

data Model = forall m. (Updatable m, Viewable m) => Model m

class Updatable m where
  data Message m :: *
  update :: m -> (Message m) -> Model

class (Updatable m) => Viewable m where
  view :: m -> (View (Message m))

data Logouted = Logouted

data Logined = Logined String

Я попытался разнести updater и view как можно дальше, по этому создал два разных класса типов, но пока это плохо получилось.

Реализация updater проста

instance Updatable Logouted where
  data Message Logouted = Login String
  update Logouted (Login name) = Model (Logined name)

instance Updatable Logined where
  data Message Logined = Logout | Greeting
  update m Logout = Model Logouted
  update m Greeting = Model m

В качестве View пришлось зафиксировать IO. Попытки сделать его более абстрактным сильно все усложняли и повышали связанность кода — тип Model должен знать, какой именно View мы собираемся использовать.

import System.IO

type View a = IO a

instance Viewable Logouted where
  view Logouted = do
      putStr "Login: "
      hFlush stdout
      fmap Login getLine

instance Viewable Logined where
  view (Logined name) = do
      putStr $ "Hello " ++ name ++ "!n"
      hFlush stdout
      l <- getLine
      pure $ if l == ""
             then
               Logout
             else
               Greeting

Ну и исполняемая среда мало отличается от аналогичной в Idris

runMUV :: Model -> IO a
runMUV (Model m) = do
  msg <- view m
  runMUV $ update m msg

main :: IO ()
main = runMUV (Model Logouted)

Автор: Михаил Потанин

Источник

Поделиться

* - обязательные к заполнению поля