# Polymorphic variants & constraints

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)``````

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

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.

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 1 Like