Início / coding / Perguntas / 77105070
Accepted
glennsl
Asked: 2023-09-14 20:52:49 +0800 CST

Coerção de subtipo com módulos de primeira classe

  • 772

Dadas as seguintes assinaturas de módulo, onde Bsubsumes A:

module type A = sig
  type t
end

module type B = sig
  type t
  val x: t
end

Normalmente, qualquer módulo que satisfaça Btambém satisfará A. No entanto, isso não se estende automaticamente aos módulos de primeira classe, porque é claro que é uma linguagem de tipo diferente que não permite a unificação automática com subtipos. Mas a coerção manual ainda deveria funcionar, não deveria? (Na verdade, isso acontece se as assinaturas do módulo contiverem apenas definições de tipo, mas não se contiverem valores.)

let f (_: (module A)) = ()
let g (b: (module B)) = f (b :> (module A)) (* Error: Type (module B) is not a subtype of (module A) *)

Esta é uma limitação fundamental dos módulos de primeira classe? Quais são as regras que determinam se um tipo de módulo é um subtipo de outro na linguagem de tipo principal? E existe uma solução prática?

types

2 respostas

  1. Best Answer

    A coerção de tipo é uma operação somente em nível de tipo no OCaml. Em outras palavras, espera-se que seja autônomo em tempo de execução.

    Para preservar esta propriedade, a subtipagem para módulos de primeira classe precisa usar um relacionamento restrito de subtipagem de módulo: (module A)<: (module B)se e somente se A<:Be todos os componentes de tempo de execução de ambos os tipos de módulo aparecerem na mesma posição.

    Por exemplo, isso é bom:

    module type A = sig
  type x = int
  type y = float
  val x : x
  val y :y
end
module type B = sig
  val x:int
  val y:float
end
let f (x:(module A) list) = (x:>(module B) list)

    porque ambos os tipos de módulo concordam que o primeiro componente de tempo de execução é xe o segundo é y. Ao contrário

    module type C = sig
  val y:int
  val x:float
end
let f (x:(module C) list) = (x:>(module B) list)

    falha porque os dois tipos de módulo discordam na posição dos campos xe y.

    • 1

  2. Para responder à minha própria pergunta sobre uma solução prática, é claro que é possível descompactar e reembalar o módulo. E neste exemplo simples isso é bastante conveniente:

    let g (module B: B) = f (module B)

    É um pouco menos conveniente quando o módulo de primeira classe está incorporado em alguma estrutura de dados.

    • 0

relate perguntas