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.
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.