Polymorphic variants & constraints

Learning
1

Hi,

I’ve been trying to figure out how use polymorphic variants and constraints to enforce the ordering of application of an algebraic data type.

In my code, below, I only want to allow the data constructor Three to be applied when the constructor Two has already been applied at least once. So

Three(3,Two(2,One 1))

and

Three(4,Two(3,Two(2,One 1)))

would type check, but

Three(2,One 1)

would not.

My understanding of polymorphic variants was that [> Two] meant a lower bound but the compiler does not complain when I construct Three(2,One 1).

How would I achieve the desired effect?

Thanks,

Michael

type 'a atLeastOne = [> `One] as 'a
type 'a atLeastTwo = [>  `Two] as 'a
type 'a atLeastThree = [>  `Three] as 'a

type 'a t = 
  | One : int -> 'a atLeastOne t
  | Two : (int * 'a atLeastOne t ) -> 'a atLeastTwo t
  | Three : (int * 'a atLeastTwo t)  -> 'a atLeastThree t
  
let x = One(1)
let y = Two(2,x)
let z = Three(3,x)
2

That’s because the input of the constructor should be “at most”, not “at least”. You want “at most” `Two | `One in your input.

type 'a t = 
  | One : int -> [> `One] t
  | Two : (int * [< `Two | `One] t ) -> [> `Two] t
  | Three : (int * [< `Two] t)  -> [> `Three] t
  
let x = One(1) (* ok *)
let y = Two(2,One 1) (* ok *)
let y' = Two(3,Two(2, One 1)) (* ok *)
let z = Three(3,One 1) (* not ok *)
let z' = Three(3,y) (* ok *)
let z'' = Three(4,Three(3,y)) (* not ok *)
2 Likes
3

Here is an alternative that doesn’t use polymorphic variants and will accept the definition of z'' from @Drup’s example:

type true_ = T
type false_ = F

type ('has_two, 'has_three) n =
| One : int -> (false_, false_) n
| Two : int * (_, 'a) n -> (true_, 'a) n
| Three : int * (true_, _) n -> (true_, true_) n

let x = One(1) (* ok *)
let y = Two(2,One 1) (* ok *)
let y' = Two(3,Two(2, One 1)) (* ok *)
let z = Three(3,One 1) (* not ok *)
let z' = Three(3,y) (* ok *)
let z'' = Three(4,Three(3,y)) (* ok *)

Note that 'has_three can be removed in this definition, but that if you want to add a Four case then it can be useful to have and will allow things like Four(5,Two(4,Three(3,Two(2,One(1))))).
If the invariant you want is that a constructor is always applied to an argument with the same constructor or one lower, then @Drup’s solution is closer to what you want.

4

You can make z'' accepted in the poly-var solution by a very short change in the definition of the Three constructor, to mimick what is done in Two.

In general, you can turn most polymorphic variant based solutions to these kind of issues into pseudo-sets (like those fake booleans) and parametric polymorphism. It gets fairly annoying after 3 or 4 cases unfortunately …

Finally: there is an alternative solution to all this: Just Split Your Type :wink:

1 Like