Help making this "poly/generic" code compile

Learning
1

Moldified from section 2 of: OCaml - The core language

open Core

  let rec sort (lst : 'a list) =
    match lst with
    | [] -> []
    | head :: tail -> insert head (sort tail)
  and insert elt lst =
    let open Poly in
    match lst with
    | [] -> [ elt ]
    | head :: tail -> if elt <= head then elt :: lst else head :: insert elt tail
  in
  let _ = sort [ "is"; "a"; "table"; "told"; "etc." ] in
  let _ = sort [ 3.14; 2.718 ] in
  let _ = sort [ 6; 2; 5; 3 ] in
  ()

The problem here, I believe is that sort starts with type 'a list -> 'a list
but the first call binds 'a to string, which causes the 2nd call to have an
error of:

37 |   let _ = sort [ 3.14; 2.718 ] in
                     ^^^^
Error: This expression has type float but an expression was expected of type
        string

Question: without redefining sort, is there a way to make this code compile ?

1 Like
2

You can use an explicitly polymorphic annotation:

let () =
  (* Here is the line that is changed! *)
  let rec sort : 'a. 'a list -> 'a list =
   fun lst ->
    match lst with [] -> [] | head :: tail -> insert head (sort tail)
  and insert elt lst =
    let open Poly in
    match lst with
    | [] ->
        [elt]
    | head :: tail ->
        if elt <= head then elt :: lst else head :: insert elt tail
  in
  let _ = sort ["is"; "a"; "table"; "told"; "etc."] in
  let _ = sort [3.14; 2.718] in
  let _ = sort [6; 2; 5; 3] in
  ()
1 Like
3

  1. That worked, thanks.

  2. Is there also a way to solve this via:

let sort (type a) (lst: a list) : a list = ...

or is this a different concept? I spent some time chasing around compiler type errors, but could not get it to compile this way.

4

Note that the original issue with

is that the type annotation (lst: 'a list) makes the function works only on list of a certain type 'a
and with the first call to sort

let _ = sort ["is"; "a"; "table"; "told"; "etc."] in

the typechecker will infer that 'a = int. Removing the annotation all together will fix the issue because then the type of sort will be generalized outside of its definition.
In other words,

let id x = x in
id 1, id "two"

is fine but not

let monomorphic_id (x:'a) = x in
monomorphic_id 1, monomorphic_id "error"

In other words, if you want to add annotation for debugging purpose, it is necessary to use an explicitly polymorphic annotation:

let id: 'a. 'a -> 'a = fun x -> x in
id 1, id "two"

If your functions were not polymorphicrecursive, using just a locally abstract type,

let sort (type a) (lst: a list) : a list = ...

would also have worked.

To avoid this caveat, I advise in general to use the `explicit polymorphic annotation with locally abstract types" short form:

let id: type a. a -> a = fun x -> x in
id 1, id "two"

which works in (almost) all case and more often than not lead to better and earlier error.

4 Likes
5

Sorry, I don’t understand this. Is there a way to make it work with let sort (type a) (lst: a list) : a list … ` ?

The reason I really care about this is the following.

Suppose we have a function:

f: A.t -> B.t -> C.t -> D.t -> out.t

My choices are:

  1. no typing:
let f a b c d = ... 
doesn't work for me, too hard to read right now
  1. typing directly on vars:
let f (a: A.t) (b: B.t) (c: C.t) (d: D.t) : Out.t = ...
problem here is it's not poly/generic, we can't do 'forall'
  1. separate type and vars: (okay, I admit type signature changed, but I think point stands)
let f : 'a. 'a -> B.t -> C.t -> D.t -> Out.t =
  fun a b c d ->
Eh, we can do the forall, but I'm not a fan of separating the types & vars

Now, back to original question. I’m really curious if we can do it via

let sort (type a) (lst: a list) : a list = ...

since if this works, we can simultaneously do “forall” and “type right next to var”

6

Sorry, the issue is that your functions are recursive (not polymorphic).

let rec f (type a) = ...

doesn’t work. For recursive functions, you have to annotate the function itself rather than its argument.

1 Like
7

One more question on poly/generic :slight_smile:

Last example in section 1.6 of OCaml - The core language

  let fixpoint : 'a. ('a -> 'a) -> 'a -> 'a  = fun f x  ->
    let open Poly in 
    let exception Done in
    let x = ref x in
    try while true do
        let y = f !x in
        if !x = y then raise Done else x := y
      done; assert false
    with Done -> !x;;

I am a little confused by this type signature of:

  let fixpoint : 'a. ('a -> 'a) -> 'a -> 'a  = fun f x  ->

I would have expected something like:

  let fixpoint : 'a : Equal. ('a -> 'a) -> 'a -> 'a  = fun f x  ->

Because of the two lines:

    let open Poly in 
    ...
        if !x = y then raise Done else x := y
    ...

Intuitively, the forall 'a is strange reading because it does not
seem to be for all 'a, only those where Poly.(=) is defined.

My confusion here is how to think of type signatures of the form:

'a. ... expr ...

8

There is no ad-hoc polymorphism in OCaml, only parametric polymorphism. Thus the function (=): 'a -> 'a -> bool is defined for all types'a (even if it does fail dynamically on some memory representation). Type constraints of the form 'a . ... reads for all types 'a. ... . A more natural example would be:

let rec len: 'a. 'a list -> int = function
| [ ] -> 0
| _ :: q -> 1 + len q