Declaration of parameters in sequences of named parameters

[ppolesiuk]

When specifying long lists of named parameters, e.g., when defining signatures of functor-like functions, some type schemes of named parameters often quantify over some type for similar purpose. For instance, in the Map module we have the following code.

pub data MapSig Key = Map of
  { T : type -> type
  , empty : {Val} -> T Val
  , singleton : {Val} -> Key -> Val -> T Val
  , method add : {Val} -> T Val -> Key -> Val ->[] T Val
  ...
  }

All defined values are polymorphic in Val type—the type of values stored in map. In order to avoid clutter, we could add the parameter construct at the level of named parameters, analogous to the parameter declarations at the level of definitions. With this feature, the above code could be simplified to the following.

pub data MapSig Key = Map of
  { T : type -> type
  , parameter Val
  , empty : T Val
  , singleton : Key -> Val -> T Val
  , method add : T Val -> Key -> Val ->[] T Val
  ...
  }

Such a construct makes sense for type parameters only: the type parameter is added to the scheme, when declared type is used. Extending the construct for implicit/value parameters is tempting (for instance, to avoid repetition of ~onError), however, the semantics of such parameters is not clear.