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 vI_{L} 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.

- OCaml functions on uncertain data types
- Module unavailable when compiling another file that uses it in OCaml
- OCaml equivalent of Python generators
- Compiling multifile projects in Ocaml, leading to Unbound Module error
- Why this recursion example in ocaml doesn't work for negative number?
- OCaml and Opam: unbound module Core
- Figuring out why these types differ when using a catch all in the pattern matching
- Submatrix Ocaml
- Is there a way to `match` on a string that starts with some value?
- Combine two lists while removing duplicates
- Base causes issue with tuple destructuring
- OCaml combine fprintf and sprintf
- deleting duplicates tail recursively in OCaml
- Concurrent write with OCaml Async
- OCaml standard Map vs. Jane Street Core.std Map
- Can't find .ocamlinit file
- Waiting for Writer.write to complete in Caml Async
- Windows support for Jane Street OCaml Core?
- solver_get_unsat_core() in ML (OCaml) API returns empty core
- Debugging with dune
- How to apply a function in an iterable list
- How can I simplify nested pattern matching clauses?
- OCaml - a function which returns all the prefixes of a list
- OCaml Syntax error with if-else block without any information
- Can't compile Hello World in F*
- How to add a library dependency in a dune project that manages the .opam file without an intermediate build error?
- How do I read in lines from a text file in OCaml?
- F# changes to OCaml
- OCaml: Simplest way to merge 2 lists
- How can I change user defined type to int?