Actual arguments in ADTs

["Steven E. Ganz" <sganz@cs.indiana.edu>]

It seems both safe and useful to allow components of ADTs accepting
actual parameters to modify the parameters from those given.  As an
example, I would like lambda calculus expressions to be typed with a 
set of potential free variables.  Then, judgements about the effects 
of various syntax-manipulating functions on free variables of an
expression can be stated to avoid repetition in proofs.

I'd like to write the following ADT, but get an error message that
actual parameters are not permitted for locally defined objects.

Exp[Ident: TYPE, freeVars: setof[Ident]]: DATATYPE
 BEGIN
  ASSUMING
   identNonempty: ASSUMPTION (EXISTS (i:Ident): TRUE)
  ENDASSUMING

  vref(ident: {i:Ident|member(i, freeVars)}): vref?
  app(rator: Exp, rand: Exp): app?
  lam(formal: Ident, 
      body: Exp[Ident, union(freeVars, singleton(formal))]): lam?
 END Exp  

Is this an enhancement that might be considered, and is there any
work-around?

Steve Ganz