Homework Assignment 4 Solution

    • Assignment Policies

Collaboration Policy. It is acceptable for students to collaborate in understanding the material but not in solving the problems or programming. Use of the Internet is allowed, but should not include searching for existing solutions.

Under absolutely no circumstances code can be exchanged between students from di erent groups. Excerpts of code presented in class can be used.

    • Assignment

In this assignment you are asked to extend the type-checker for the language REC with references, pairs, lists and trees. The interpreter is provided for you. This assignment is organized in four parts:

    1. Part 1. Add type-checking for references.

    2. Part 2. Add type-checking for pairs.

    3. Part 3. Add type-checking for lists.

    4. Part 4. Add type-checking for trees.

The new language including all these constructs will be called CHECKED PLUS.


    • Type-Checking References

One new grammar production, which is added to the parser for CHECKED PLUS, is needed for the concrete syntax of expressions.


<Expression>    ::=    ()

The concrete syntax of types must be extended so as to allow the typing rules described below to be implemented. Two new productions are added, the one for unit and for ref:




1


<Type>
::=
int
<Type>
::=
bool
<Type>
::=
unit
<Type>
::=  ref(<Type>)
<Type>
::=
(<Type> -> <Type>)

The typing rules are:

‘ e :: t

‘ newref(e) :: ref(t)

‘ e :: ref(t)

‘ deref(e) :: t


‘ e1 :: ref(t)    ‘ e2 :: t


‘ setref(e1,e2) :: unit


‘ () :: unit

Note the use of the type unit, to indicate that the return result of the assignment operation is not important.

3.1    Task

You have to update the code for the type checker by adapting the    le checker.ml of the

CHECKED language to EXPLICIT-REFS so that type_of_expr can handle :


let    rec    t y p e _ o f _ e x p r  :  expr    ->  texpr    t e a _ r e s u l t  =  function

    • ...

|  Unit    ->  return    UnitType

    • ...

|  NewRef ( e )  ->  error  " I m pl em e nt    me!"

    • |  DeRef ( e )  ->  error  " I mp l em en t  me!"

|  SetRef ( e1 ,  e2 )  ->  error  " Im p le me n t  me!"

Here are some examples:

1
#
chk
" let
x
=
newref (0)  in  deref (x)" ;;




-
:  texpr  Checked . ReM . result  =  Ok  IntType
3
#
chk
" let
x
=
newref (0)  in  x" ;;




-
:  texpr  Checked . ReM . result  = Ok  ( RefType  IntType )
5
#
chk
" let
x
=
newref (0)  in  setref (x ,4)" ;;




-
:  texpr  Checked . ReM . result  =  Ok  UnitType
7
#
chk
" newref ( newref ( zero ?(0))) " ;;




-
:  texpr  Checked . ReM . result  = Ok  ( RefType  ( RefType  BoolType ))
9
#
chk
" let
x
=
0  in  setref (x ,4) " ;;





-
:  texpr
Checked . ReM . result  =  Error  " setref :  Expected  a  re f er en ce  type "









    • Pairs

4.1    Concrete syntax

Two new productions are added to the grammar of CHECKED PLUS:



2


<Expression>    ::=    pair(<Expression>,<Expression>)

<Expression>    ::=    unpair (<Identi er>,<Identi er>)=<Expression> in <Expression>

Some examples of programs using pairs follow:


pair (3 ,4)

2

pair ( pair (3 ,4) ,5)

4

pair ( zero ?(0) ,3)

6

pair ( proc  ( x : int )  {  x  -  1  } ,  4)

8

proc  ( z : < int * int >)  {  unpair  (x , y )= z  in  x  }

10

proc  ( z : < int * bool >)  {  unpair  (x , y )= z  in  pair (y , x )  }

12

let  f  =  proc  ( z : < int * bool >)  {  unpair  (x , y )= z  in  pair (y , x )  }

    14 in  ( f  pair (1 ,  zero ?(0)))

Note that the concrete syntax of the types is also extended with a new production:

<Type>
::=
int
<Type>
::=
bool
<Type>
::=
unit
<Type>
::=  ref(<Type>)
<Type>
::=
(<Type> -> <Type>)
<Type>
::=
<<Type> * <Type>>

Regarding the behavior of these expressions they are clear. For example, the expression (proc (z:<int*int>) unpair (x,y)=z in x pair(2, 3)) is a function that given a pair of integers, projects the rst component of the pair.

4.2    Task

Add two new cases to the de nition of the function type_of_expr in the    le checker.ml:


let    rec    t y p e _ o f _ e x p r  :  expr    ->  texpr    t e a _ r e s u l t  =  function

    • ...


|
Pair ( e1 , e2 )  ->  error  " Im p le me n t
me!"
4
|
Unpair ( id1 , id2 , e1 , e2 )  ->  error
" I mp le m en t  me!"





You    rst need to devise the appropriate typing rules!

Here are some examples:


#
chk  " pair (2 ,  3)" ;;







2
-
:  texpr  Checked . ReM . result  =  Ok  ( PairType  ( IntType ,  IntType ))

#
chk  "( proc  (z: < int *int >)  { unpair  (x,y)=z
in  x}  pair (2 ,
3)) ";;





4
-
:  texpr  Checked . ReM . result  =  Ok  IntType



#
chk  "( proc  (z:int )  { unpair
(x,y)=z
in  x}
pair (2 ,  3)) " ;;






6
-
:  texpr  Checked . ReM . result
=  Error
" unpair :  Expected  a
pair  type "














3

    • Lists

5.1    Concrete syntax

The concrete syntax for expressions should be extended with the following productions:

<Expression>
::=
emptylist <Type>
<Expression>
::=  cons (<Expression>, <Expression>)
<Expression>
::=  null? (<Expression>)
<Expression>
::=  hd (<Expression>)
<Expression>
::=
tl (<Expression>)

The concrete syntax for types includes one new production (the last one listed below):

<Type>
::=
int
<Type>
::=
bool
<Type>
::=
unit
<Type>
::=  ref(<Type>)
<Type>
::=
(<Type> -> <Type>)
<Type>
::=
<<Type> * <Type>>
<Type>
::=
list(<Type>)

The new type constructor is for typing lists. For example,

    1. list(int) is the type of lists of integers

    2. (int -> list(int)) is the type of functions that given an integer produce a list of integers.


Here are some sample expressions in the extended language. They are supplied in order to help you understand how each constructor works.


#
chk
" em pt y li st  int " ;;





2
-
:  texpr  Checked . ReM . result  =  Ok  ( ListType  IntType )








4
#
chk
" cons (1 ,  em pt y li st
int )" ;;









-
:  texpr  Checked . ReM . result
=  Ok  ( ListType
IntType )
6




















#
chk
"hd( cons (1 ,
e mp t yl is t
int ))" ;;



8
-
:  texpr  Checked . ReM . result  =  Ok  IntType












10
#
chk
"tl( cons (1 ,
e mp t yl is t
int ))" ;;









-
:  texpr  Checked . ReM . result
=  Ok  ( ListType
IntType )
12

















#
chk
" cons ( null ?( e mp ty l is t
int ) ,  e mp ty l is t  int )" ;;







14
-
:  texpr  Checked . ReM . result  =




Error
" cons :  type
of
head
and  tail  do  not
match "

16






















#
chk
" proc (x: int )
{
proc
(l: list (int ))  {
cons (x,l)
}  }";;






18
-
:  texpr  Checked . ReM . result  =




Ok
( FuncType  ( IntType ,  FuncType  ( ListType
IntType ,
ListType  IntType )))












Here are the typing rules:



4


5.2    Typing rules





‘ e1 :: t
‘ e2 :: list(t)
‘ emptylist t :: list(t)




‘ cons(e1,e2) :: list(t)

‘ e :: list(t)


‘ e :: list(t)


‘ tl(e) :: list(t)

‘ hd(e) :: t

‘ e :: list(t)

‘ null?(e) :: bool


5.3    Task

Extend the type-checker to del with the new constructs:


    • let  rec  t y p e _ o f _ e x p r  :  expr  ->  texpr  t e a _ r e s u l t  =  function

...

3
|
E mp t yL is t ( t )
->
error
" I mp le m en t
me!"

|
Cons ( he ,  te )
->
error
" I m pl em e nt
me!"

    • |  Null ( e )  ->  error  " I mp le m en t  me!"

    • Hd ( e )  ->  error  " Im pl e me nt  me!"

7|  Tl ( e )  ->  error  " Im pl e me nt  me!"


    • Trees

6.1    Concrete syntax

The concrete syntax for expressions should be extended with the following productions:

<Expression>
::=
emptytree <Type>
<Expression>
::=  node (<Expression>, <Expression>, <Expression>)
<Expression>
::=  nullT? (<Expression>)
<Expression>
::=  getData (<Expression>)
<Expression>
::=  getLST (<Expression>)
<Expression>
::=
getRST (<Expression>)

The concrete syntax for types includes one new production (the last one listed below):

<Type>    ::=

<Type>    ::=

<Type>    ::=

<Type>    ::=

<Type>    ::=

<Type>    ::=

<Type>    ::=

<Type>    ::=

int

bool

unit

ref(<Type>)

(<Type> -> <Type>)

<<Type> * <Type>>

list(<Type>)

tree (<Type>)

Here is a sample program that assumes you have implemented the append operation on lists. Note that you will not be able to run this program unless you have extended the


5


interpreter to deal with lists and trees. This assignment only asks you to write the type-checker, not the interpreter. You are, of course, encouraged to write the interpreter too!
Here is another example.    It should type-check with result    and

evaluate to Ok (ListVal [NumVal 1; NumVal 2; NumVal 3]):


letrec    append ( xs : list ( int )):    list ( int )  ->  list ( int )    =

    • proc  ( ys : list ( int ))  {


if  null ?( xs )



4
then
ys

else
cons ( hd ( xs ) ,(( append  tl ( xs ))  ys ))




    • }

in

    • letrec  inorder ( x : tree ( int )): list ( int )   =

if    nullT ?( x )

    10 then  e mp ty li s t  int

else  (( append  ( inorder    getLST ( x )))    cons ( getData ( x ) ,

    12 ( inorder  getRST ( x ))))

in

    14 ( inorder  node (2 ,


node (1 , e mp t yt re e
int , e m pt yt r ee
int ) ,




16
node (3 , e mp t yt re e
int , e m pt yt r ee
int )))





6.2    Typing rules


‘ emptytree t :: tree(t)

‘ e :: tree(t)

‘ getData(e) :: t

‘ e :: tree(t)

‘ getLST(e) :: tree(t)



‘ e1 :: t    ‘ e2 :: tree(t)    ‘ e3 :: tree(t)


‘ node(e1,e2,e3) :: tree(t) ‘ e :: tree(t)

‘ nullT?(e) :: bool ‘ e :: tree(t)

‘ getRST(e) :: tree(t)


6.3    Task

Extend the type-checker to del with the new constructs:


let    rec    t y p e _ o f _ e x p r  :  expr    ->  texpr    t e a _ r e s u l t  =  function

    • ...


|
E mp t yT re e ( t )  ->  error  " I mp le m en t  me!"






4
|
Node ( de ,
le ,
re )
->  error  " Im pl e me nt  me!"

|
NullT ( t )
->
error
" I mp l em en t  me!"







    • |  GetData ( t )  ->  error  " Im pl e me nt  me!"

    • GetLST ( t )  ->  error  " I m pl em e nt  me!"

8|  GetRST ( t )  ->  error  " I m pl em e nt  me!"


Here are some sample expressions in the extended language. They are supplied in order you to help you understand how each construct works.


#
chk  " em pt y tr ee  int
" ;;





2
-
:  texpr
Checked . ReM
. result  =
Ok
( TreeType
IntType )

4
#
chk  " nullT ?( node (1 ,
node (2 ,

e mp t yt re e  int ,
e mp ty t re e  int ) ,  e mp ty t re e  int ))" ;;











-
:  texpr
Checked . ReM
. result
=
Ok
BoolType














6


6

















#
chk
" getData ( node (1 ,  node (2 ,
e m pt yt r ee  int ,  e mp t yt re e  int ) ,  e mp t yt re e
int ))"
;;
8
-
:  texpr
Checked . ReM . result
=  Ok  IntType


10
#
chk
" getLST ( node (1 ,
node (2 ,
e mp t yt re e  int ,  e mp ty t re e  int ) ,  e mp ty t re e
int ))" ;;










-
:  texpr
Checked . ReM
. result
=
Ok  ( TreeType  IntType )















    • Submission instructions

Submit a le named HW3 <SURNAME>.zip through Canvas which includes all the source les required to run the interpreter and type-checker. Your grade will be determined as follows, for a total of 100 points:



Section
Grade




Unit
5




Reference
15




Pair
20




List
30




Tree
30





































7