编译器接受的OCaml中明显无效的幻像类型 [英] Apparently invalid phantom type in OCaml accepted by the compiler

问题描述

我试图回答这个问题: 在其他类型声明中可能会选择一个类型的子类型 使用幻像类型.所以我正要提出这段代码:

I was trying to answer this question: Ocaml selecting a type's subtype in another type declaration using phantom types. So I was about to propose this code:

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类型.但是所有内容都已编译，程序可以执行.

because g is of type red t -> colour and square is of type yellow t. But everything compiled, and the program can be executed.

我在这里想念什么?这是编译器的预期行为吗?

What did I miss here? Is this the expected behavior of the compiler?

推荐答案

由于您要在ColouredShape的签名中公开CoulouredShape.t的结构，因此类型检查器会同时知道red t = shape * colour和yellow t = shape * colour，然后是red t = yellow t.

Since you're exposing the structure of CoulouredShape.t in the signature of ColouredShape, the type checker knows that both red t = shape * colour and yellow t = shape * colour, and it then follows that red t = yellow t.

但是，如果使ColouredShape.t为抽象，则在ColouredShape之外这些类型的相等性是未知的，因此您将得到适当的错误:

If you make ColouredShape.t abstract however, those type equalities aren't known outside ColouredShape, and hence you'll get the appropriate error:

    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

这篇关于编译器接受的OCaml中明显无效的幻像类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！