Lambda the Ultimate

Thought some people might find this interesting. Years ago in the LFCS I was talking to Mike Fourman about Lisp and ML and the eval function and how I liked eval; he said 'What is the type of eval?'. I had no answer. Years later I can answer :).

In Shen, eval exists as a function that takes lists and evaluates them. so (* 3 4) gives 12 and [* 3 4] is a heterogeneous list w.o. a type in virgin Shen. If you apply eval to a list structure you get the normal form of the expression you would get by replacing the [...]s in the argument by (...)s.

e.g (eval [* 3 4]) = (* 3 4) = 12

Let's call these arguments to eval terms. Now some terms raise dynamic type errors to eval and some do not. So what we'd like is a class of terms that are well typed. We'll define term as a parametric type so [* 3 4] : (term number).

Using sequent calculus notation in Shen we enter the type theory. See the introductory video here (http://shenlanguage.org/) if you don't understand this notation.

(datatype term

  T1 : (term (A --> B));
  T2 : (term A);
  __________________
  [T1 T2] : (term B);   
  
  \\ some clerical stuff skipped here 
  X : (term A) >> Y : (term B);
  ______________________________
  [lambda X Y] : (term (A --> B));  
  
  if (not (cons? T))
  T : A;
  ______________________
  T : (mode (term A) -);)

So what is the type of eval?

eval : (term A) --> A. Surely?

Let's add this to the end of our data type definition

  _______________________
  eval : ((term A) --> A);

and run it.

Shen, copyright (C) 2010-2017 Mark Tarver
www.shenlanguage.org, Shen Professional Edition 17
running under Common Lisp, implementation: SBCL
port 2.1 ported by Mark Tarver
home licensed to Mark Tarver

(0-) (datatype term

  T1 : (term (A --> B));
  T2 : (term A);
  __________________
  [T1 T2] : (term B);   
  
  \\ some clerical stuff skipped here 
  X : (term A) >> Y : (term B);
  ______________________________
  [lambda X Y] : (term (A --> B));  
  
  if (not (cons? T))
  T : A;
  ______________________
  T : (mode (term A) -);

  _________________________
  eval : ((term A) --> A);)
type#term

(1-) (tc +)  \\ enable type checking
true

(2+) (* 3 4)
12 : number

(3+) ((* 3) 4)
12 : number

(4+) (eval [[* 3] 4])
12 : number

(5+) (eval [[* 3] "a"])
type error

(6+) [* 3]
[* 3] : (term (number --> number))

(7+) (eval [* 3])
# CLOSURE (LAMBDA (V1852)) {1006925DFB} : (number --> number)

(8+) [lambda X [lambda Y X]]
[lambda X [lambda Y X]] : (term (B --> (A --> B)))

(9+) (eval [lambda X [lambda Y X]])
# FUNCTION (LAMBDA (X)) {1006B5799B} : (B --> (A --> B))

You only need a few more rules to complete the term data type and add currying on the fly, but I'll leave it there. This was a byproduct of a much more extensive project I'm working on wrt to a typed 2nd order logic; but I thought it was fun to share.

bw

Mark