Видимо неверный фантомный тип в OCaml, принятый компилятором - PullRequest
Новая
       30

Видимо неверный фантомный тип в OCaml, принятый компилятором

1 голос
/ 11 марта 2020

Я пытался ответить на этот вопрос: Ocaml выбирает подтип типа в другом объявлении типа , используя фантомные типы. Поэтому я собирался предложить этот код: 

type colour = Red | Blue | Yellow                                                                                    
type shape  = Rectangle | Square


module ColouredShape : sig
  (* Type parameterized by 'a, just for the type system. 'a does not appear in the 
    right hand side *)
  type 'a t = shape * colour

  (* Dummy types, used as labels in the phantom type *)
  type red
  type yellow

  val make_red    : shape ->    red t
  val make_yellow : shape -> yellow t

  val make_rectangle : unit ->    red t
  val make_square    : unit -> yellow t

  val f :     'a t -> colour
  val g :    red t -> colour
  val h : yellow t -> colour

end
=
struct

  type 'a t = shape * colour
  type red
  type yellow

  let make_red    s = (s, Red)
  let make_yellow s = (s, Yellow)

  let make_rectangle ()  = make_red    Rectangle
  let make_square    ()  = make_yellow Square

  let f x = snd x
  let g x = snd x
  let h x = snd x

end



open ColouredShape
open Printf

let _ =
  let rectangle = make_rectangle () in
  let square    = make_square () in
  let c = f square in
  printf "%b\n" (c = Red);

  let c = f rectangle in
  printf "%b\n" (c = Red);

  let c = g square in
  printf "%b\n" (c = Red);

  let c = g rectangle in
  printf "%b\n" (c = Red);

  let c = h square in
  printf "%b\n" (c = Red);

  let c = h rectangle in
  printf "%b\n" (c = Red)

Я ожидал, что компилятор отклонит код в строке 

let c = g square in

, поскольку g имеет тип red t -> colour и square относится к типу yellow t. Но все скомпилировано, и программа может быть выполнена.

Что я здесь упустил? Это ожидаемое поведение компилятора?

Ответы [ 2 ]

3 голосов
/ 11 марта 2020

Поскольку вы выставляете структуру CoulouredShape.t в сигнатуре ColouredShape, средство проверки типов знает, что оба значения red t = shape * colour и yellow t = shape * colour, и из этого следует, что red t = yellow t.

Если вы сделаете ColouredShape.t абстрактным, однако, эти равенства типов не известны за пределами ColouredShape, и, следовательно, вы получите соответствующую ошибку: 

    let c = g square
              ^^^^^^
Error: This expression has type ColouredShape.yellow ColouredShape.t
       but an expression was expected of type
         ColouredShape.red ColouredShape.t
       Type ColouredShape.yellow is not compatible with type
         ColouredShape.red
2 голосов
/ 11 марта 2020

Одно из решений состоит в том, чтобы сделать тип абстрактным, то есть интерфейс модуля должен отображать только это: 

(* abstract *)
type 'a t

вместо 

(* concrete *)
type 'a t = shape * colour

Промежуточное решение, которое работает с последними версии OCaml должны объявлять тип как закрытый: 

type 'a t = private (shape * colour)

Обычно это полезно для раскрытия структуры типа в целях сопоставления с образцом, в то же время вынуждая пользователя создавать правильно сформированные объекты, вызывая Функции модуля.

Более простой пример использования private - для создания уникального идентификатора: 

module ID : sig
  type t = private int
  val create : unit -> t
end = struct
  type t = int  (* note: no 'private' *)
  let counter = ref 0
  let create () =
    let res = !counter in
    if res < 0 then
      failwith "ID.create: int overflow";
    incr counter;
    res
end
...