Подтвердить что ты не робот

Функциональные возможности OCaml:: противоинтуитивное поведение

Я экспериментирую с языком модуля OCaml (3.12.1), определяя функторы и сигнатуры для модулей и т.д., в основном следуя примерам из Глава 2 из руководства OCaml, и я случайно наткнулся на ситуацию, когда, по-видимому, моя ментальная модель того, как работают функторы и сигнатуры модулей, является ошибочной. Я попытался сузить ситуацию, с которой я столкнулся, до кратчайшего возможного кода, поэтому не спрашивайте, чего я пытаюсь выполнить, это полностью надуманный пример для демонстрации функции OCaml, о которой идет речь.

Итак, у нас есть функтор, который просто предоставляет идентификационную функцию 'f' и параметризуется модулем, снабжающим тип входного параметра этой функции. На самом деле надуманный пример, как я сказал.

module type SOMETYPE = sig type t end ;;
module Identity = functor (Type: SOMETYPE) -> struct let f (x: Type.t) = x end ;;

Учитывая вышеизложенное, мы переходим к определению модуля для подачи типа int:

module IntType = struct type t = int end ;;

.. и затем мы используем функтор для генерации модуля для функции тождества int:

module IdentityInt = Identity(IntType) ;;

Разумеется, сгенерированный модуль и его функция f будут вести себя так, как ожидалось:

#IdentityInt.f(3) + 10 ;;
- : int = 13

Ментальная модель функторов, являющаяся функциями, которые берут модули в качестве входных и возвращаемых модулей, кажется, служит нам до сих пор. Функтор Identity ожидает в качестве входного параметра модуля подписи (тип модуля) SOMETYPE, и действительно, модуль, который мы поставили (IntType), имеет правильную сигнатуру, и поэтому создается допустимый модуль вывода (IdentityInt), чей f работает так, как ожидалось.

Теперь идет неинтуитивная часть. Что, если мы хотим сделать это явным, что поставляемый модуль IntType действительно является модулем типа SOMETYPE. Как в:

module IntType : SOMETYPE = struct type t = int end ;;

а затем сгенерируйте модуль вывода функтора так же, как и раньше:

module IdentityInt = Identity(IntType) ;;

... попробуйте использовать функцию f для вновь созданного модуля:

IdentityInt.f 0 ;;

Затем REPL жалуется на:

"Error: This expression [the value 0] has type int but an expression was expected of type IntType.t."

Как обеспечить избыточную, но правильную информацию о типе, нарушить код? Даже в случае A модуль-функтор Identity должен был обрабатывать модуль IntType как тип SOMETYPE. Итак, почему явное объявление типа IntType будет SOMETYPE дает другой результат?

4b9b3361

ОТВЕТЫ

Ответ 1

Конструкция : отличается на основном языке и на языке модуля. На основном языке это аннотация. Например, ((3, x) : 'a * 'a list) ограничивает выражение выражением типа, являющегося экземпляром 'a * 'a list; так как первый элемент пары является целым числом, let (a, b) = ((3, x) : 'a * 'a list) in a + 1 хорошо типизирован. Конструкция : на модулях не означает этого.

Конструкция M : S связывает модуль M с сигнатурой S. Это непрозрачная печать: только информация, указанная в сигнатуре S, остается доступной при использовании типов M : S. Когда вы пишете module IntType : SOMETYPE = struct type t end, это альтернативный синтаксис для

module IntType = (struct type t end : SOMETYPE)

Так как поле типа t в SOMETYPE остается неопределенным, IntType имеет поле абстрактного типа t: тип IntType - это новый тип, созданный этим определением.

Кстати, вы, вероятно, имели в виду module IntType = (struct type t = int end : SOMETYPE); но в любом случае IntType.t является абстрактным типом.

Если вы хотите указать, что модуль имеет определенную подпись, оставив некоторые открытые типы, вам необходимо добавить явное равенство для этих типов. Нет никакой конструкции, чтобы добавить все выводимые равенства, потому что применение сигнатуры к модулю обычно предназначено для скрытия информации. В интересах простоты язык предлагает только одну генеративную конструкцию уплотнения. Если вы хотите использовать определенную подпись SOMETYPE и сохранить прозрачность типа t, добавьте ограничение к сигнатуре:

module IntType = (struct type t = int end : SOMETYPE with type t = int)

Ответ 2

Если вы посмотрите на выведенную подпись, когда вы не пишете что-то явно:

# module IntType = struct type t = int end ;;
module IntType : sig type t = int end

Подпись показывает, что t является int. Ваша подпись, напротив:

# module IntType : SOMETYPE = struct type t = int end ;;
module IntType : SOMETYPE

действительно:

# module IntType : sig type t end = struct type t = int end ;;
module IntType : sig type t end

Это, кажется, решает вашу проблему:

# module IntType : (SOMETYPE with type t = int) = struct type t = int end ;;
module IntType : sig type t = int end
# module IdentityInt = Identity(IntType) ;;
module IdentityInt : sig val f : IntType.t -> IntType.t end
# IdentityInt.f 0 ;;
- : IntType.t = 0

(вам не нужны парнеры, но они помогают мысленно разобрать). В принципе, вы раскрываете тот факт, что t является int с вашей подписью. Так что OCaml знает равенство IntType.t = int.

Для получения дополнительной информации о внутренних компонентах я оставлю его более осведомленным людям.

Ответ 3

Когда вы пишете:

module IntType : SOMETYPE = struct type t = int end ;;

Вы ограничиваете подпись InType точным SOMETYPE. Это означает, например, что тип t теперь становится абстрактным типом (реализация которого неизвестна типу).

Так что IdentityInt.f type по-прежнему IntType.t -> IntType.t, но, используя ограничение подписи, вы явно удалили уравнение IntType.t = int из знаний о типе. Сообщение об ошибке, которое вы получите, сообщает вам именно это.

Ответ 4

Ваша ключевая ошибка была здесь:

module IntType: SOMETYPE = struct type t end;;

Когда вы приписываете подпись SOMETYPE, это непрозрачный заголовок, а личность с int теряется. Тип IntType.t теперь абстрактный тип.

Вместо этого вам нужно приписать подпись SOMETYPE with type t = int.

Этот протокол показывает разницу:

# module type SOMETYPE = sig type t end;;
module type SOMETYPE = sig type t end
# module IntType : SOMETYPE with type t = int = struct type t = int end;; 
module IntType : sig type t = int end
# module AbsType : SOMETYPE = struct type t = int end;;                 
module AbsType : SOMETYPE

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