Модули и классы типов в Ur / Web

Я играю с модулями в Ur / Web и не могу понять, как вывести стандартные (показать, прочитать, eq) экземпляры класса типов вместе с системой модулей. Рассмотрим следующий код:

signature USER = sig
    type id
    type password
    val id_read : read id
    val pass_read : read password
    val id_show : show id
    val login : { Id : id, Password : password } -> transaction bool
    val whoami : transaction (option id)
end

functor MakeUser(M : sig type id
                         type password
                    end) : USER = struct
    type id = M.id
    type password = M.password

    table user : { Id : id, Password : password }
                     PRIMARY KEY Id
    cookie c : { Id : id, Password : password }
    fun login r =
        b <- oneRowE1 (SELECT COUNT( * ) > 0
                       FROM user
                       WHERE user.Id = {[r.Id]}
                         AND user.Password = {[r.Password]});
        if b then
            setCookie c { Value = r, Expires = None, Secure = False };
            return True
        else return False
    val whoami =
        cc <- getCookie c;
        case cc of
            None => return None
          | Some r =>
            b <- oneRowE1 (SELECT COUNT( * ) > 0
                           FROM user
                           WHERE user.Id = {[r.Id]}
                             AND user.Password = {[r.Password]});
            if b then
                return (Some r.Id)
            else
                return None
end

structure User = MakeUser(struct
                              type id = string
                              type password = string
                          end)


fun main () =
    me <- User.whoami;
    return <xml><body>
      <h1>Logged in as : {cdata (show me)}</h1>
    </body></xml>
and login () =
    return <xml><body>
      <form>
        <textbox{#Id}/>
        <textbox{#Password}/>
        <submit action = {signin}/>
      </form>
    </body></xml>
and signin r =
    success <- User.login { Id = readError r.Id, Password = readError r.Password };
    if success then main()
    else login ()

этот код не компилируется с ошибками

Unmatched signature item Item:  val id_read : read id
Unmatched signature item Item:  val password_read : read password
Unmatched signature item Item:  val id_show : show id

Должен ли я явно реализовать эти экземпляры в аргументе функтора, или их все еще можно вывести? Как заставить этот код работать? И вообще "хорошей" документации по классам типов в Уре я не нашел.

Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
2
0
45
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Спасибо Адам, который указал мне на решение:

It's necessary to include lines like val id_read = _ in the functor body.

Также пришлось добавить

val inj_id : sql_injectable id
val inj_prim_id : sql_injectable_prim id
val inj_pass : sql_injectable password

в сигнатуру аргумента функтора.

Итак, я пришел к следующему определению функтора MakeUser:

functor MakeUser(M : sig type id
                         type password
                         val id_read : read id
                         val pass_read : read password
                         val id_show : show id
                         val inj_id : sql_injectable id
                         val inj_prim_id : sql_injectable_prim id
                         val inj_pass : sql_injectable password
                    end) : USER = struct
    type id = M.id
    type password = M.password
    val id_read = _
    val pass_read = _
    val id_show = _

    table user : { Id : id, Password : password }
                     PRIMARY KEY Id
    cookie c : { Id : id, Password : password }
    fun login r =
        b <- oneRowE1 (SELECT COUNT( * ) > 0
                       FROM user
                       WHERE user.Id = {[r.Id]}
                         AND user.Password = {[r.Password]});
        if b then
            setCookie c { Value = r, Expires = None, Secure = False };
            return True
        else return False
    val whoami =
        cc <- getCookie c;
        case cc of
            None => return None
          | Some r =>
            b <- oneRowE1 (SELECT COUNT( * ) > 0
                           FROM user
                           WHERE user.Id = {[r.Id]}
                             AND user.Password = {[r.Password]});
            if b then
                return (Some r.Id)
            else
                return None
end

Другие вопросы по теме