\PassOptionsToPackage{unicode=true}{hyperref} % options for packages loaded elsewhere
\PassOptionsToPackage{hyphens}{url}
%
\documentclass[english,]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\usepackage{fixltx2e} % provides \textsubscript
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
  \usepackage{textcomp} % provides euro and other symbols
\else % if luatex or xelatex
  \usepackage{unicode-math}
  \defaultfontfeatures{Ligatures=TeX,Scale=MatchLowercase}
\fi
% use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
% use microtype if available
\IfFileExists{microtype.sty}{%
\usepackage[]{microtype}
\UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\IfFileExists{parskip.sty}{%
\usepackage{parskip}
}{% else
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
}
\usepackage{hyperref}
\hypersetup{
            pdftitle={CSci 555: Functional Programming Type System Concepts},
            pdfauthor={H. Conrad Cunningham},
            pdfborder={0 0 0},
            breaklinks=true}
\urlstyle{same}  % don't use monospace font for urls
\usepackage{color}
\usepackage{fancyvrb}
\newcommand{\VerbBar}{|}
\newcommand{\VERB}{\Verb[commandchars=\\\{\}]}
\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\}}
% Add ',fontsize=\small' for more characters per line
\newenvironment{Shaded}{}{}
\newcommand{\AlertTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\AnnotationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\AttributeTok}[1]{\textcolor[rgb]{0.49,0.56,0.16}{#1}}
\newcommand{\BaseNTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\BuiltInTok}[1]{#1}
\newcommand{\CharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\CommentTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textit{#1}}}
\newcommand{\CommentVarTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\ConstantTok}[1]{\textcolor[rgb]{0.53,0.00,0.00}{#1}}
\newcommand{\ControlFlowTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\DataTypeTok}[1]{\textcolor[rgb]{0.56,0.13,0.00}{#1}}
\newcommand{\DecValTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\DocumentationTok}[1]{\textcolor[rgb]{0.73,0.13,0.13}{\textit{#1}}}
\newcommand{\ErrorTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\ExtensionTok}[1]{#1}
\newcommand{\FloatTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\FunctionTok}[1]{\textcolor[rgb]{0.02,0.16,0.49}{#1}}
\newcommand{\ImportTok}[1]{#1}
\newcommand{\InformationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\KeywordTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\NormalTok}[1]{#1}
\newcommand{\OperatorTok}[1]{\textcolor[rgb]{0.40,0.40,0.40}{#1}}
\newcommand{\OtherTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{#1}}
\newcommand{\PreprocessorTok}[1]{\textcolor[rgb]{0.74,0.48,0.00}{#1}}
\newcommand{\RegionMarkerTok}[1]{#1}
\newcommand{\SpecialCharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\SpecialStringTok}[1]{\textcolor[rgb]{0.73,0.40,0.53}{#1}}
\newcommand{\StringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\VariableTok}[1]{\textcolor[rgb]{0.10,0.09,0.49}{#1}}
\newcommand{\VerbatimStringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\WarningTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{0}
% Redefines (sub)paragraphs to behave more like sections
\ifx\paragraph\undefined\else
\let\oldparagraph\paragraph
\renewcommand{\paragraph}[1]{\oldparagraph{#1}\mbox{}}
\fi
\ifx\subparagraph\undefined\else
\let\oldsubparagraph\subparagraph
\renewcommand{\subparagraph}[1]{\oldsubparagraph{#1}\mbox{}}
\fi

% set default figure placement to htbp
\makeatletter
\def\fps@figure{htbp}
\makeatother

\usepackage{caption}
\DeclareCaptionLabelFormat{nolabel}{}
\captionsetup{labelformat=nolabel}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[shorthands=off,main=english]{babel}
\else
  % load polyglossia as late as possible as it *could* call bidi if RTL lang (e.g. Hebrew or Arabic)
  \usepackage{polyglossia}
  \setmainlanguage[]{english}
\fi

\title{CSci 555: Functional Programming\\
Type System Concepts}
\author{\textbf{H. Conrad Cunningham}}
\date{\textbf{3 February 2019}}

\begin{document}
\maketitle

{
\setcounter{tocdepth}{4}
\tableofcontents
}
Copyright (C) 2018, 2019, \href{http://www.cs.olemiss.edu/~hcc}{H.
Conrad Cunningham}\\
Professor of \href{https://www.cs.olemiss.edu}{Computer and Information
Science}\\
\href{http://www.olemiss.edu}{University of Mississippi}\\
211 Weir Hall\\
P.O. Box 1848\\
University, MS 38677\\
(662) 915-5358

\textbf{Browser Advisory:} The HTML version of this textbook requires a
browser that supports the display of MathML. A good choice as of
February 2019 is a recent version of Firefox from Mozilla.

\newpage

\hypertarget{type-system-concepts}{%
\section{Type System Concepts}\label{type-system-concepts}}

\hypertarget{introduction}{%
\subsection{Introduction}\label{introduction}}

The goal of these notes are to examine the general concepts of type
systems.

\hypertarget{types-and-subtypes}{%
\subsection{Types and Subtypes}\label{types-and-subtypes}}

The term \emph{type} tends to be used in many different ways in
programming languages. What is a type?

Conceptually, a \emph{type} is a set of values (i.e.~possible states or
objects) and a set of operations defined on the values in that set.

Similarly, a type \texttt{S} is (a behavioral) \emph{subtype} of type
\texttt{T} if the set of values of type \texttt{S} is a ``subset'' of
the values in set \texttt{T} and set of operations of type \texttt{S} is
a ``superset'' of the operations of type \texttt{T}. That is, we can
safely \emph{substitute} elements of subtype \texttt{S} for elements of
type \texttt{T} because \texttt{S}'s operations behave the ``same'' as
\texttt{T}'s operations.

This is known as the \emph{Liskov Substitution Principle} {[}Liskov
1987{]} {[}Wikipedia 2018a{]}.

Consider a type representing all furniture and a type representing all
chairs. In general, we consider the set of chairs to be a subset of the
set of furniture. A chair should have all the general characteristics of
furniture, but it may have additional characteristics specific to
chairs.

If we can perform an operation on furniture in general, we should be
able to perform the same operation on a chair under the same
circumstances and get the same result. Of course, there may be
additional operations we can perform on chairs that are not applicable
to furniture in general.

Thus the type of all chairs is a subtype of the type of all furniture
according to the Liskov Substitution Principle.

\hypertarget{constants-variables-and-expressions}{%
\subsection{Constants, Variables, and
Expressions}\label{constants-variables-and-expressions}}

Now consider the types of the basic program elements.

A \emph{constant} has whatever types it is defined to have in the
context in which it is used. For example, the constant symbol \texttt{1}
might represent an integer, a real number, a complex number, a single
bit, etc., depending upon the context.

A \emph{variable} has whatever types its value has in a particular
context and at a particular time during execution. The type may be
constrained by a declaration of the variable.

An \emph{expression} has whatever types its evaluation yields based on
the types of the variables, constants, and operations from which it is
constructed.

\hypertarget{static-and-dynamic}{%
\subsection{Static and Dynamic}\label{static-and-dynamic}}

In a \emph{statically typed language}, the types of a variable or
expression can be determined from the program source code and checked at
``compile time'' (i.e.~during the syntactic and semantic processing in
the front-end of a language processor). Such languages may require at
least some of the types of variables or expressions to be
\emph{declared} explicitly, while others may be \emph{inferred}
implicitly from the context.

Java, Scala, and Haskell are examples of statically typed languages.

In a \emph{dynamically typed language}, the specific types of a variable
or expression cannot be determined at ``compile time'' but can be
checked at runtime.

Lisp, Python, JavaScript, and Lua are examples of dynamically typed
languages.

Of course, most languages use a mixture of static and dynamic typing.
For example, Java objects defined within an inheritance hierarchy must
be bound dynamically to the appropriate operations at runtime. Also Java
objects declared of type \VERB|\BuiltInTok{Object}| (the root class of
all user-defined classes) often require explicit runtime checks or
coercions.

\hypertarget{nominal-and-structural}{%
\subsection{Nominal and Structural}\label{nominal-and-structural}}

In a language with \emph{nominal typing}, the type of value is based on
the type \emph{name} assigned when the value is created. Two values have
the same type if they have the same type name. A type \texttt{S} is a
subtype of type \texttt{T} only if \texttt{S} is explicitly declared to
be a subtype of \texttt{T}.

For example, Java is primarily a nominally typed language. It assigns
types to an object based on the name of the class from which the object
is instantiated and the superclasses extended and interfaces implemented
by that class.

However, Java does not guarantee that subtypes satisfy the Liskov
Substitution Principle. For example, a subclass might not implement an
operation in a manner that is compatible with the superclass. (The
behavior of subclass objects are thus different from the behavior of
superclass objects.) Ensuring that Java subclasses preserve the
Substitution Principle is considered good programming practice in most
circumstances.

In a language with \emph{structural typing}, the type of a value is
based on the \emph{structure} of the value. Two values have the same
type if they have the ``same'' structure; that is, they have the same
\emph{public} data attributes and operations and these are themselves of
compatible types.

In structurally typed languages, a type \texttt{S} is a subtype of type
\texttt{T} only if \texttt{S} has all the public data values and
operations of type \texttt{T} and the data values and operations are
themselves of compatible types. Subtype \texttt{S} may have additional
data values and operations not in \texttt{T}.

Haskell is an example of a primarily structurally typed language.

\hypertarget{polymorphic-operations}{%
\subsection{Polymorphic Operations}\label{polymorphic-operations}}

\emph{Polymorphism} refers to the property of having ``many shapes''. In
programming languages, we are primarily interested in how
\emph{polymorphic} function names (or operator symbols) are associated
with implementations of the functions (or operations).

In general, two primary kinds of polymorphic operations exist in
programming languages:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  \emph{Ad hoc polymorphism}, in which the same function name (or
  operator symbol) can denote different implementations depending upon
  how it is used in an expression. That is, the implementation invoked
  depends upon the types of function's arguments and return value.

  There are two subkinds of ad hoc polymorphism.

  \begin{enumerate}
  \def\labelenumii{\alph{enumii}.}
  \item
    \emph{Overloading} refers to ad hoc polymorphism in which the
    language's compiler or interpreter determines the appropriate
    implementation to invoke using information from the context. In
    statically typed languages, overloaded names and symbols can usually
    be bound to the intended implementation at \emph{compile time} based
    on the declared types of the entities. They exhibit \emph{early
    binding}.

    Consider the language Java. It overloads a few operator symbols,
    such as using the \texttt{+} symbol for both addition of numbers and
    concatenation of strings. Java also overloads calls of functions
    defined with the same name but different signatures (patterns of
    parameter types and return value). Java does not support
    user-defined operator overloading; C++ does.

    Haskell's \emph{type class} mechanism implements overloading
    polymorphism in Haskell. There are similar mechanisms in other
    languages such as Scala and Rust.
  \item
    \emph{Subtyping} (also known as \emph{subtype polymorphism} or
    \emph{inclusion polymorphism}) refers to ad hoc polymorphism in
    which the appropriate implementation is determined by searching a
    hierarchy of types. The function may be defined in a supertype and
    redefined (overridden) in subtypes. Beginning with the actual types
    of the data involved, the program searches up the type hierarchy to
    find the appropriate implementation to invoke. This usually occurs
    at runtime, so this exhibits \emph{late binding}.

    The object-oriented programming community often refers to
    inheritance-based subtype polymorphism as simply
    \emph{polymorphism}. This is the polymorphism associated with the
    class structure in Java.

    Haskell does not support subtyping. Its type classes do support
    \emph{class extension}, which enables one class to inherit the
    properties of another. However, Haskell's classes are not types.
  \end{enumerate}
\item
  \emph{Parametric polymorphism}, in which the same implementation can
  be used for many different types. In most cases, the function (or
  class) implementation is stated in terms of one or more type
  parameters. In statically typed languages, this binding can usually be
  done at compile time (i.e.~exhibiting early binding).

  The object-oriented programming (e.g.~Java) community often calls this
  type of polymorphism \emph{generics} or \emph{generic programming}.

  The functional programming (e.g.~Haskell) community often calls this
  simply \emph{polymorphism}.
\end{enumerate}

TODO: Bring ``row polymorphism'' into the above discussion?

\hypertarget{polymorphic-variables}{%
\subsection{Polymorphic Variables}\label{polymorphic-variables}}

A \emph{polymorphic variable} is a variable that can ``hold'' values of
different types during program execution.

For example, a variable in a dynamically typed language (e.g.~Python) is
polymorphic. It can potentially ``hold'' any value. The variable takes
on the type of whatever value it ``holds'' at a particular point during
execution.

Also, a variable in a nominally and statically typed, object-oriented
language (e.g.~Java) is polymorphic. It can ``hold'' a value its
declared type or of any of the subtypes of that type. The variable is
declared with a static type; its value has a dynamic type.

A variable that is a parameter of a (parametrically) polymorphic
function is polymorphic. It may be bound to different types on different
calls of the function.

\hypertarget{exercises}{%
\subsection{Exercises}\label{exercises}}

TODO

\hypertarget{acknowledgements}{%
\subsection{Acknowledgements}\label{acknowledgements}}

In Spring 2018, I wrote the general Type System Concepts section as a
part of a chapter that discusses the type system of Python 3
{[}Cunningham 2018a{]}.

In Summer 2018, I revised it to become Section 5.2 in the new Chapter 5
of the textbook \emph{Exploring Languages with Interpreters and
Functional Programming} (ELIFP) {[}Cunningham 2018b{]}. I also moved the
``Kinds of Polymorphism'' discussion from the 2017 List Programming
chapter of that book to the new subsection ``Polymorphic Operations''.
(This section draws on various Wikipedia articles {[}Wikipedia 2018b{]}
and other sources.)

In Fall 2018, I copied the general concepts from ELIFP and recombined it
with the Python-specific content from the first part of {[}Cunningham
2018a{]} to form a chapter for a posible future book based on Python 3.

This chapter sought to be compatible with the concepts, terminology, and
approach of the 2018 version of my textbook \emph{Exploring Languages
with Interpreters and Functional Programming} {[}Cunningham 2018b{]}, in
particular of Chapters 2, 3, and 5.

In Spring 2019, I extracted the general concepts discussion from the
Python 3 chapter for use in a Scala-based course

I maintain this chapter as text in Pandoc's dialect of Markdown using
embedded LaTeX markup for the mathematical formulas and then translate
the document to HTML, PDF, and other forms as needed.

\hypertarget{references}{%
\subsection{References}\label{references}}

\begin{description}
\tightlist
\item[{[}Cunningham 2018a{]}:]
H. Conrad Cunningham.
\href{https://john.cs.olemiss.edu/~hcc/csci658/notes/PythonMetaprogramming/Py3RefMeta02.html}{Basic
Features Supporting Metaprogramming}, Chapter 2, \emph{Python 3
Reflexive Metaprogramming}, 2018.
\item[{[}Cunningham 2018b{]}:]
H. Conrad Cunningham. \emph{Exploring Languages with Interpreters and
Functional Programming},
\url{https://www.cs.olemiss.edu/~hcc/csci450/ELIFP/ExploringLanguages.html},
draft 2018.
\item[{[}Liskov 1987{]}:]
Barbara Liskov. Keynote Address---Data Abstraction and Hierarchy, In the
Addendum to the \emph{Proceedings on Object-Oriented Programming
Systems, Languages, and Applications (OOPSLA '87)}, Leigh Power and Zvi
Weiss, Editors, ACM, 1987.
{[}\href{../../localcopy/Liskov_Data_Abstraction_and_Hierarchy_1987.pdf}{local}{]}
\item[{[}Wikipedia 2018a{]}:]
Wikipedia,
\href{https://en.wikipedia.org/wiki/Liskov_substitution_principle}{Liskov
Substitution Principle}, accessed 30 August 2018.
\item[{[}Wikipedia 2018b{]}:]
\emph{Wikipedia} articles on ``Polymorphism'', ``Ad Hoc Polymorphism'',
``Parametric Polymorphism'', ``Subtyping'', and ``Function
Overloading'', accessed 30 August 2018.
\end{description}

\hypertarget{terms-and-concepts}{%
\subsection{Terms and Concepts}\label{terms-and-concepts}}

Object, object characteristics (state, operations, identity,
encapsulation, independent lifecycle), immutable vs.~mutable, type,
subtype, Liskov Substitution Principle, types of constants, variables,
and expressions, static vs.~dynamic types, declared and inferred types,
nominal vs.~structural types, polymorphic operations (ad hoc,
overloading, subtyping, parametric/generic), early vs.~late binding,
compile time vs.~runtime, polymorphic variables.

\end{document}