[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Actual arguments in ADTs

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
   identNonempty: ASSUMPTION (EXISTS (i:Ident): TRUE)

  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

Steve Ganz