Типы модулей OCaml и отдельная компиляция

Question

Я читаю через OCaml lead designer's 1994 paper on modules, types, and separate compilation. (любезно указал на меня Norman Ramsey в another question). Я понимаю, что в документе обсуждается происхождение нынешней системы типа/подписи системы OCaml. Это он, автор предлагает непрозрачную интерпретацию деклараций типов в подписях (чтобы разрешить раздельную компиляцию) вместе с декларациями манифеста (для выразительности). Попытка собрать воедино некоторые примеры моих собственных, чтобы продемонстрировать вид проблем OCaml модуль подписи нотация пытается решить я написал следующий код в двух файлах:

В файле ordering.ml (или .mli - Я пробовал оба) (файл а):

module type ORDERING = sig 
type t 
val isLess : t -> t -> bool 
end 

и в файле useOrdering.ml (файл в):

open Ordering 
module StringOrdering : ORDERING 
    let main() = 
    Printf.printf "%b" StringOrdering.isLess "a" "b" 
    main() 

Идея состоит в том, чтобы ожидать, что компилятор будет жаловаться (при компиляции второго файла), который недостаточно для информации о типе, доступен на модуле StringOrdering для typecheck приложения StringOrdering.isLess (и тем самым мотивирует необходимость синтаксиса with type). Однако, хотя файл A компилируется, как ожидается, файл B вызывает 3.11.2 ocamlc, чтобы жаловаться на синтаксическую ошибку. Я понял, что подписи должны позволять кому-то писать код на основе подписи модуля, без доступа к реализации (структура модуля).

Я признаю, что я не уверен, о синтаксисе: module A : B который я столкнулся в this rather old paper on separate compilation, но это заставляет меня задаться вопросом, существует ли такой или подобный синтаксис (без участия функторов), чтобы позволить кому-то писать код, основанный только на тип модуля, с фактической структурой модуля, предоставленной во время связывания, подобно тому, как можно использовать файлы *.h и *.c на C/C++. Без такой возможности, казалось бы, что типы модулей/сигнатуры в основном предназначены для герметизации/скрытия внутренних модулей или более явной проверки/аннотации типов, но не для отдельной/независимой компиляции.

На самом деле, глядя на OCaml manual section on modules and separate compilation, кажется, что моя аналогия с C единицей компиляции нарушаются, так как руководство OCaml определяет OCaml единицы компиляции, чтобы стать A.ml и A.mli дуэтом, в то время как в C/C++ в .h файлах вставляются в единица компиляции любого импортирующего файла .c.

Answer 1

Правильный способ сделать такую ​​вещь, чтобы сделать следующее:

1. В ordering.mli пишут:

   (* This define the signature *) 
   module type ORDERING = sig 
       type t 
       val isLess : t -> t -> bool 
   end 
   
   (* This define a module having ORDERING as signature *) 
   module StringOrdering : ORDERING 
   

2. Compile файл: ocamlc -c ordering.mli

3. В другой файл, см. скомпилированную подпись:

   open Ordering 
   
   let main() = 
       Printf.printf "%b" (StringOrdering.isLess "a" "b") 
   
   let() = main() 
   

   При компиляции файла вы получаете ожидаемую ошибку типа (т.е. string не совместим с Ordering.StringOrdering.t). Если вы хотите удалить ошибку типа, добавьте ограничение with type t = string к определению StringOrdering в ordering.mli.

Так ответ вам второй вопрос: да, в режиме байт-кода компилятор просто нужно знать об интерфейсах Ваш, в зависимости от, и вы можете выбрать, какую реализацию использовать во время компоновки. По умолчанию это неверно для компиляции собственного кода (из-за оптимизации между модулями), но вы можете отключить его.

Answer 2

Возможно, вас просто смущает связь между явным определением модулей и сигнатур и неявное определение модулей через файлы .ml/.mli.

В принципе, если у вас есть файл a.ml и использовать его в какой-либо другой файл, то это, как если бы вы написали

module A = 
struct 
    (* content of file a.ml *) 
end 

Если у вас также есть a.mli, то это, как если бы вы написали

module A : 
sig 
    (* content of file a.mli *) 
end = 
struct 
    (* content of file a.ml *) 
end 

Обратите внимание, что это только определяет модуль с именем A, а не модуль типа. Этому механизму нельзя дать имя подписи.

Другой файл, использующий A, может быть скомпилирован только против a.mli, без предоставления a.ml вообще. Однако вы хотите убедиться, что вся информация о типе становится прозрачной там, где это необходимо. Например, предположим, что вы должны определить отображение над целыми числами:

(* intMap.mli *) 
type key = int 
type 'a map 
val empty : 'a map 
val add : key -> 'a -> 'a map -> 'a map 
val lookup : key -> 'a map -> 'a option 
... 

Здесь key сделан прозрачным, потому что любой код клиента (модуля IntMap, что эта подпись описывает) должен знать, что он должен быть в состоянии чтобы добавить что-то на карту. Однако сам тип map может (и должен) быть абстрактным, потому что клиент не должен вмешиваться в его детали реализации.

Отношение к файлам заголовков C состоит в том, что они в основном только позволяют использовать прозрачные типы. В Ocaml у вас есть выбор.

Answer 3

module StringOrdering : ORDERING - это декларация модуля. Вы можете использовать это в сигнатуре, чтобы сказать, что подпись содержит поле модуля, которое называется StringOrdering и имеет подпись ORDERING. Это не имеет смысла в модуле.

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

module StringOrderingImplementation = struct 
    type t = string 
    let isLess x y = x <= y 
end 

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

module StringOrderingAbstract = (StringOrdering : ORDERING) 

Тогда StringOrderingImplementation.isLess "a" "b" хорошо набран, тогда как StringOrderingAbstract.isLess "a" "b" не может быть напечатан, поскольку StringOrderingAbstract.t является абстрактным типом, который не совместит с string или любым другим типом, существовавшим ранее. На самом деле невозможно построить значение типа StringOrderingAbstract.t, так как модуль не содержит никакого конструктора.

Если у вас есть единица компиляции foo.ml, это модуль Foo, а подпись этого модуля задается файлом интерфейса foo.mli. То есть, файлы foo.ml и foo.mli эквивалентны определению модуля

module Foo = (struct (*…contents of foo.ml…*) end : 
       sig (*…contents of foo.mli…*) end) 

При компиляции модуля, использующего Foo, компилятор смотрит только на foo.mli (или скорее результат его компиляции: foo.cmi), а не на foo.ml ¹. Вот как сочетаются интерфейсы и отдельная компиляция. C нуждается в #include <foo.h>, поскольку в нем отсутствует какая-либо форма пространства имен; в OCaml Foo.bar автоматически ссылается на bar, определенный в модуле компиляции foo, если в области нет другого модуля с именем Foo.

¹ _{На самом деле, компилятор нативного кода рассматривает реализацию Foo для выполнения оптимизации (inlining). Контроллер типа никогда не смотрит ни на что, а на интерфейс.}