it's called intuitionistic type theory On Sat, Sep 15, 2018 at 04:47 Tim Daly <axiom...@gmail.com> wrote:
> In the video "The Most Beautiful Program Ever Written" > https://www.youtube.com/watch?v=OyfBQmvr2Hc > > 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" > http://www-formal.stanford.edu/jmc/towards.ps 1997 > > "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 > https://letoverlambda.com/ > > Are you aware of any references that focus on a "theory of representable > data spaces" that does not involve sets? > > > Tim > > > > > > -- (c) Robert Harper. All rights reserved.
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
