Estou tentando criar um tipo de soma local dentro de uma função e, em seguida, retornar o referido tipo de soma sem que ele seja declarado em main. Isso é possível? Não acredito que seja diretamente, mas tenho brincado com GADTs e variantes polimórficas para tentar encontrar uma solução alternativa, mas ainda sou relativamente novo no OCaml e não os entendo completamente.
O que eu quero que a função faça é o seguinte. Dada uma tupla do tipo ('a, 'b), retorne o primeiro elemento, mas com o tipo da soma entre 'ae 'b.
Pela resposta de gallais , tentei trabalhar type ('a, 'b) either = | Left of 'a | Right of 'b, mas não consegui fazê-lo funcionar.
Editar: em resposta ao comentário de Glennsl, o problema que estou tentando resolver é para o meu projeto de curso. Estou tentando implementar o isomorfismo Curry-Howard entre Lógica Construtiva e programas. Atualmente, consegui que o provador de teoremas funcionasse, bem como a extração do programa, mas estou lutando para converter a forma abstrata de um programa em código OCaml ao lidar com as regras de disjunção. O conjunto de regras que estou usando vem da página 34 deste documento . Incluí uma imagem das regras de disjunção .
O exemplo que perguntei é o teorema (anb) -> (avb). Existem duas provas que fazem sentido, e escolhi aquela que utiliza a regra vI L , que corresponde à injeção da soma à esquerda da variável do tipo A em um tipo soma com duas componentes, A e B. O programa representado por esta teorema (usando esta regra), é uma função que recebe uma tupla e retorna o primeiro elemento, mas com o tipo de soma A + B. Gostaria de ajuda vindo do código OCaml para esta função de exemplo. Depois de entender isso, espero ser capaz de generalizá-lo.