Re: Actual arguments in ADTs

[Natarajan Shankar <shankar@csl.sri.com>]

> 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

1. There is a workaround.  Drop the freeVars parameter and define the
datatype as
Exp[Ident: TYPE+]: DATATYPE
 BEGIN
  vref(ident: Ident): vref?
  app(rator: Exp, rand: Exp): app?
  lam(formal: Ident, 
      body: Exp): lam?
 END Exp

The Ident : TYPE+ allows the ASSUMING to be dropped. 
Then define a predicate term? as
Expression[Ident: TYPE+]: THEORY
 BEGIN

  IMPORTING Exp[Ident]

  term?(fvars: set[Ident])(e : Exp[Ident]): RECURSIVE bool
   = (CASES e OF
      vref(i): member(i, fvars),
      app(f, a): term?(fvars)(f) AND term?(fvars)(a),
      lam(i, a): term?(add(i, fvars))(a)
      ENDCASES)
 MEASURE e BY <<

END Expression

 The type (term?(fvars)) captures the notion of a term over a set
of free variables fvars.

2. The reason for excluding this kind of construction is that the datatype
declaration generates a collection of parametric theories, and this
couldn't done if the parameter is allowed to vary through a recursion.

-Shankar