ocamlsum-type

# Returning an unnamed sum type

I am trying to create a local sum type inside of a function and then return said sum type without it being declared in main. Is this possible? I don't believe it is directly, but I have been playing around with GADT's and polymorphic variants to try and find a work around, but I am still fairly new to OCaml and do not fully understand them.

What I want the function to do is the following. Given a tuple of type `('a, 'b)`, return the first element, but with the type of the sum between `'a` and `'b`.

From gallais's answer, I tried working with `type ('a, 'b) either = | Left of 'a | Right of 'b`, but wasn't able to get it work.

Edit: In response to glennsl's comment, the problem I am trying to solve is for my course project. I am trying to implement the Curry-Howard isomorphism between Constructive Logic and programs. I've currently gotten the theorem-prover working as well as the program extraction, but I am struggling to convert the abstract form of a program to OCaml code when dealing with the disjunction rules. The ruleset I am using comes from page 34 of this document. I have included a picture of the Disjunction rules.

The example I asked about is the theorem (a n b) -> (a v b). There are two proofs which make sense, and I chose the one which uses the vIL rule, which corresponds to the left sum injection of the variable of type A into a sum type with two components, A and B. The program represented by this theorem (using this rule), is a function that takes in a tuple and returns the first element, but with the sum type A + B. I would like help coming the OCaml code for this example function. Once I understand that, hopefully I will be able to generalize it.

Solution

• It doesn't make a lot of sense to say you want to define a type that's local to a function. A function body is an expression, i.e., it is made from values not types. You can define a type in a module that's local to a function. But constructors defined in the module aren't allowed to escape the scope of the function.

``````# let f x =
let module M = struct type 'a t = T of 'a end in
M.T x;;
Error: [...] The type constructor M.t would escape its scope
``````

Using a globally defined type your function is easy to write:

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

let f (a, b) = Left a
``````

Here is an application of the function:

``````# f (3, "yes");;
- : (int, 'a) either = Left 3
``````

I don't think it helps to use GADTs or polymorphic variants. They are complicated but they don't allow violation of scoping rules which are a different thing.

You can use the OCaml module system to define an abstract type, if that's what you want. Make both the type and the function local to a module.