Polymorphic type conversion

Learning
1

Hi, I am trying to understand how polymorphic type works, and read some related questions like Polymorphic variants - converting polymorphic variant type to type with lower bound constraint and Inferred types and polymorphic variants. They are helpful, but I don’t know how to fit my situation.

I want to create a variable c with type `Imm. However, the result is of type [> `Imm of int ]. I guess that `Imm constructor does not know the return type of T.create () so it has a '>' symbol for the type. However, how can I convert this [> `Imm of int ] to [`Imm]?

(Polymorphic variants - converting polymorphic variant type to type with lower bound constraint) suggested to use explicit coercion, but it is applied for a function where I am dealing with a variable.

open Core

module T = struct
  type t = int
  let create () = 1
end

module A = struct
  type operand = 
  [`Imm of T.t]
end

module C = struct
  let foo =
    let c = `Imm (T.create ()) in
    printf "%d " c
end
2

wut? There was a type problem w/the printf, but that was all.

Process OCaml finished
OCaml version 4.14.0
Enter #help;; for help.

# open Printf

module T = struct
  type t = int
  let create () = 1
end

module A = struct
  type operand = 
  [`Imm of T.t]
end

module C = struct
  let foo =
    let c = `Imm (T.create ()) in
    printf "%d " (match c with `Imm n -> n)
end;;
1 module T : sig type t = int val create : unit -> int end
module A : sig type operand = [ `Imm of T.t ] end
module C : sig val foo : unit end
#
1 Like
3

Thank you for your reply :grinning:. In fact it is a simplified version of my project. In the above case, this match method works and returned a int, can I get the value with type [`Imm]?

4

Unsure what you mean, but this typechecks just fine:

module C = struct
  let foo =
    let c = `Imm (T.create ()) in
    let x : [`Imm of T.t] = c in
    printf "%d " (match c with `Imm n -> n)
end;;

What do you mean by

the value with type [`Imm]?

1 Like
5

Hmm … maybe you mean this (note A.create):

Process OCaml finished
OCaml version 4.14.0
Enter #help;; for help.

# open Printf

module T = struct
  type t = int
  let create () = 1
end

module A = struct
  type operand = 
  [`Imm of T.t]
  let create () : [`Imm of T.t] = `Imm (T.create())
end

module C = struct
  let foo =
    let c = A.create() in
    let x : [`Imm of T.t] = c in
    printf "%d " (match c with `Imm n -> n)
end;;
Line 17, characters 8-9:
17 |     let x : [`Imm of T.t] = c in
             ^
Warning 26 [unused-var]: unused variable x.
1 module T : sig type t = int val create : unit -> int end
module A :
  sig type operand = [ `Imm of T.t ] val create : unit -> [ `Imm of T.t ] end
module C : sig val foo : unit end
#
1 Like
6

Reading your post more literally, perhaps you’re asking why is the type [> `Imm of T.t] instead of of [ `Imm of T.t] ?

Answer (to the best of my knowledge): the > signifies that other polymorphic variants may also be members of this type. The idea is that if you’re using polymorphic variants, then you’re probably going to use types with more than one variant. So you’ll have code like:

match e1 with
pat1 -> .... `Imm e1
| pat2 -> .... `Bar e2
... etc ...

Now if the type of `Imm e1 is [ `Imm of e1ty ], then that’s not very useful is it? B/c then the type of `Bar e2 would be [ `Bar of e2ty ] and those two types don’t unify, do they? Whereas if each is [ > .... etc etc ] then the two types unify into a type like [> `Imm of e1ty | `Bar of e2ty ]

Does that make sense ?

ETA: It’s a little confusing, and whenever I use polyvariants, I always end up using a lot of typecasting to make sure I know what the types are for most of the variable-bindings.

1 Like
7

Thank you for your thoughtful answer :smile: ! It makes sense for me to understand the existence of '>'. And it is awesome to declare variable with its type explicitly. I only used them in signature before and it totally makes sense to use in the function body as well!

8

Ah, OK, so maybe worth writing a little more about “when you should think about putting type-constraints on variables”. It’s been a long time since I was an adept in the Church of Curry-Howard, so my understanding is certainly out-of-date and erroneous in parts. But

Generally speaking, if you stick to the pure functional core of Caml, plus algebraic datatypes, then you will get most general types automatically inferred. So type-annotations are for hiding type-information, or temporarily added to debug why the type-checker won’t accept your code. In the end, except for hiding type-info, there’s no need for type-constraints.

[here’s where it gets really dicey …] When you start introducing mutable data (as I was reminded a few days ago here in this forum grin) and for sure polyvariants and objects, you are going to find more and more cases where you must add type-constraints, simply because the type-inference algorithm is not complete. [geez, I think that’s the right term … beeen so long]

I think that that’s the state of play these days: for the various extensions of what we might call “Core Caml”, you have to add type annotations sometimes.

1 Like