Subtyping function signatures

Learning
1

Hi,

I’m trying to use two types with the same signature, as below. Ocaml happily compiles the code without errors, but I would like the compiler to fail at test_want_compile_failure.

I suspect the solution lies in covariance/contravariance, but I’m unsure how to apply this in this context.

Thanks.

  type 'a maptype1 = 'a -> 'a

  type 'a maptype2 = 'a -> 'a

  let x: 'a maptype1 =
    fun value -> value

  let y: 'a maptype2 =
    fun value -> value

  let apply ( thing : 'a maptype1 ) =
    thing

  let test_want_compile_ok () =
    apply x

  let test_want_compile_failure () =
    apply y
2

When you write

type 'a maptype1 = 'a -> 'a

the type 'a maptype1 is an abbreviation for 'a -> 'a. Consequently, we have 'a maptype1 = 'a -> 'a = 'a maptype2.

One solution is to use an explicit signature to make the type constructor mapttype abstract, hiding this type equality:

module type Map = sig
   type 'a t
   val x: 'a t
   val apply: 'a t -> 'a -> 'a
end

module Map1: Map =struct
  type 'a t = 'a -> 'a
  let x value = value
  let apply f x = f x
end


module Map2: Map =struct
  type 'a t = 'a -> 'a
  let x value = value
  let apply f x = f x
end 

let x= Map1.x
let y = Map2.x
let ok () = Map1.apply x
let fail () = Map1.apply y
3

Thanks for the explanation and workaround. The solution is quite noisy - would be great if there was a way to control type unfolding inline, but I guess that’s life.

4

You can also wrap the value with a single constructor type (or single field record)

type 'a map1 = A of ('a -> 'a) [@@unboxed] 
type 'a map2 = B of ('a -> 'a) [@@unboxed]
let x = A (fun x -> x)
let y = B(fun x -> x)
let apply1 (A f) x = x
let apply2 (B f) x = x
let ok () = apply1 x
let fail () = apply1 y

Depending on your precise use case, it might be less noisy.

5

Definitely easier on the eye - thank you!