Use of phantom types

[polytypic]

Currently Picos uses phantom types to both prevent certain unsafe operations from being done accidentally and to document the intentions and restrictions of the design (but not necessarily strictly prevent programming errors).

For example, the trigger type

picos/lib/picos/picos.mli

Line 347 in 07d6c2d

type -'allowed t

includes the 'allowed type variable. The on_signal operation on triggers requires the trigger to allow On

picos/lib/picos/picos.mli

Lines 402 to 407 in 07d6c2d

	val on_signal :
	[> `On | `Signal ] t ->
	'x ->
	'y ->
	([> `Signal ] t -> 'x -> 'y -> unit) ->
	bool

which is only given through an await call

picos/lib/picos/picos.mli

Line 365 in 07d6c2d

val await : [> `Await ] t -> Exn_bt.t option

that performs the Await effect

picos/lib/picos/effects_intf.ocaml5.ml

Lines 32 to 34 in 07d6c2d

	type _ Effect.t +=
	private
	| Await : [ `On | `Signal ] t -> exn_bt option Effect.t

passing the trigger allowing On to the scheduler.

This way only a scheduler may call on_signal on a trigger, which is how triggers are intended to work: the scheduler attaches a
resume action to the trigger that will then be called when the trigger is signaled. Making it so that only the scheduler may call on_signal allows the trigger implementation to be simpler, faster, and safer. There is no need to have a list of actions and the caller of signal can be relatively certain that any action attached (via on_signal or by the Picos framework itself) is safe to call from any context.

The phantom types do not guard from all potential bugs or misuse. You can e.g. locally install a handler for Await and then call on_signal on the trigger or you can simply use an unsafe cast. This requires a bit of effort and is unlikely to happen entirely accidentally.

The downside of the phantom typing scheme is that it makes it more cumbersome to program with triggers (and other Picos concepts), which is a feedback communicated to me. I agree. The phantom types do make the types more complex and require some extra care to handle. On the other hand, the phantom types do prevent some simple mistakes and also document some of the intentional restrictions formally.

The question is, should we just remove the phantom types and replace them with documentation?

I don't have a strong opinion on this except that the intentions and constraints do need to be communicated somehow.

[c-cube]

I'd suggest returning multiple values that have different capabilites instead of using phantom types, indeed. A trigger could have the await-er side (what is currently Trigger.t and a separate opaque type to signal it, typically only used by the scheduler. Internally these two types (and the two values when creating the trigger) are the same.