Sto scrivendo un controllo di tipo per un dialetto ML che implica la generazione di variabili di tipo "fresche" (nuove e univoche) "(valori che rappresentano le incognite). La mia strategia e la strategia che sembra essere utilizzata nelle esercitazioni è identificare le variabili di tipo con un numero intero univoco e mantenere un contatore incrementato ogni volta che viene generata una nuova variabile di tipo.
In precedenza, ho mantenuto il contatore come un campo mutabile di un tipo di record che rappresenta lo stato del controllo di tipo.
Il programma deve confrontare le variabili di tipo; lo fa confrontando i loro ID interi. Poiché i diversi stati di controllo dei tipi mantengono i propri contatori, è possibile confrontare le variabili di tipo generate da due diversi stati di controllo del tipo e renderle uguali. Questo è un uso improprio dell'API e non dovrebbe mai accadere.
type state =
{ mutable vargen : int
; (* Other fields... *) }
let fresh_tvar st =
st.vargen <- st.vargen + 1;
Type.Var.{ id = st.vargen - 1
; (* Other fields... *) }
let compare lhs rhs = compare lhs.id rhs.id
Per applicare meglio la correttezza, ho deciso di spostare il contatore dallo stato di tipo checker a un membro globale e privato del tipo variable module. Ora, le variabili di tipo distinte non possono mai essere uguali. Il codice al di fuori del modulo non può accedere al contatore o all'ID di una variabile di tipo; possono solo confrontare due variabili di tipo.
module type Var = sig
type t
val fresh : some_type -> some_other_type -> t
val compare : t -> t -> bool
end
module Var : Var = struct
type t = { id : int; (* Other fields... *) }
let counter = ref 0 (* Global mutable state not exposed in signature *)
let fresh some_arg some_other_arg =
counter := !counter + 1;
{ id = counter - 1
; (* Other fields... *) }
let compare lhs rhs = compare lhs.id rhs.id
end
Poiché lo stato globale mutabile è considerato dannoso (specialmente nella programmazione funzionale!), non sono sicuro che il mio nuovo codice sia valido.
- Lo stato globale mutabile è giustificato in questo contesto?
- Se il mio primo progetto è migliore, in generale, come posso far rispettare l'invariante che i valori generati da stati fisicamente separati non vengano usati insieme? (Un altro esempio di tale violazione, in C ++, sarebbe confrontare gli iteratori con contenitori diversi.)
- Lo stato del controllo di tipo è di per sé un singleton che si comporta come stato globale in tutto tranne il nome?
Sto usando OCaml, a proposito, se gli idiomi specifici della lingua influenzano la risposta alla mia domanda.