Skip to content

Latest commit

 

History

History
390 lines (278 loc) · 10.4 KB

notes.org

File metadata and controls

390 lines (278 loc) · 10.4 KB
Raw

Notes

Notes

[0/5]

  • [ ] Improve `cast’ function (n-ary functions)
    • [ ] Change n-ary to n partial applications
  • [ ] Type Checker for $λ→\langle τ \rangle$
  • [ ] Change ~ to work with pair and ->n types
  • [ ] Custom Reader
    • [ ] Read Scheme files
    • [ ] Cast, Type Check
    • [ ] Send to compiler : cf
  • [ ] Handle REPL

Useful environments

system-global-environment  ; use for redefining stuff
(the-environment)          ; needs to be called. use inside functions/macros (at top level)
                           ; i.e. bind inside a `let' fist
(nearest-repl/environment) ; needs to be called.

General pattern for redefining internal procedures

Get value from the environment

(define *symbol* (environment-lookup system-global-environment 'symbol))
(define-syntax symbol
  ...)

Scheme types we are concerned with

  • fixnum : an integer constant. e.g. 1
  • ratnum : a rational constant e.g. (/ 1 2)
  • flonum : a floating point constant e.g. 1.0
  • recnum : a complex number e.g. 3+4i
  • string : a string e.g. ("H")
  • character : a character e.g. #\c
  • pair : a cons cell e.g. (1 . 2)
  • list : a cons cell ending with the empty list e.g (1 2)
  • procedure : a lambda expression e.g. (lambda (x) x)
  • interned-symbol : a symbol
  • uninterned-symbol : a fresh symbol guaranteed to not exist in the environment

Getting run-time type information in MIT/Scheme

The expression is evaluated

(dispatch-tag expr)
(dispatch-tag-contents (dispatch-tag expr)) ; to view the contents

No-eval macro

quote is used to stop evalution.

(define-syntax no-eval
  (syntax-rules ()
    ((_ expr)
     (quote expr))))

Using the pattern matcher in linear-match

linear-match.scm contains the pattern matcher found at http://okmij.org/ftp/Scheme/macros.html#match-case-simple

Each pattern is required to have a guard. () is the empty guard. (,x) represents a variable. Will be bound as x if matched.

Examples

(define (sum-list ls)
  (match ls
    (() () 0) ; match with empty list
    ((,x . ,xs) (number? x) (+ x (sum-list xs)))))

Type consistency ~

All of this can be found in the file first.scm

Implements the following rules

$$τ ∼ τ$$

$$\frac{σ_1 ∼ τ_1 \qquad σ_2 ∼ τ_2}{σ_1 → σ_2 ∼ τ_1 → τ_2}$$

$$τ ∼ ?$$

$$? ∼ τ$$

(define (~ type1 type2)
  (cond ((or (any-type? type1) (any-type? type2)) #t)
	((equal? type1 type2) #t)
	((and (pair? type1) (pair? type2))
	 (and (~ (car type1) (car type2))
	      (~ (cdr type1) (cdr type2))))
	(else #f)))

Type Checker – typed-lambda

All of this can be found in the file first.scm

Implements the typing rule

$$\frac{Γ, x:σ \vdash e : τ}{Γ \vdash (λ x : σ . e) : σ → τ}$$

The typed-lambda form simply evaluates to a lambda expression for now. Later on, we will want to use type-check on the expression first.

Examples of typed-lambda

(define inc (typed-lambda (: x 'number) (+ x 1)))

(define len
  (typed-lambda (: x 'list)
		(if (null? x)
		    0
		    (+ 1 (len (cdr x))))))

(define apply-func
  (typed-lambda (: f '(-> any any))
		(typed-lambda (: x 'any)
			      (f x))))

(define (type-check expr type gamma)
  (match expr
    ...					; Lot more here

    (('typed-lambda (: ,x ,s) ,body) (arrow-type? type)
     (if (not (~ s (domain type)))
	 (error "Inconsistent parameter type -- " s 'with (domain type))
	 (let ((param-type s))
	   (make-arrow param-type
		       (type-check body
				   (codomain type)
				   (cons (cons x param-type) gamma))))))

    (__ () (error "Type checking failed -- " expr 'with type))))

Dealing with n-ary functions

$$σ →n τ ≡ \underbrace{σ × σ × … × σ}n → τ$$

Types

(->n number number)
(-> number (-> boolean any))
(->2 number boolean)
(-> (* number number) boolean)
(-> (* number boolean) string)

Typing Rules

Will have to rethink these rules. Approach now is to first cast Scheme expressions and then type-check

Variables

$$\frac{Γ(x) = σ}{Γ \vdash x : σ}$$

Abstractions

unary

$$\frac{Γ, x:σ \vdash M : τ}{Γ \vdash λ x:σ.M :σ → τ}$$

n-ary

$$\frac{Γ, x_1 : σ_1, x_2 : σ_2, …, x_n : σ_n \vdash M : τ}{Γ \vdash λ (x_1:σ_1,x_2:σ_2,…,x_n:σ_n).M : σ_1 × σ_2 × … × σ_n → τ}$$

$$\frac{Γ,x_ii∈1,…,n:σ \vdash M : τ}{Γ \vdash λ (x_1:σ,x_2:σ,…,x_n:σ).M : σ →n τ}$$

Application

$$\frac{Γ \vdash M : σ →_n τ \quad Γ \vdash N_ii ∈ 1,…,n : σ}{Γ \vdash (M N_1 N_2 … N_n) : τ}$$

Type Checking without Casting

The following passes the current type checker.

(type-check '((typed-lambda (:: x number) (+ x 1)) "H") 'any '())

There doesn’t seem to be a straightforward way to add the typed-lambda expression to the type environment (() here). Took a look at the main paper again, and it seems like casting is one way this issue can be avoided.

Casting to an Intermediate Language

This is probably the approach we should take. It is also the one described in “Gradual Typing for Functional Languages”

Cast Insertion

For right now, we’ll implement the following rules.

Rule for variables. $⌊ τ ⌋$ represents an optional type. We are going to set this to the any type as a default.

$$\frac{Γ x = ⌊ τ ⌋}{Γ \vdash x ⇒ x : τ}$$

Rule for predefined types and constants. Think +, *, >, <, and so on $$\frac{Δ c = τ}{Γ \vdash c ⇒ c : τ}$$

Rule for $λ$ $$\frac{Γ, x : σ \vdash e ⇒ e^’ : τ}{Γ \vdash λ x : σ . e ⇒ λ x : σ . e^’ : σ → τ}$$

Rule for application. The rules depend on the information available in $Γ$ $$\frac{Γ \vdash e_1 ⇒ e_1^’ : ? \quad Γ \vdash e_2 ⇒ e_2^’ : τ_2}{Γ \vdash e_1 e_2 ⇒ (\langle τ_2 → ? \rangle e_1^’) e_2^’ : ?}$$

$$\frac{Γ \vdash e_1 ⇒ e_1^’ : τ → τ^’ \quad Γ \vdash e_2 ⇒ e_2^’ : τ_2 \quad τ_2 ≠ τ \quad τ_2 ∼ τ}{Γ \vdash e_1 e_2 ⇒ e_1^’ (\langle τ \rangle e_2^’) : τ^’}$$

$$\frac{Γ \vdash e_1 ⇒ e_1^’ : τ → τ^’ \quad Γ \vdash e_2 ⇒ e_2^’ : τ}{Γ \vdash e_1 e_2 ⇒ e_1^’ e_2^’ : τ^’}$$

Casting Function

Will look something like this

(define (cast e Γ)
  (pmatch expr
    (,e (guard (symbol? e)) `(: e (lookup Γ e)))  
    ((λ (: ,x ,type) ,body) `(λ (: x type) (cast body (extend Γ x type))))
    ((,e1 . ,e2) ... rules for application)))

Cast expressions

The cast function should be idempotent.

Syntax is (: <expr> <type>)

(castu '(fn (: x number) x) '())
 => (: (fn (: x number) (: x number)) (-> number number))

(castu '(f x) '())
 => (: ((: f (-> any any)) (: x any)) any)

(castu '(f x) '((x . number)))
 => (: ((: f (-> number any)) (: x number)) any)

(castu '(is-zero? x) '((is-zero? . (-> number boolean))))
 => (: ((: is-zero? (-> number boolean)) (: x number)) boolean)

(castu '(f (x y)) '())
 => (: ((: f (-> any any)) (: ((: x (-> any any)) (: y any)) any)) any)

(castu '((f x) y) '())
 => (: ((: ((: f (-> any any)) (: x any)) (-> any any)) (: y any)) any)

The usual suspects

self application

OCaml

fun x -> x x;;
(* This expression has type 'a -> 'b but an expression was
   expected of type 'a. The type variable 'a occurs inside 'a -> 'b *)

Typed Racket

(lambda (x) (x x))
;; Type Checker: missing type for identifier;
(lambda ([x : (-> Any Any)]) (x x))
;; - : (-> (-> Any Any) Any)
(lambda ([x : (-> Any Any)]) (x (x x)))
;; - : (-> (-> Any Any) Any)

double/apply-twice

OCaml

fun f x -> f (f x);;
(* : - : ('a -> 'a) -> 'a -> 'a = <fun> *)

Typed Racket

(lambda ([f : (-> Any Any)] [x : Number]) (f (f x)))
;; - : (-> (-> Any Any) Number Any)
(lambda (f x) (f (f x)))
;; Type Checker: Cannot apply expression of type Any, 
;; since it is not a function type

different brach types for if

OCaml

fun x -> if x > 0 then 1 else false;;
(* Error: This expression has type bool but an expression was expected of type int *)

Typed Racket

(lambda ([x : Real]) (if (> x 0) 1 #f))
;; - : (-> Real (U False One))

different types in containers

OCaml

[1; false; "string"];;
(* This expression has type bool but an expression was expected of type int *)

Typed Racket

'(1 #f "string")
;; - : (Listof (U False One String)) [mode precisely: (List One False String)]

A note on self application

Typed Racket

Can write a function that performs self application, but we don’t get anything we can use from it

(define self-app (lambda ([x : (-> Any Any)]) (x x)))
(define iden (lambda (x) x))

(self-app iden) ; Type : Any ; Value : #<procedure:iden>
((self-app iden) 1) ; ERROR

Here is how it works in Scheme

(define self-app (lambda (x) (x x)))
(define iden (lambda (x) x))
(self-app iden) ; #<procedure>
((self-app iden) 1) ; 1

A note on DOUBLE in typed racket

(lambda ([f : (-> Any Any)] [x : Number])
  (f (f x)))
;; (-> (-> Any Any) Number Any)
(lambda ([f : (-> Any Number)] [x : Number])
  (f (f x)))
;; (-> (-> Any Number) Number Number)
(lambda ([f : (-> Number Any)] [x : Number])
  (f (f x)))
;; type mismatch, expected : Number, given : Any