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  2618 reads

Browse archivesActive forum topics 
Recent comments
39 min 34 sec ago
19 hours 52 min ago
20 hours 18 min ago
21 hours 13 min ago
1 day 54 min ago
1 day 23 hours ago
1 day 23 hours ago
5 days 12 hours ago
6 days 2 hours ago
6 days 5 hours ago