[Caml-list] Lack of an empty variant type

[Caml-list] Lack of an empty variant type

[François Pottier]

Hello,

I was surprised today to see that this code is rejected:

# let f (x : [< `A]) = ();;
val f : [< `A ] -> unit = <fun>

# let g (x : [< `B]) = ();;
val g : [< `B ] -> unit = <fun>

# fun b x -> if b then f x else g x;;
Error: This expression has type [< `A ]
        but an expression was expected of type [< `B ]
        These two variant types have no intersection

The type-checker rejects this code, even though it is safe,
and its type should be [< ] -> unit, where [< ] is the empty
variant type.

I imagine that the type-checker wants to be my friend and
wants to prevent me from defining a useless function.

However, in the real use case I have in mind, I am abusing
polymorphic variants to encode sets at the type level, and
the lack of an empty set is painful!

Just a random remark,

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

Re: [Caml-list] Lack of an empty variant type

[François Pottier]

Le 17/11/2020 à 02:02, Jacques Garrigue a écrit :
> Can’t you work around that by adding a dummy element to your sets?

Hi Jacques, yes, I can; but it adds visual clutter to types that
are already difficult to read. Not a big deal, I guess.

-- 
François Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/