Locally abstract type, polymorphism and function signature

Learning
1

So I have been learning about both type theory and GADT lately and I thought I could try to encode a constructive proof on my own with GADT. I decided to encode a proof of a version of law of excluded middle for natural integer (two integers are either equal or not equal). During the process, I got puzzled by the interaction between locally abstract types and the displayed function signature. I tried a bit to reduce the problem but I am not yet very confortable and I don’t fully understand the problem, so I give you the entire code (which is not that long anyway). Here is what I came up with :

type void = |
type 'a neg = 'a -> void
type ('a, 'b) either = Left of 'a | Right of 'b
type (_, _) eq = Refl: ('a, 'a) eq

type zero
type _ s = S: 'n -> 'n s
type _ nat = Z: zero nat | S: 'n nat -> 'n s nat

type ('n1, 'n2) nat_lem = (('n1 nat, 'n2 nat) eq, ('n1 nat, 'n2 nat) eq neg) either

let z_not_s: (zero nat, 'n s nat) eq -> void = function _ -> .
let s_not_z: ('n s nat, zero nat) eq -> void = function _ -> .

let prop_eq: type n1 n2. (n1 nat, n2 nat) eq -> (n1 s nat, n2 s nat) eq =
  function Refl -> Refl
  
let backprop_eq: type n1 n2. (n1 s nat, n2 s nat) eq -> (n1 nat, n2 nat) eq =
  function Refl -> Refl
  
let prop_neq: type n1 n2.(n1 nat, n2 nat) eq neg -> (n1 s nat, n2 s nat) eq neg
    = fun n1_n2_neq n1s_n2s_eq -> n1_n2_neq (backprop_eq n1s_n2s_eq)

let propagate:  type n1 n2. (n1, n2) nat_lem -> (n1 s, n2 s) nat_lem = function
  | Left peq -> Left (prop_eq peq)
  | Right pneq -> Right (prop_neq pneq)

let rec are_equal: type n1 n2. n1 nat -> n2 nat -> (n1, n2) nat_lem = 
fun n1 n2 -> match n1, n2 with
  | Z, Z -> Left Refl
  | Z, S _ -> Right z_not_s
  | S _, Z -> Right s_not_z
  | S n1, S n2 -> propagate (are_equal n1 n2)

let () = match are_equal (S (S Z)) (S (S Z)) with
  | Left _ -> print_endline "true !"
  | Right _ -> print_endline "false !"

It works : in this case, the code prints true, and if you change the first (S (S Z)) to Z or S Z, it will print false. So I am happy with that. My first question would be : is there anything in this code that I could improve or that you would have done differently.

I have a second, more specific question : when I type the function prop_eq in utop, the type it displays is simply :

 val prop_eq : ('n1 nat, 'n2 nat) eq -> ('n1 s nat, 'n2 s nat) eq

Instead of the more specific type I wrote, which is :

type n1 n2. (n1 nat, n2 nat) eq -> (n1 s nat, n2 s nat) eq

So I would tend to think that in this specific case, the typechecker has deduced that these types are equivalent. But if I change my type annotation in prop_eq with the type above (the one given by utop with more standard polymorphism), then the function propagate does not compile anymore :

let prop_eq: ('n1 nat, 'n2 nat) eq -> ('n1 s nat, 'n2 s nat) eq =
  function Refl -> Refl
  ...
let propagate:  type n1 n2. (n1, n2) nat_lem -> (n1 s, n2 s) nat_lem = function
  | Left peq -> Left (prop_eq peq)
  | Right pneq -> Right (prop_neq pneq)

Line 2, characters 30-33:
Error: This expression has type (n1 nat, n2 nat) eq
but an expression was expected of type (n1 nat, n1 nat) eq
Type n2 is not compatible with type n1

The error does not help me much. So it seems that these two types are indeed different, even in my specific case. My question is then : why are they printed the same way in toplevel ? Is it the intended behaviour or just some small mistake waiting to be fixed ? I also know that you can’t specify explicit polymorphism or locally abstract types in module signatures, is this related ? If I do the same thing with prop_neq or backprop_eq, the same error arises.

If you could also take this occasion to re-explain the subtleties between locally abstract types, explicit polymorphism and the combination of both, that could also help me. For example, why do I need to use locally abstract type in my example. By doing the exercises on gadt I finally got a kind of instinct of which one to use in which case but it is still not clear for me, and I have yet to find a case where I should use the form with only locally abstract type - this one :

let f = fun (type t) (foo : t list) -> …

Instead of this one (with explicit polymorphism):

let f : type t. t list -> ... = fun foo -> …

Thank you in advance !

2

An important point is that the meaning of type variables ('a, 'b, …) are slightly different in type signature and explicit type annotation.

Typically:

val fst: 'a * 'b -> 'a

means for all type 'a and 'b, the function fst takes a pair of 'a and 'b and returns a 'a.
Contrarily, the following function compiles:

# let not_fst: 'a * 'b -> 'a = fun (x,y) -> x + y;;
val not_fst: int * int -> int

because the explicit type annotation means: there are some types 'a and 'b such that not_fst has type 'a * 'b -> 'a. And in this case, those types 'a and 'b are actually int. If you want to express, that a function f should have the type 'a * 'b -> 'a, you need to add an explicit for all annotation:

# let fst: 'a 'b. 'a * 'b -> 'a = fun (x,y) -> x;;
val fst: 'a * 'b -> 'b

Here, the prefix 'a 'b. ... in the explicit type annotation means: for all 'a and 'b.
The important point is that this for all quantification is implicitly always here in type signature.

One way to look at this difference is that type annotation are here to help the type inference, whereas in type signature the inference is already done, so the syntax can focus on conveying the final type.

In fact locally abstract types are a good example of annotations which are needed for type inference, but never appear in type signature. Those types have mostly two use case: in local modules and in GADTs. For GADTs, there are needed to communicate that a type may be refined by pattern matching on a GADT.

For instance, your prop_eq function can be written:

let prop_eq (type n1 n2):  (n1 nat, n2 nat) eq -> (n1 s nat, n2 s nat) eq =
  function Refl -> Refl

Here, we add a local type equation n1 nat = n2 nat on the right hand side of -> and use it to prove that
n1 s nat = n2 s nat.
Without such annotation, the typechecker would follow the normal global inference rule:

let prop_eq ('n1 nat, 'n2 nat) eq -> ('n1 s nat, 'n2 s nat) eq =
  function Refl -> Refl

and deduce that 'n1 = 'n2 because Refl has type ('a,'a) eq.

Concerning the question of the difference between explicit polymorphic annotations and locally abstract types, the short version is that polymorphic annotations are needed for polymorphic recursion and locally abstract types for GADTs. Consequently, if you are defining a non-recursive function like prop_eq, you can use only a locally abstract type. However, if you are defining a recursive function on a GADT type, you probably need both. Your function are_equal is classical use case:

let rec are_equal: type n1 n2. n1 nat -> n2 nat -> (n1, n2) nat_lem = 
fun n1 n2 -> match n1, n2 with
  | Z, Z -> Left Refl
  | Z, S _ -> Right z_not_s
  | S _, Z -> Right s_not_z
  | S n1, S n2 -> propagate (are_equal n1 n2)

In the example above, type n1 n2. ... is a shorthand notation that combines an explicit polymorphic annotation with the introduction of two local abstract types n1 and n2. It is possible to split the two notion and rewrite are_equal as:

 let rec are_equal: 'n1 'n2. 'n1 nat -> 'n2 nat -> ('n1,'n2) nat_lem =
 fun (type n1) (type n2) (n1:n1 nat) (n2:n2 nat): (n1,n2) nat_lem ->
 match n1, n2 with
  | Z, Z -> Left Refl
  | Z, S _ -> Right z_not_s
  | S _, Z -> Right s_not_z
  | S n1, S n2 -> propagate (are_equal n1 n2);;

but this form is a bit of a mouthful, so most people only use the shorthand version.

6 Likes
3

Thanks for the long answer, that helps a lot. “Polymorphism annotation for recursion, locally abstract type for GADT” was the kind of rule of thumb I was looking for. Thinking about this, would it be correct if I’d say that using locally abstract type is actually saying to the typechecker “here is a type a that you will use in this function, this is neither a concrete type that you know about nor a polymorphic type, don’t try to infer a generic type for this function but just resolve locally the types independently at each call site” ?

4

This is the right idea but I would slightly amend your phrasing to

here is a type a that you will use in this function, this is neither a concrete type that you know about
nor a type variable that you can unify you another type

because, once the function is typed, the locally abstract type are generalized:

 # let f (type a) (x:a) = (x:a);;
val f : 'a -> 'a = <fun>

In fact, this illustrates another use case for locally abstract types: debugging a function by making sure that an argument type is never unified with anything.
For instance, the function f below fails to compile when the type inference try to deduce that a=int.

let f (type a) (x: a list) = match x with
| a :: l -> (a + 1) :: l
| [] -> []

Line 2, characters 13-14:
Error: This expression has type a but an expression was expected of type int