Changes between Version 3 and Version 4 of PIL

Timestamp:

10/03/24 16:06:01 (20 months ago)

Author:

siegel

Comment:

--

PIL

@@ -44 +44 @@
 - Type definitions: `typedef typename ID;`
 
+== Functions
+
+There are two kinds of functions in PIL:
+1. Imperative functions = "procedures"
+1. Logic functions
+
+=== Procedures
+
+Like in C.  These can be nested.  Obviously they can have side-effects, be nondeterministic, and the behavior can depend on non-local state.  A procedure call `f(x1,...,xn)` is an expression that can be used anywhere an expression with side-effects is allowed.  Imperative procedures are not values and cannot be assigned to anything.  However, as in C, a pointer to a procedure is a first-class value that can be assigned, used as an argument, returned, etc.   There is a procedure type, exactly like C's function type, e.g.,
+{{{
+       typedef int(int) i2i;
+}}}
+defines `i2i` to be the type "procedure consuming int and returning int".  Most commonly, pointers to procedure types will be used, e.g.,
+{{{
+       typedef int(int)* i2ip;
+}}}
+defines the type "pointer to procedure from int to int".  As in C, a pointer to a procedure can be used in a procedure call.
+
+A procedure definition can be templated:
+{{{     
+       <T1,T2,...> <procedure def>
+}}}   
+This defines one procedure for each assignment of types to the Ti.
+     
+=== Logic functions
+
+Typically specified by a $lambda expression. These are first-class objects in PIL: they can be assigned to variables, passed as an argument in a function call (including a procedure call), and can be returned by a function.  Each has a type of the form `$fun<U,T1,...,Tn>` (functions from `T1` x ... x `Tn` to `U`).  They are side-effect-free.  An application of a logic function `f(x1,...,xn)` is an expression that can be used anywhere an expression is allowed.  A logic function is not necessarily pure, i.e., the value of an application may depend on any part of the state, not just the arguments.
+  
+=== Lambda expressions
+
+There are two kinds of lambda expressions.  The first kind defines a procedure, the second a logical function.
+
+Procedural lambda syntax:
+{{{
+  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) { S1; ... }
+}}}
+where
+* the `Ti` and `Uj` are types
+* the `xi` and `vj` are variables
+* R is a type (the return type), which may be void
+* {S1; ...} is a block (same as in function definition)
+* the only variables that can occur free in the block are the xi and vj
+* if R is not void, the block must return a value of type R
+
+The type of this expression is `R(T1, ..., Tn)`.
+
+Logic function lambda syntax:
+{{{
+  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) expr
+}}}
+where 
+* the `Ti` and `Uj` are types
+* the `xi` and `vj` are variables
+* R is a type (the return type), which cannot be void
+* `expr` is a side-effect-free expression of type R 
+* the only variables that can occur free in `expr` are the xi and vj
+
+The type of this expression is `$fun<R, T1, ..., Tn>`. 
+
+In both cases, the initializer expressions `initj` are expressions using any variables in scope.
+
+==== Semantics
+
+FIX THIS:  difference between logic and procedural functions...
+
+
+
+The lambda expression is evaluated to yield a *closure*:  an ordered pair consisting of a dyscope and an expression.  The dyscope has variables `v1`, ..., `vm`, initialized by evaluating `init1`, ..., `initm`.  The dyscope has no parent scope, it is associated only with the closure.  The expression is `expr`.  The dyscope is destroyed whenever it becomes unreachable, i.e., whenever no part of the state is assigned the closure.
+
+A logic function application `f(e1,...,en)` is evaluated by first evaluating the arguments `ei`, then assigning the `ei` to the `xi` and evaluating expr in the closure dyscope.  Note that since expr has no side effects, the values of the xi are constant.  [Note: a possible change is to allow side-effects in logic functions.]
+
 == Tuples
 
@@ -125 +196 @@
 - `void $map_addAll($map<K,V> * this, $map<K,V> that);`
 
-== Functions
-
-There are two kinds of functions in PIL:
-1. (Imperative) procedures
-1. Logic functions
-
-=== Procedures
-
-Like in C.  These can be nested.  Obviously they can have side-effects, be nondeterministic, and the behavior can depend on non-local state.  A procedure call `f(x1,...,xn)` is an expression that can be used anywhere an expression with side-effects is allowed.  Imperative procedures are not values and cannot be assigned to anything.  However, as in C, a pointer to a procedure is a first-class value that can be assigned, used as an argument, returned, etc.   There is a procedure type, exactly like C's function type, e.g.,
-{{{
-       typedef int(int) i2i;
-}}}
-defines `i2i` to be the type "procedure consuming int and returning int".  Most commonly, pointers to procedure types will be used, e.g.,
-{{{
-       typedef int(int)* i2ip;
-}}}
-defines the type "pointer to procedure from int to int".  As in C, a pointer to a procedure can be used in a procedure call.
-
-A procedure definition can be templated:
-{{{     
-       <T1,T2,...> <procedure def>
-}}}   
-This defines one procedure for each assignment of types to the Ti.
-     
-=== Logic functions
-
-Typically specified by a $lambda expression. These are first-class objects in PIL: they can be assigned to variables, passed as an argument in a function call (including a procedure call), and can be returned by a function.  Each has a type of the form `$fun<T1,...,Tn;U>` (functions from `T1` x ... x `Tn` to `U`).  They are side-effect-free.  An application of a logic function `f(x1,...,xn)` is an expression that can be used anywhere an expression is allowed.  A logic function is not necessarily pure, i.e., the value of an application may depend on any part of the state, not just the arguments.
-  
-=== Lambda expressions
-
-There are two kinds of lambda expressions.  The first kind defines a procedure, the second a logical function.
-
-Procedural lambda syntax:
-{{{
-  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) { S1; ... }
-}}}
-where
-* the `Ti` and `Uj` are types
-* the `xi` and `vj` are variables
-* R is a type (the return type), which may be void
-* {S1; ...} is a block (same as in function definition)
-* the only variables that can occur free in the block are the xi and vj
-* if R is not void, the block must return a value of type R
-
-The type of this expression is `R(T1, ..., Tn)`.
-
-Logic function lambda syntax:
-{{{
-  $lambda [U1 v1=init1; ... Um vm=initm;] R (T1 x1, ..., Tn xn) expr
-}}}
-where 
-* the `Ti` and `Uj` are types
-* the `xi` and `vj` are variables
-* R is a type (the return type), which cannot be void
-* `expr` is a side-effect-free expression of type R 
-* the only variables that can occur free in `expr` are the xi and vj
-
-The type of this expression is `$fun<R, T1, ..., Tn>`. 
-
-In both cases, the initializer expressions `initj` are expressions using any variables in scope.
-
-==== Semantics
-
-FIX THIS:  difference between logic and procedural functions...
-
-
-
-The lambda expression is evaluated to yield a *closure*:  an ordered pair consisting of a dyscope and an expression.  The dyscope has variables `v1`, ..., `vm`, initialized by evaluating `init1`, ..., `initm`.  The dyscope has no parent scope, it is associated only with the closure.  The expression is `expr`.  The dyscope is destroyed whenever it becomes unreachable, i.e., whenever no part of the state is assigned the closure.
-
-A logic function application `f(e1,...,en)` is evaluated by first evaluating the arguments `ei`, then assigning the `ei` to the `xi` and evaluating expr in the closure dyscope.  Note that since expr has no side effects, the values of the xi are constant.  [Note: a possible change is to allow side-effects in logic functions.]
 
 == Heaps