Variant bindings are weird

[brendanzab]

At the moment variants do some spooky injection of their constructors into the environment. For example the following will add Some and None to the environment, along with Option:

type Option a =
    | Some a
    | None

This doesn't seem consistent with the type construct, which normally behaves like a regular binding, albeit at the type level.

[brendanzab]

This is how the crazy 1ml encodes it:

type OPT =
{
  type opt a;
  none 'a : opt a;
  some 'a : a -> opt a;
  caseopt 'a 'b : opt a -> (() -> b) -> (a -> b) -> b;
};
Opt :> OPT =
{
  type opt a = wrap (b : type) => (() -> b) -> (a -> b) -> b;
  none 'a = wrap (fun (b : type) (n : () -> b) (s : a -> b) => n ()) : opt a;
  some 'a x = wrap (fun (b : type) (n : () -> b) (s : a -> b) => s x) : opt a;
  caseopt xo = (unwrap xo : opt _) _;
};
include Opt;

¯\_(⊙︿⊙)_/¯

[Marwes]

It seems like 1ml also injects the constructors though? I'd be open for a less spooky solution though.

Maybe remove the injection of the constructors and provide the constructor through projection?

type Option a =
    | Some a
    | None
Option.Some
Option.None

And force the user to explicitly bring the constructors into scope

// May need a different syntax
let { Some, None } = Option

type { Some, None } = Option // ??

[brendanzab]

I was thinking that actually. But then Option would be both a type and recordy thingy. Maybe that would be ok though...