Início / coding / Perguntas / 77588230
Accepted
Travis
Asked: 2023-12-02 05:42:03 +0800 CST

Retornando um tipo de soma sem nome

  • 772

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.

ocaml

1 respostas

  1. Best Answer

    Não faz muito sentido dizer que você deseja definir um tipo local para uma função. O corpo de uma função é uma expressão, ou seja, é feito de valores e não de tipos. Você pode definir um tipo em um módulo que seja local para uma função. Mas os construtores definidos no módulo não podem escapar do escopo da função.

    # 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

    Usando um tipo definido globalmente, sua função é fácil de escrever:

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

let f (a, b) = Left a

    Aqui está uma aplicação da função:

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

    Não acho que ajude usar GADTs ou variantes polimórficas. Eles são complicados, mas não permitem a violação das regras de escopo, que são uma coisa diferente.

    Você pode usar o sistema de módulos OCaml para definir um tipo abstrato, se desejar. Torne o tipo e a função locais para um módulo.

    • 1

relate perguntas