LAMP: Exercise 5 Records and Subtyping

Exercise 5 Records and Subtyping

English only

Administrative Issue: This is the last exercise session before graded assignments begin. You might want to use the session to ask any questions about the things you learned up to now.

Exercise 5 Records and Subtyping

In this informal grammar, label and x stand for arbitrary identifiers. In records, the key-value pairs are separated with a comma.

Source Language

Internal Language

Values

E ::= x  
      E E   
      \x: T.E  
      true  
      false
      zero
      succ E
      pred E
      iszero E
      if E then E else E
      let x = E in E
      let rec x: T = E in E
      E.label
      { label_i = E_i ^i∈1..n }

 T ::= Num
       Bool
       T->T
       { label_i: T_i ^i∈1..n }
       Top

E ::= x 
      E E    
      \x: T.E  
      true   
      false
      zero
      succ E             
      pred E             
      iszero E           
      if E then E else E 
      fix E
      let x = E in E
      E.label
      { label_i = E_i ^i∈1..n }

T ::= Num
       Bool
       T->T
       { label_i: T_i ^i∈1..n }
       Top

V ::=  BV
       NV
       \x: T.E 
      { label_i = V_i ^i∈1..n }

BV ::= true   
       false

NV ::= zero   
       succ NV

Derived Forms
let rec f:T = E₁ in E₂ --> let f = fix \f:T.E₁ in E₂

In this exercise, we add records, like this one { x=3, foo=true } which is of type { x: Int, foo: Boolean }, and a most general type Top.

The new tree nodes are (from Expr.scala)

// records
case class Record(inf: Int, content:List[Pair[String,Expr]]) extends Expr;
case class Select(inf: Int, e:Expr, n:String) extends Expr;

case class  TyRecord(keys:List[Pair[String,Type]]) extends Type;
case object TyTop extends Type;

Again, the first parameter inf is only for error messages.

Careful: Records are represented an an ordered list of key-value pairs! But we want them to be unordered, such that the above example would be the same as { foo=true, x=3 }. You must be careful not to assume any particular order when dealing with records.

Note: We use the symbol |- for the algorithmic typing and subtyping relations, for readability. The book uses a a different symbol for declarative and algorithmic definitions of typing.

(algorithmic) Typing

Γ |- true: Bool

 
 Γ |- false: Bool

 
 Γ |- zero: Num

x: T ∈ Γ 

Γ |- x: T

Γ |- E: Num

Γ |- pred E: Num

Γ |- E: Num

Γ |- succ E: Num

Γ |- E: Num

Γ |- iszero E: Bool

Γ |- E1: Bool  E2: T   E3: T

Γ |- if E1 then E2 else E3: T

Γ, x: T1 |-  E: T2

Γ |- \x: T1. E: T1->T2

Γ  |- E1: T1 -> T2   Γ  |- E2: T   T <: T1

Γ |- E1 E2: T2

Γ |-  E1: T1   Γ, f: T1 |- E2:T2

Γ |- let f = E1 in E2: T2

Γ |-  E: T -> T

Γ |- fix E : T

Γ |-  E: { labeli:Ti }

Γ |- E.labeli : Ti

Γ |-  Ei: Ti for each i

Γ |- { labeli = Ei }: { labeli:Ti }

(algorithmic) Subtyping

S <: Top
Num <: Num
Bool <: Bool

T₁ <: S₁ S₂ <: T₂

S₁ -> S₂ <: T₁ -> T₂

{ Alabeli i∈1..n } subset of { Blabelj  j∈1..m }

                Blabelj = Alabeli implies Sj <: Ti
              

{ Blabelj: Sj j∈1..m } <: { Alabeli: Ti  i∈1..n }

Only the highlighted sections of the type system are new. Algorithmic subtyping is specified by the contra-co-variant rule for functions, and the rule for records. The record rule checks at the same time whether a record has more fields and whether a field has a subtype.

Good news: You need not implement an Evaluator in this exercise. Just for information, here are the new computation and congruence rules for records and field selection:

{ labeli = Vi i∈1..n }.labeli → Vi

E  →  E'

E.label  → E'.label

E  → E'

{label1=V1...labeli-1=Vi-1,labeli = E...}  → {label1=V1...labeli-1=Vi-1,labeli = E'...}

Task 5.1

Download the partial implementation and complete the missing cases in src/subrec/TypeChecking.scala

You can test with scala subrec.Main test\*.sub. All tests except ifjoin.sub and err*.sub should pass.

Task 5.2

Refine the typing rule with joins and meets, such that we can give do better typechecking for "if"

Γ |- E1: Bool  E2: T2   E3: T3  

T2 ∨ T3 = T

Γ |- if E1 then E2 else E3: T

Add functions meet(s:Type, t:Type):Type and join(s:Type, t:Type):Type that compute the meet ∧ and the join ∨ of two types. Here is their mutually recursive definition

S ∨ T =

Bool	if S = T = Bool
Num	if S = T = Num
S₁ ∧ T₁ `->` S₂ ∨ T₂	if S = S₁ `->` S₂, T = T₁ `->` T₂
{j_l:J_l^l∈1..q}	S = {k_j:S_j^j∈1..m}, T = {l_i:T_i^i∈1..n} {j_l^l∈1..q} = {k_j^j∈1..m} intersect {l_i^i∈1..n} J_l = S_j ∨ T_i for each j_l=k_j=l_i
Top	otherwise

S ∧ T =

S	if T = Top
T	if S = Top
Bool	if S = T = Bool
Num	if S = T = Num
S₁ ∨ T₁ `->` S₂ ∧ T₂	if S = S₁ `->` S₂, T = T₁ `->` T₂
{m_l:M_l^l∈1..q}	S = {k_j:S_j^j∈1..m}, T = {l_i:T_i^i∈1..n} {m_l^l∈1..q} = {k_j^j∈1..m} union {l_i^i∈1..n} M_l = S_j ∧ T_i for each j_l=k_j=l_i M_l = S_j if m_l=k_j only occurs in S M_l = T_i if m_l=l_i only occurs in T
fail	otherwise

Verify that ifjoin.sub works with your adapted typechecker.

Tips

There are several ways to manipulate lists. You will need to use one in order to handle the contents of records.

Nested recursive functions These are functions that take a list as an argument, and make a pattern match. For nonempty lists, they handle the case x::xs, where x is an element and xs is a list. For empty lists, they return some neutral value. Nested functions can be defined anywhere, in particular also inside other functions. For instance, here is a function that could transform a List[Pair[String,Expr]] into a List[Pair[String,Type]]

   def doSomething(li: List[Pair[String,Expr]]): List[Pair[String,Type]] = 
        li match {
          case Pair(key,value)::xs => ... :: doSomething( xs )
          case Nil => Nil;
        }
   val newList = doSomething(myList)

using map and higher-order functions. All recursive functions to map a list like above are very similar. Using map one can type a bit less and achieve the same:

   val newList = myList.map { x => ... }

for-comprehensions. To do something for each element in a list, one can write

   for(val c <- myList) { ... }

The results of the body are thrown away, and the whole "for" returns nothing (has type Unit). If you want the results of the body to be saved and concatenated to a list, you can use

   val newList = for(val c <- myList) yield { ... }

Iterators. If you call the elements method of a list, you get an iterator, which can be traversed with a while loop.

  val it = myList.elements; while( it.hasNext ) {
    val c = it.next;
    ...
  }

The good thing about iterators is that they have a find method which takes a boolean function. This can help finding an entry in a list, like here

val myList:List[Pair[String,Type]] = ...;
myList.elements.find { x => x._1 == "foo" } match {

  case Some(Pair(_,tpe)) =>
    ... myList contains the Pair("foo",tpe)...

  case _ =>
    ... myList does not contain an entry for "foo"

}