Функторы OCaml :: нелогичное поведение - PullRequest
13 голосов
/ 20 марта 2012

Я экспериментирую с языком модулей 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 дает другой результат?

Ответы [ 4 ]

10 голосов
/ 20 марта 2012

Конструкция : отличается в основном языке и в языке модуля.На базовом языке это конструкция аннотации.Например, ((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:type 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)
7 голосов
/ 20 марта 2012

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

# 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.

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

5 голосов
/ 20 марта 2012

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

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 ведущего дизайнера по модулям, типам и отдельной сборке .Волосатые математические части можно пропустить.

5 голосов
/ 20 марта 2012

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

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

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

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

...