`(a,b)` versus `(a*b)` in ocaml

user_242189 0
Viewed 117

It seems that only a * b can fit in to _ and only (a,b) can fit in to (a,_).

I can imagine that a*b is a proper type for the internal product with components a and b whereas (a,b) is a external product of type a and type b (just a guess)

But are there examples distinguishing the two ?

type zero = Z : zero
type 'a succ = S : 'a succ

type _ ptree1 =
  | Leaf : 'a -> ('a * zero) ptree1
  | Node : (('a * 'n) ptree1 * ('a * 'n) ptree1) -> ('a * 'n succ) ptree1

type (_, _) ptree =
  | Leaf : 'a -> ('a, zero) ptree
  | Node : (('a, 'n) ptree * ('a, 'n) ptree) -> ('a, 'n succ) ptree

(* bad
type ('a * _) ptree =
  | Leaf : 'a -> ('a, zero) ptree
  | Node : (('a, 'n) ptree * ('a, 'n) ptree) -> ('a, 'n succ) ptree
 *)

let rec last1 : type n a. (a * n) ptree1 -> a = function
  | Leaf x      -> x
  | Node (_, t) -> last1 t

let rec last : type n a. (a, n) ptree -> a = function
  | Leaf x      -> x
  | Node (_, t) -> last t
ml ocaml
1 Answers

Type constructors have an arity in OCaml. For instance, in

type ('a,'b) either =
 | Left of 'a
 | Right of 'b

the type constructor either has an arity of two. And ('a,'b) either denotes the type constructor either applied to two argument 'a and 'b. The form ('a,'b) does not exist by itself in the language.

However, it is possible to encode type constructor with an arity of n as a type constructor of arity 1 constrained on only having a n-tuple type as an argument. Typically, this means rewriting either to

type 'p either2 =
 | Left2 of 'a
 | Right2 of 'b
constraint 'p = 'a * 'b

let translation: type a b. (a*b) either2 -> (a,b) either = function
| Left2 x -> Left x
| Right2 x -> Right x

Here, either2 is a type constructor of arity one, but which arguments must be a 2-tuple type.

This is the equivalent of translating a function of type 'a -> 'b -> 'c to a function of type 'a * 'b -> 'c at the type-level. And another point of view is that type-level applications were written like function applications ('a,'b) either would be written either 'a 'b and ('a * 'b) either2 would become either2 ('a * 'b).

Without GADTs, this kind of encoding requires the use of an explicit constraint and they are thus not that frequent. With GADTs, since the definition of the GADTs is free to construct its own type indices, this choice is simply more apparent. For instance, one can define an eccentric version of either as

type (_,_,_) either3 =
| Left3: 'a -> ('a list -> _, 'a * unit, _) either3
| Right3: 'a -> ( _ -> 'a array, _, unit * 'a) either3

let translate: type a b. (a list -> b array, a * unit, unit * b) either3 -> (a,b) either =
function
| Left3 x -> Left x
| Right3 x -> Right x

Here, either3 is a type constructor of arity 3, which stores the left and right types all over the place among its 3 argument.

user_73693660
Related