### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# PROGRAMMING LANGUAGES COMP 311

Rice University

GPA 3.72

### View Full Document

## 7

## 0

## Popular in Course

## Popular in ComputerScienence

This 12 page Class Notes was uploaded by Cleora Stiedemann on Monday October 19, 2015. The Class Notes belongs to COMP 311 at Rice University taught by Staff in Fall. Since its upload, it has received 7 views. For similar materials see /class/224956/comp-311-rice-university in ComputerScienence at Rice University.

## Similar to COMP 311 at Rice University

## Reviews for PROGRAMMING LANGUAGES

### What is Karma?

#### Karma is the currency of StudySoup.

#### You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 10/19/15

Type Systems COMP 311 Rice University Houston Texas COMP 311 Tme Systems a Type Systems for Programming Language were invented by mathematicians before electronic computers were invented What is a type A meaningful subset of the set of the domain of data values used in a program Types are used to describe the intended behavior of program operations The concept is derived from mathematics functions have specified domain and codomains sets which are often called types In fact a function with domain A and codomain B is often said to have type A gt B Moveover the variables used in mathematical formulas typically have specified types Mathematicians informally check that uses of functions and variables in formulas are respected just as they informally check that reasoning used in proofs is sound In computer programs some forms of type checkingquot can be formalized and automated COMP 311 Type Systems 6 a Foundation type systems for functional languages 0 Canonical functional language the A calculus Mii Cl X l MM l Ml0 c E C a set of constants X E V a set of variables 80 the A calculus is really a family of languages that differ only in the constants and variables 0 A simple type system for the A calculus Atype has the form 3952 b r gtc b E B a set of base types Augmented language syntax M c X ll1M MIT M COMP 311 3 Type Systems Typing rules for the simply typed A calculus Each constant c E C has a given type xc Since an expression M inside a A calculus program may contain free variables type rules keep track of the types of these variables using a type environment P E V x T where Tdenotes the set oftypes 395 This type environment is simply a symbol table that records a symbol s type Assume MO gt 39c and N 0 Then M N 395 Assume X 0 implies that M 395 Then M o M o gt 39c The process of assigning types to A calculus programs can be rigorously formalized as a natural deduction system where the formal sentences are typing judgements ofthe form F M 39c and the mechanisms for generating true sentences are axioms ofthe form F M 39c and inference rules of the form I i Mi2m I MMum gt I Mc COMP 311 Type Systems Explanation 0 Axioms are typing judgements that are manifestly true 0 Inference rules produce true consequences given true premises 0 Common notation for rules F1 Mi El By MNI EN I M 395 Natural deduction rules for simply typed A calculus F is arbitrary F XI39E X 395 F l C xlcl F MO gt 395 F N10 gt elimination or application F M N 395 o F X10 Mr gt introduction or abstraction I Mid M G gt1 COMP 311 Type Sys tem s Example A calculus language 0 C I U F where I 2 1 0 1 2 FI 0 Va b z aa 0 Bint 0 xiintforiEI xfint gtGnt gtint 0 What is type of M int gt int Ag int gt int M int fgx Gnt gtint gt Gnt gtint gt int gtint which is the curried form of Gnt gtint x int gtint gt int gtint COMP 311 Type Systems Sample Typing Proof Show Q M int gtint Ag int gtint Mint fg X int gtint gt int gtint gt int gtint Tree1 fint gtint g int gtint Xint g int gtint fint gtint g int gtint Xint IX int fint gtint g int gtint Xint g X int Tree2 fint gtint g int gtint Xint fint gtint Tree1 fint gtint g int gtint Xint fg 0 int fint gtint g int gtint A Xint fg X int gtint fint gtint A g int gtint A Xint fg X int gtint gt int gtint Q A fint gtint A g int gtint A Xint fg X int gtint gt int gtint gt int gtint COMP 311 Type Sys tem s Question what is the relationship between the untyped A calculus and the simply typed Acalculus 7 Many expressions and complete programs in the untyped A calculus cannot be typed in the simply typed A calculus Example Ax x x x requires atype o o a 1 but no such type exists 7 lfthe constant operations terminate for all inputs then every typable program terminates for all inputs Question is there a tractable algorithm for determining the type of an expression in the untyped Acalculus and rejecting the expression if no such type exists Yes The standard algorithm called the type reconstruction algorithm is based on a very simple idea generate a distinct type variable for every subexpression of the given expression M record the equality constraints between these variables dictated by the typing rule that matches the program context in which the subexpression associated with each variable appears and s COMP 3slolve these constraints Type Sys tem s More details Create only one type variable for each distinct program variable all occurrences of a given variable must have the same type Create a compound type variable 0 a 1 for each subexpression that appears as the head M of an application M N For each constant c assign it the type xc Every subexpression now has a symbolic type For each application M N where M has symbolic type 0 a 1 equate o with the symbolic type of N and equate 1 with the symbolic type of M N For each abstraction Ax M where x has symbolic type 0 and M has symbolic type 1 equate o a 1 with the symbolic type of Ax M Solve the resulting set of equations on symbolic types which are just symbolic expressions that can be represented as trees using the uni cation algorithm invented by John Alan Robinson a professor of philosophy at Rice in the 1960 s The generated solution is a substitution mapping type variables to symbolic types COMP 311 Type Sys tem s What is unification Tree pattern matching where match variables only appear as leaves A na39I39ve recursive algorithm can be written in afew lines of Scheme r ML The common practical algorithm relies on a unionfind representation of finite sets to record equivalent symbolic types Every set contains at least one symbolic type that is just a variable This algorithm runs in essentially lineartime A linear algorithm exists but it is not as efficient for problems of practical size as the unionfind based algorithm Question is the reconstructed type unique Many Acalculus programs have multiple typings Consider the program Ax X It can be assigned the type 0amp0 for any type 0 E T eg int int int in a in a in The type reconstruction algorithm deftly addresses this problem by returning the most general symbolic typing all of the possible ground typings containing no type variables are substitution instances of this typing For this reason the typing produced by the type reconstruction algorithm is called the principal typing ortype of the program COMP 311 Type Sys tem s Robin Milner s Creative Leaps COMP 311 The simple type system for the Acalculus is truly onerous because polymorphic functions those with variables in their principal types have to be rewritten for each different typing The original Pascal language suffers from precisely this problem Milner recognized that a surprisingly useful form of polymorphism could be added to the simply typed Acalculus by adding a let construct to the language family The extension adds one new form to the family syntax M let x M M Given an expression of the form let X M N x can be used polymorphically in N without breaking the principal typing property Type reconstruction can first infer the principal type of M and subsequently use a renamed version of this type a fresh name for each distinct type variable for each distinct occurrence of x in N Type Sys tem s Robin Milner s Creative Leaps continued E planation in essence the definition ofx is treated like a macro abbreviation that is replicated for each occurrence of x in N Of course a language imp emen tion only needs one copy of he code for M provided that all the different instantiations of the principal type use the same data layout Example In our simple A language let i Ax x i i2 2 In a richer language of the family let append A xy if empty x y cons first x append rest x y append cons append cons 1 empty cons 2 empty empty empty Note empty and cons are polymorphic constants let is recursive 7 Milner also realized he could rigorously prove a that typable programs cannot generate certain errors Type reconstruction proves that runtime typeerrors cannot occur provided that we define the notion of type error rather narrowly A similar theorem holds for Java we think COMP 311

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

## Why people love StudySoup

#### "I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"

#### "When you're taking detailed notes and trying to help everyone else out in the class, it really helps you learn and understand the material...plus I made $280 on my first study guide!"

#### "I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"

#### "It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.