OCaml: How to handle sum type properly?

Question

suppose I have the following code:

type s = A of a | B of b


let foo (a:?) = 

let bar (input:s) = match input with
| A a -> foo input
| B b -> ...

My question is what should I fill in the question mark in the signature of foo so I won't need a (redundant) match statement in it? Or is there a better pattern to do this?

Answer 1

If you want to avoid rematch, I see 3 solutions:

1. have the function foo simply take the "payload" of the value constructor A, and reconstruct a value of type s as its output (or any other type matching the output type of bar).

   # type a;;
   type a
   # type b;;
   type b
   
   
   # module Ex1 = struct
   
     type s = A of a | B of b
   
   
     let foo (a:a) = A a
   
     let bar (input:s) = match input with
     | A a -> foo a
     | B b -> (* ... *) input
   end;;
   
   module Ex1 :
   sig
     type s = A of a | B of b 
     val foo : a -> s 
     val bar : s -> s 
   end
   

2. use polymorphic variants:

   # module Ex2 = struct
   
     type s = [ `A of a | `B of b ]
   
     let foo (`A a) = `A a
   
     let bar (input:s) = match input with
       | `A _ as a -> foo a
       | `B b -> (* ... *) input
    end;;
    module Ex2 :
    sig
      type s = [ `A of a | `B of b ]
      val foo : [< `A of 'a ] -> [> `A of 'a ]
      val bar : s -> s
    end
   

3. use GADTs:

   # module Ex3 = struct
   
     type _ s = 
     | A : a -> a s 
     | B : b -> b s
   
   
     let foo (a: a s) : a s = 
       match a with
       | A a -> A a
   
     let bar: type x.  x s -> x s = fun input ->
       match input with
       | A _ as a -> foo a
       | B b -> (* ... *) input
   
    end;;
    module Ex3 :
    sig
      type _ s = A : a -> a s | B : b -> b s
      val foo : a s -> a s
      val bar : 'x s -> 'x s
    end
   

Answer 2

Starting with your example, the solution would be simple:

type s = A of a | B of b


let foo (a:a) = 

let bar (input:s) = match input with
| A a -> foo a
| B b -> ...

But constraint here is not needed. Looks like that you're misunderstanding the idea of type constraints. In general, in OCaml type constraints cannot affect the program. Programs with and without type constraints have the same behavior. So, here you don't need to put any constraints at all. You must think of type annotations only as a helper tool for programmer.

Update

I'm still not sure, that I understand what actually you want, but if you want to split your variants into subsets, and keep this split refutable, then, indeed, you can use polymorphic variants, as Pascal suggested.

Let me first rephrase the questions. Suppose I have type:

  type t = A | B | C | D | E

and I have a pattern match

  let f = function
    | A | B | C as x -> handle_abc x
    | D | E as x -> handle_de x

How can I prove to a compiler, that handle_abc takes only a subset of all possible constructors, namely A | B | C ?

The answer is, with regular variants it is impossible. But it is possible with polymorphic variants:

type t = [`A | `B | `C | `D | `E]

let f = function
  | `A | `B | `C as x -> handle_abc x
  | `D | `E as -> handle_de x

So, handle_abc now needs only to pattern match on three variants, and don't need to have any redundant matches. Moreover, you can give names to a groups of constructors, and pattern match on this names:

type abc = [`A | `B | `C ]
type de  = [`D | `E ]
type t = [ abc | de ]

let f = function
  | #abc as x -> handle_abc x
  | #de as -> handle_de x

As a real world example, you can take a look at BAP project where polymorphic variants are used to represent instruction code. Here we split all codes into different subgroups, like all move instructions, all branch instructions and so on. And later we can pattern match on the groups directly.