Hidden arguments in abstract syntax

[PeterLjunglof]

Hidden arguments a la Agda/Cayenne is nice.

E.g., lights are both switchable and dimmable:

fun light : (dev:DeviceType) -> Device(dev);

The first argument has to be in the lin definition, unused:

lin light _ = ...

Better would be to be able to say that DeviceType is a hidden argument, e.g.:

fun light : (dev:DeviceType) |-> Device dev;
lin light = ...

Another example, with both hidden and ordinary arguments:

fun request : (menu:Menu) |-> Action menu -> Utterance;
lin request act = "i want to" ++ act ++ "please";