In the video "The Most Beautiful Program Ever Written" Byrd derives (define eval-expr (lambda (expr env) (pmatch expr [,x (guard (symbol? x)) (env x)] [(lambda (,x) ,body) (lambda (arg) (eval-expr body (lambda (y) (if (eq? x y) arg (env y))))))] [(,rator) (,rand) ((eval-expr rator env) (eval-expr rand env))]))) He points out that it has lexical scope and higher-order functions. At a glance it is obvious that the program is the lambda calculus x | lambda x | (e1 e2) but it also has an interesting wrinkle in the environment encoding (aka Gamma) in that the 'env' argument is an expression that captures local scope, aka data, in a lambda binding. Since it is recursive the environment is built and scoped as closures in the 'env' argument. It seems straightforward to add types (as lambda expressions, not as the traditional symbol form like alpha, etc.). Depending on how they get handled in closures they could be static or dynamic. But McCarthy raises an issue of data. From McCarthy "Towards a Mathematical Science of Computation" "Procedures are usually built up from elementary procedures. What these elementary procedures may be, and how more complex procedures are constructed from them, is one of the first topics in computer science. This subject is not hard to understand since there is a precise notion of a computable function to guide us, and computability relative to a given collection of initial functions is easy to define. Procedures operate on members of certain data spaces and produce members of other data spaces, using in general still other data spaces as intermediates. A number of operations are known for constructing new data spaces from simpler ones, but there is as yet no general theory of representable data spaces comparable to the theory of computable functions." Most of the treatments I've seen fall back upon set theory to handle Gamma, such as saying that items to the left of a turnstile are sets or that imperative program actions modify a set of known variables. The closest I've seen to a theory of "representable data spaces" occurs in the Let Over Lambda book Are you aware of any references that focus on a "theory of representable data spaces" that does not involve sets? Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
it's called intuitionistic type theory On Sat, Sep 15, 2018 at 04:47 Tim Daly <[hidden email]> wrote:
(c) Robert Harper. All rights reserved.
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |