;; The first three lines of this file were inserted by DrScheme. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#lang plai
; Lecture Notes 
; Programming Languages and Types
; 
; October 21, 2009
; Instructor: Sebastian Erdweg
; Lecture notes by Klaus Ostermann

; Use this file with DrScheme and the PLAI language level

; Based on PLAI by Shriram Krishnamurthi

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; F1WAE features first-order functions

; let's go higher-order - meaning that functions can accept or return other 
; functions as values

; functions will also be *first-class* values, meaning that they have all
; the "rights" of other values (such as: storage in variables etc.)

; This implies that functions are (possibly) anonymous

; Changed grammar:

; <FWAE> ::= <num> 
;          | {+ <FWAE> <FWAE> }
;          | {with {<id> <FWAE> } <FWAE> }
;          | <id>
;          | {fun {<id>} <FWAE>}
;          | {<FWAE> <FWAE>}

; The corresponding data-type is:

(define-type FWAE
  [num (n number?)]
  [add (lhs FWAE?) (rhs FWAE?)]
  [with (name symbol?) (named-expr FWAE?) (body FWAE?)]
  [id (name symbol?)]
  [fun (param symbol?) (body FWAE?)]
  [app (fun-expr FWAE?) (arg-expr FWAE?)])


; With higher-order functions, we do not need the first-order function dictionary
; from F1WAE (why?)

; Now let's write the corresponding interpreter

; First, we will write a substitution-based interpreter again

; Here is the substitution function

(define (subst e1 x e2)
  (type-case FWAE e1
     [num (n) e1]
     [add (l r) (add (subst l x e2) (subst r x e2))]
     [with (z e3 e4)
           (if (symbol=? z x)
               (with z (subst e3 x e2) e4)
               (with z (subst e3 x e2) (subst e4 x e2)))]
     [id (y) (if (symbol=? x y) e2 (id y))]
     [app (f a) (app (subst f x e2) (subst a x e2))]
     [fun (param body) 
          (if (symbol=? param x)
              e1
              (fun param (subst body x e2)))]))



; What is the contract of "interp"? What should it return?

(define-type FWAE-Value
  [numV (n number?)]
  [funV (param symbol?) (body FWAE?)])

(define (val2expr val)
  (type-case FWAE-Value val
     [numV (n) (num n)]
     [funV (p b) (fun p b)]))

; interp: FWAE -> Value
(define (interp expr)
  (type-case FWAE expr
    [num (n) (numV n)]
    [add (l r) (numV (+ (numV-n (interp l)) (numV-n (interp r))))]
    [with (bound-id named-expr bound-body) (interp (subst bound-body bound-id (val2expr (interp named-expr))))]
    [id (v) (error 'interp "unbound identifier")]
    [fun (bound-id bound-body) (funV bound-id bound-body)]
    [app (fun-expr arg-expr)
       (let ((fun-val (interp fun-expr))
             (arg-val (interp arg-expr)))
          (interp (subst (funV-body fun-val) (funV-param fun-val) (val2expr arg-val))))]))





; Tests

(define test1 
  (with 'x (num 3)
         (with 'f (fun 'y (add (id 'x) (id 'y)))
               (with 'x (num 5)
                     (app (id 'f) (num 4))))))


(test (interp test1) (numV 7))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; In FWAE we can encode "with" using the other language primitives

; How?

; (with x t1 t2) ~> (app (fun x t2) t1)

; Hence, in FWAE "with" is a typical example of "syntactic sugar":
; it is convenient, but it can easily be encoded using other language constructs

; In the study of PLs, syntactic sugar only distracts from the important aspects
; Hence, in the future we will assume that syntactic sugar is added through preprocessors
; or other mechanisms not in the scope of this lecture

; The remaining language is basically the untyped lambda calculus

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; Talking about encodings:

; *Currying* is a technique by which a multi-parameter function can be
; encoded as a single-argument higher-order function

; Let's curry the function
; add-and-double: x y -> (x+y) + (x+y)

(define add-and-double
  (lambda (x y)
    (+ (+ x y)  (+ x y))))


; add-and-double-curry: x -> (y -> (x+y) + (x+y))

(define add-and-double-curry
  (lambda (x)
    (lambda (y)
      (+ (+ x y)  (+ x y)))))

; The reverse process is called *uncurrying*