User loginNavigation 
archivesthe type of eval in ShenThought 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) 20102017 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 By Mark Tarver at 20170515 16:21  LtU Forum  login or register to post comments  other blogs  2549 reads

Browse archivesActive forum topics 
Recent comments
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 4 days ago
2 weeks 4 days ago
2 weeks 6 days ago
3 weeks 4 hours ago
3 weeks 4 days ago
3 weeks 5 days ago