Reputation: 4931
I would like to switch some of my types to use Ocaml polymorphic variants, factoring them with open recursion, whilst still retaining the enforcement of my existing private non-polymorphic types, as well as the exhaustiveness checks on pattern matches.
My product is a compiler so the set of types is changed by various algorithms, at present I have to include all the constructors with the ones that shouldn't occur "assert false"ed out.
I should add I used to use polymorphic variants but switched back to ordinary ones because type inference doesn't play well with polymorphic variants: the error messages are hard to read and they're wrong a lot more than the usual bad inferences, requiring a lot more type annotations on parameters to retain any sanity. The problem is without them, enforcement by private constructors is strong but enforcement for client algorithms is weak.
I'm not really sure if it's possible or practical to combine "ad hoc" subsets of constructors with privacy. Any suggestions as to how practical it is?
EDIT: simple example types:
(* open *)
type 'a x' = [`A | `B of 'a]
(* closed *)
type x = private 'u x' as 'u
(* open extension *)
type 'a y' = ['a x' | `C of 'a]
(* closed extension *)
type y = private 'u y' as 'u
let mkA () = `A
let mkB' (a:'a x') = `B a
(* how to do this? *)
let mkB (a:x) = mkB' (a :> 'a x')
With open recursion the constructor functions have to follow the open/closed pattern of the types. The client is only going to see the closed versions. Which means, unlike my current system where a single constructor function is enough, i now need one for each closed type, for each type the constructor is contained in.
Even if I can figure out how to do this, which is pretty hard if you have say 6 mutually dependent types ALL of which use open recursion, leading to an exponential explosion of possible combinations, its not clear whether this is an advantage compared to just accepting run time checks. It takes me about 2 hours to add a new constructor because every pattern match fails with an exhaustiveness fault and has to be fixed .. even if the new constructor has no use in that phase of compilation.'
Upvotes: 4
Views: 240
Reputation: 237
Private polymorphic variant are only interesting with module and interfaces. They are puclic in the module, but private outside thanks to the interface. If outside the module you want to be have access to the public representation, then you have to provide the function to do it:
module M : sig
(* open *)
type 'a x' = [`A | `B of 'a]
(* closed *)
type x = private 'u x' as 'u
val f: x -> x x'
end = struct
type 'a x' = [`A | `B of 'a]
type x = 'u x' as 'u
let f a = a
end
Another way to have it is to change a bit your type, making only the head constructor private:
(* open *)
type 'a x' = [`A | `B of 'a]
(* closed *)
type x = 'u x' as 'u
(* private *)
type px = private x
let f (a: px) = (a :> x)
Upvotes: 1