►Hack Your Own Language
▼Assignments
•7 — Simple Types (b)
7.0.0.13
    ← prev  up  next → 

7 — Simple Types (b)

Draft

Due Tuesday, 27 Feb; 9:00am

Delivery Send me a zip file named 7-lastname1-lastname2.zip with your solutions. The zip archive should contain a single directory called 7-lastname1-lastname2, which in turn contains two files, each starting as follows:
; Problem Set 7
; Lastname1, Firstname1
; Lastname2, Firstname2
The two files should be named

  • lang.rkt, for the revised language implementation,

  • client.rkt, for the revised language client file,

The directory may contain other files.

image

Here are the grammar descriptions of the network flow programming languages, slightly revised from 6 — Simple Types (a).

Types
  t = Edge
  | Node
  | Weight
  | Path
  | [Listof t]
  | (t -> t)

Programs
p = (define x t e) ... n ... q

Nodes

  n = (node x e ...)

Questions

  q = (solve x x e)

Expressions
  e = x
  | (λ ({x : t}) e)
  | (e e)
  | (if0 e e e)
  | w
  | (o e e)
  | argmax
  | argmin
  | (edge x e)
  | (edge-to e)
  | (edge-cost e)
  | (cons e e)
  | (first e)
  | (rest e)
  | (empty t)
  | (empty? e)
  | (path e e)
  | (path-cost e)
  | (path-list e)
     
  o = +
  | -
  | *
  | /
See figure 3 for a (somewhat nonsensical but syntactically comprehensive) sample program.

; — the definitions
(define maximizer
  ((Path -> Weight) -> ([Listof Path] -> Path))
  (λ ({f (Path -> Weight)})
     (λ ({p* [Listof Path]})
        (path (if0 (empty? p*) 0 (path-cost ((argmax f) p*)))
          (empty Node)))))
(define to-b
  Edge
  (edge b 10))
(define to-c
  Edge
  (edge c 20))
(define to-both
  [Listof Edge]
  (cons to-b (cons to-c (empty Edge))))
 
; — the network
(node a to-both)
(node b (edge d 30))
(node c (edge d 30))
(node d)
 
; — the question
(solve a d maximizer)

Figure 3: A Sample Program

The Type System

We want to make sure that programs p are well-typed. Since the data definition for programs refers to Nodes, Questions, and Expressions, the design recipe dictates that the specification of the type system needs four judgments:

  • (⊢p p), read as "without context, program p is provably well-typed"

  • (⊢n G n), read as "in type context G, we can prove node specification n well-typed"

  • (⊢q G q), read as "in type context G, we can prove question q well-typed"

  • (⊢e G e t), read as "in type context G, we can prove expression e has type t"

Note that the first three judgments do not need to prove that a phrase has a specific type. It is understood that they establish that the phrase’s components are well-typed or have appropriate types. Also, the last three judgments need contextual information, which represents in left-to-right order the typed variable declarations encountered on the way from the program to the specific phrase within the program.

The specific type rules follow. They imply scoping rules.

Typing Programs

   (⊢e G e_d t_d) ...

   (⊢n G n) ...

   (⊢q G q)

   where G = ({x_d t_d} ... {x_n Node} ...)

   --------------------------------------------------------- p

   (⊢p (define x_d t_d e_d) ...

        n = (node x_n e_n ...) ...

        q)

Typing Nodes

   (⊢e G e_n Edge) ...

   --------------------------------------------------------- node-seq

   (⊢n G (node x_n e_n ...))

   

   (⊢e G e_n [Listof Edge])

   --------------------------------------------------------- node-list

   (⊢n G (node x_n e_n))

The first rule deals with a node specification where each outgoing edge is specified individually; the second one allows programmers to "insert" an entire list of outgoing edges (probably specified in separate definition as in the above example in figure 3).

Typing Queries

   (⊢e G x_from Node)

   (⊢e G x_to   Node)

   (⊢e G e      t)

   where t = ((Path -> Weight) -> ([Listof Path] -> Path))

   --------------------------------------------------------- question

   (⊢q G (solve x_from x_to e))

Typing Expressions

Core computational constructs

   where ((x_1 t_1) ... (x t) (x_2 t_2) ...) = G

   --------------------------------------------------------- variable

   (⊢e G x t)

   

   where t = ((Path -> Weight) -> ([Listof Path] -> Path))

   --------------------------------------------------------- argmax

   (⊢e G argmax t)

   

   (where t = ((Path -> Weight) -> ([Listof Path] -> Path)))

   --------------------------------------------------------- argmin

   (⊢e G argmin t)

   

   (⊢e ((x t_dom) (x_1 t_1) ...) e t_rng)

   --------------------------------------------------------- lambda

   (⊢e ((x_1 t_1) ...) (λ ({x t_dom}) e) (t_dom -> t_rng))

   

   (⊢e G e_fun (t_dom -> t_rng))

   (⊢e G e_arg t_dom)

   --------------------------------------------------------- fun-app

   (⊢e G (e_fun e_arg) t_rng)

   

   (⊢e G e_con Weight)

   (⊢e G e_thn t)

   (⊢e G e_els t)

   --------------------------------------------------------- if0

   (⊢e G (if0 e_con e_thn e_els) t)

Weights

   --------------------------------------------------------- lit-const

   (⊢e G w Weight)

   

   (⊢e G e_1 Weight)

   (⊢e G e_2 Weight)

   --------------------------------------------------------- operations

   (⊢e G (o e_1 e_2) Weight)

Edges

   (⊢e G e Weight)

   (⊢e G x Node)

   --------------------------------------------------------- edge

   (⊢e G (edge x e) Edge)

   

   (⊢e G e Edge)

   --------------------------------------------------------- edge-cost

   (⊢e G (edge-cost e) Weight)

   

   (⊢e G e Edge)

   --------------------------------------------------------- edge-to

   (⊢e G (edge-to e) Node)

Lists

   (⊢e G e_1 t)

   (⊢e G e_2 [Listof t])

   --------------------------------------------------------- cons

   (⊢e G (cons e_1 e_2) [Listof t])

   

   --------------------------------------------------------- empty

   (⊢e G (empty t) [Listof t])

   

   (⊢e G e [Listof t])

   --------------------------------------------------------- empty?

   (⊢e G (empty? e) Weight)

   

   (⊢e G e [Listof t])

   --------------------------------------------------------- first

   (⊢e G (first e) t)

   

   (⊢e G e [Listof t])

   --------------------------------------------------------- rest

   (⊢e G (rest e) t)

The rules for typing lists use a common trick in mathematics: use a meta-variable (here t) to say that these types can be anything as long as they are the same. This avoids repetitive specifications even if the specified language lacks abstraction (for this facility) and the programmer will have to produce repeated code.

Paths

   (⊢e G e_1 Weight)

   (⊢e G e_2 [Listof Node])

   --------------------------------------------------------- path

   (⊢e G (path e_1 e_2) Path)

   

   (⊢e G e Path)

   --------------------------------------------------------- path-cost

   (⊢e G (path-cost e) Weight)

   

   (⊢e G e Path)

   --------------------------------------------------------- path-list

   (⊢e G (path-list e) [Listof Node])

Tasks

  1. Implement the typed network flow language using the libraries and macro-defining conventions that Stephen Chang developed during lecture.

  2. Place the sample program from figure 3 into a separate client file and make sure it type checks.

    ← prev  up  next →