\require{AMSsymbols} \require{AMSmath} \newcommand{\mathcd}[1]{\mathrm{#1}} \newcommand{\mathbcd}[1]{\mathrm{#1}} \newcommand{\mathbcd}[1]{\mathrm{#1}} \newcommand{\var}{\mathit{var}} \newcommand{\val}{\mathit{val}} \newcommand{\e}{\mathit{exp}} \newcommand{\n}{n} \newcommand{\x}{\mathrm{x}} \newcommand{\trueval}{\mathrm{true}} \newcommand{\falseval}{\mathrm{false}} \newcommand{\enum}[1]{\ulcorner\mathcd{#1}\urcorner} %\newcommand{\econst}[1]{\ulcorner{#1}\urcorner} \newcommand{\econst}[1]{{#1}} \newcommand{\efn}[3]{\mathcd{\backslash}{#1}\ \mathcd{::}\ {#2}\mathbcd{\ \rightarrow\ }{#3}} \newcommand{\eplus}[2]{{#1}\ \mathbcd{+}\ {#2}} \newcommand{\elt}[2]{{#1}\ \mathbcd{<}\ {#2}} \newcommand{\eif}[3]{\mathbcd{if}\ #1\ \mathbcd{then}\ #2\ \mathbcd{else}\ #3} \newcommand{\elet}[3]{\mathbcd{let}\ #1\ \mathbcd{=}\ #2\ \mathbcd{in}\ #3} \newcommand{\eapply}[2]{{#1}\,{#2}} \newcommand{\epair}[2]{\langle #1,#2\rangle} \newcommand{\efst}[1]{\mathbcd{fst}\ #1} \newcommand{\esnd}[1]{\mathbcd{snd}\ #1} \newcommand{\econs}[2]{#1\ \mathbcd{:}\ #2} \newcommand{\enil}[1]{\mathcd{nil}\ \mathcd{::}\ #1} \newcommand{\ecase}[5]{\begin{array}{rll}\mathbcd{case}\ #1\ \mathbcd{of} & \mathbcd{nil} & \mathbcd{\Rightarrow\ } #2 \\\ \mathbcd{|} & {#3}\mathbcd{:}{#4} & \mathbcd{\Rightarrow\ } #5\end{array}} \newcommand{\t}{\mathit{ty}} \newcommand{\G}{\Gamma} \newcommand{\wfe}[3]{\ #1\,\vdash\,#2\,::\,#3\ } \newcommand{\fe}[2]{\ #1\,::\,#2\ } \newcommand{\tarrow}[2]{#1 \rightarrow #2} \newcommand{\ttimes}[2]{(#1, #2)} \newcommand{\tpair}[2]{(#1, #2)} \newcommand{\tlist}[1]{[\;#1\;]} \newcommand{\tint}{\mathrm{int}} \newcommand{\tbool}{\mathrm{bool}} \newcommand{\infer}[2]{\frac{#2}{#1}} \newcommand{\AND}{\quad} \newcommand{\subtypeof}{\sqsubseteq}

Aside: Professors as Human Beings

Duty & Responsibility

SIGCSE Story

Overall gist, sometimes when you're looking around waiting for someone else to step up, you may realize it needs to be you.

Introduction to Types

What's this?

Consider

• 1617972849
• 1900965984
• 1.02223624099482e+30
• `pNq
• 恰乱
• ld h,b; ld (hl),b; ld c,(hl); ld (hl),c
• bra pc+0x70; nop
• call pc+0x81c139c4
• 01100000011100000100111001110001

What do these things have in common?

But most similarly, they all the same bit-sequence (hex 0x 60 70 4E 71) interpreted in different ways!

• Big-Endian Integer
• Little-Endian Integer
• IEEE 32-bit Floating Point
• ASCII/UTF-8
• UTF-16
• Z80 Assembly (8-bit instructions)
• m68k Assembly (16-bit instructions)
• x86 (variable-length instructions)

The same data can mean different things, depending on the type.

Types

What is a type?

• An abstraction.
• A definition of data and what can/cannot be done with it.
• Something that defines the representation of data (what to put in memory and how).
• A set of allowed values.
• A set of fundamental operators for these values.
• A label for humans.
• A context for the data
• A composition of other types.

What are types for?

• They help us catch programming errors.
• They allow compilers to generate more efficient code.
• They allow us to write code that is more expressive.
• They provide an interpretation for information.
• They provide restrictions on what we can do with information.
• Allow code optimization / generation

What is a type system?

• A system of rules that govern types.
• A system providing the behaviors of types with each other

What does it mean for a program to be "well-typed"?

Let's consider the variable x.

Is the following well-typed? let x = 1 in x+1

What about this? let x = true in x+1

Classifying Type Systems

We say that languages that catch the error at compile time are statically typed and that languages which catch the error at runtime are dynamically typed.

How Types Influence Meaning

Consider the example

"one" + 2

What could it mean? From that, extrapolate some of the distinguishing characteristics of different type systems.

Some possible results include:

• Error: Examples:
  • Unknown operation for those types
  • Ambiguous whether string should be cast to integer or vice-versa
• Note that errors can be either static (compile-time) or dynamic (run-time)
• "one2" - cast the 2 to a string and append
• ("one", 2) - put the string and the integer in a tuple
• "qne" - add two to the first character's ASCII code
• "qpg" - add two to all characters' ASCII codes
• "e" - move the pointer to the string two characters forward
• 3 - cast the string to an integer and add
• 2 - cast the string to an integer, fail because that cast doesn't generally work, yield the default integer (0) and add.
• "onetwo" - cast the integer to a string and append

Notably, the above errors can both be generated at compile or runtime, depending on the language.

Let's Make a Type System

Types Recap

What do type systems give us?

Insight: typing is essentially a system for formal reasoning about your code...

Formalities

Showing that an expression is well-typed is, essentially, a proof.

Thus, we can define typing rules as proof rules (see the type rules section for an example). Using the form of logic inference rules we learned in CS 81:

\[ \infer { Conclusion } { Premise(s) } \]

Note: \[ \infer {\text{CS131 is fun!}} {} \]

This means the conclusion is inherently true (since it requires no premises). -- MorganFrisby - 12 Mar 2019 (Also known as a tautology -- OwenGillespie - 9 May 2019)

Type Rules for a Simple Language

Imagine a programming language with abstract syntax somewhat similar to Assignment 1 (Lambda calculus with some extra functionality, but not all the functionality of Haskell). It has two primitive datatypes: int and bool; and composite types for tuples, lists and functions.

A Simple Functional Language

We'll work with this simple language:

\[ \begin{array}{rll} \t ::= &\tint\ |\ \tbool \\\ |&\tarrow{\t_1}{\t_2}\\\ |&\ttimes{\t_1}{\t_2}\\\ |&\tlist{\t}\\\ \var ::= &\mathcd{x}\ |\ \mathcd{y}\ |\ \mathcd{foo}\ | \cdots\\\ \n ::= &{\mathcd{0}}\ |\ {\mathcd{1}}\ |\ \cdots\\\ \val ::=&\econst{\n}\\\ |&\econst{\trueval}\\\ |&\econst{\falseval}\\\ |&\efn{\var}{\t}{\e} \\\ |&\enil{\t} \\\ \e ::= &\val\\\ |&\eplus{\e_1}{\e_2}\\\ |&\elt{\e_1}{\e_2}\\\ |&\var\\\ |&\eif{\e_1}{\e_2}{\e_3}\\\ |&\elet{\var}{\e_1}{\e_2}\\\ |&\epair{\e_1}{\e_2}\\\ |&\efst{\e}\\\ |&\esnd{\e}\\\ |&\eapply{\e_1}{\e_2}\\\ |&\econs{\e_1}{\e_2}\\\ |&\ecase{\e_1}{\e_2}{\var_1}{\var_2}{\e_3} \end{array} \]

• This syntax is similar to Haskell, but much more simplified. If there are things that look Haskell-y, then they probably behave in the same way.

Type Rules

\[ \infer {\fe{\econst{\n}}{\tint}} {} \]

\[ \infer {\fe{\econst{\trueval}}{\tbool}} {} \]

\[ \infer {\fe{\econst{\falseval}}{\tbool}} {} \]

\[ \infer {\fe{(\eplus{\e_1}{\e_2})}{\tint}} {\fe{\e_1}{\tint} \AND {\fe{\e_2}{\tint}}} \] (where the top premises are combined by an implicit AND)

\[ \infer { \fe{ (\elt{\e_1} {\e_2}) } {\tbool} } {\fe{\e_1}{\tint} \AND {\fe{\e_2}{\tint}}} \]

Providing Context: Type Environments

Just like value environments used in evaluation... but more mathy...

Note that we can not have rules like \[ \infer {\fe{\econst{\x}}{\tbool}} {} \] or \[ \infer {\fe{\econst{\x}}{\tint}} {} \] because that would imply that all values of x would have to satisfy those rules, or else our proof system would have false premises. Instead, we turn to environments to represent allowable deductions for variables' types.

Type environments:

• Map names to types — Γ(var)
• Can be partially/fully specified — Γ, var :: ty
• Provide context for predicates ... — Γ ⊢ exp :: ty (meaning, "In the context of Gamma, exp is of type ty)

i.e., We want to be able to say: \[ \wfe{\x :: \tint}{\x \;+\; \econst{1}}{\tint} \]

or \[ \G, \wfe{\x :: \tint}{\x \;+\; \econst{1}}{\tint} \]

In English, we could read this as, "A type environment Γ with x being of type int entails x+1 being of type int."

Revised Type Rules

We will rewrite the above type rules using Gamma, our mathy environment for types:

Basic typechecking:

\[ \infer {\wfe{\G}{\econst{\n}}{\tint}} {} \]

\[ \infer {\wfe{\G}{\econst{\trueval}}{\tbool}} {} \]

\[ \infer {\wfe{\G}{\econst{\falseval}}{\tbool}} {} \]

Addition:

\[ \infer {\wfe{\G}{(\eplus{\e_1}{\e_2})}{\tint}} {\wfe{\G}{\e_1}{\tint} \AND {\wfe{\G}{\e_2}{\tint}}} \]

Comparison:

\[ \infer {\wfe{\G}{(\elt{\e_1}{\e_2})}{\tbool}} {\wfe{\G}{\e_1}{\tint} \AND {\wfe{\G}{\e_2}{\tint}}} \]

Variable Lookup:

\[ \infer {\wfe{\G}{\var}{\G(var)}} {\var\in\mathop{\mathrm{dom}}(\G)} \] NOTE: $\mathop{\mathrm{dom}}(\G)$ means the domain of Γ.

Why is it necessary to include $\mathop{\mathrm{dom}}(\G)$?

(more in next class)

-- MelissaONeill - 29 Mar 2020