Skip to content
Toggle navigation
P
Projects
G
Groups
S
Snippets
Help
Mark Cohen
/
thesis
This project
Loading...
Sign in
Toggle navigation
Go to a project
Project
Repository
Merge Requests
0
Pipelines
Members
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Commit
146aa5b2
authored
Jun 05, 2019
by
Mark Cohen
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
paper: progress
parent
f1cec376
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
107 additions
and
14 deletions
paper/main.bib
paper/main.tex
paper/main.bib
0 → 100644
View file @
146aa5b2
@article{associated-types,
author = "Manuel M. T. Chakravarty and Gabriele Keller and Simon Peyton Jones",
title = "Associated Type Synonyms",
journal = "ICFP",
year = "2005"
}
@article{typeclasses,
author = "Philip Wadler and Stephen Blott",
title = "How to make ad-hoc polymorphism less ad hoc",
journal = "PoPL",
year = "1989"
}
@article{traits,
author = "Natanael Sch{\"a}rli and Oscar Nierstrasz and St{\'e}phane Ducasse and Roel Wuyts and Andrew Black",
title = "Traits: The Formal Model",
year = "2003"
}
paper/main.tex
View file @
146aa5b2
\documentclass
[1
2
pt]
{
article
}
\documentclass
[1
1
pt]
{
article
}
\usepackage
{
amssymb, amsmath, amsthm, amsrefs
}
\usepackage
{
parskip, setspace, fullpage
}
\usepackage
[margin = 0.
9
in]
{
geometry
}
\usepackage
[margin = 0.
75
in]
{
geometry
}
\onehalfspacing
\setlength\parindent
{
0pt
}
...
...
@@ -13,11 +13,10 @@
%% better code font
% https://tex.stackexchange.com/q/88001/5764
\usepackage
{
listings, inconsolata, letltxmacro
}
\lstset
{
basicstyle=
\ttfamily
\small
, breaklines=true
}
\lstset
{
basicstyle=
\ttfamily
, breaklines=true
}
\LetLtxMacro\oldttfamily\ttfamily
\DeclareRobustCommand
{
\ttfamily
}{
\oldttfamily\csname
ttsize
\endcsname
}
\newcommand
{
\setttsize
}
[1]
{
\def\ttsize
{
#1
}}
%
\setttsize
{
\small
}
% ONE MOTHERFUCKING SPACE AFTER EACH MOTHERFUCKING SENTENCE
\frenchspacing
...
...
@@ -41,6 +40,9 @@
\usepackage
{
multicol
}
\setlength\columnsep
{
33pt
}
\usepackage
{
hyperref
}
\title
{
Iterative Programming in ML with Type Classes and Associated Types
}
\author
{
Mark Cohen
\\
...
...
@@ -60,10 +62,6 @@ type classes and associated types. This paper presents the motivation, design, i
formalism behind this language. Advised by Adam Shaw.
\end{abstract}
% gobble page number for title
\thispagestyle
{
empty
}
\clearpage
\begin{multicols}
{
2
}
\section
{
Introduction
}
...
...
@@ -117,23 +115,99 @@ res.collect::<HashMap<K, V>>()
\section
{
Design
}
To enable iteration, we propose a structure built around complementary pairs of type classes and
two
keyword constructs. First, to mark a type as iterable, the programmer creates an instance of the
\tt
{
Iterable
}
typeclass, defined as follows:
To enable iteration, we propose a structure built around complementary pairs of type classes and
three keyword constructs.
\end{multicols}
\begin{center}
\begin{lstlisting}
[mathescape=true]
\begin{center}
\begin{
tabular}
{
|c|
}
\hline
\begin{
lstlisting}
[mathescape=true]
class Iterable
$
\alpha
$
where
type item
val next:
$
\alpha
$
$
\arrow
$
item
$
\arrow
$
(item *
$
\alpha
$
) option
val next:
$
\alpha
$
$
\arrow
$
(item *
$
\alpha
$
) option
class Collectible
$
\alpha
$
where
type item
val default:
$
\alpha
$
val insert:
$
\alpha
$
$
\arrow
$
item
$
\arrow
$
$
\alpha
$
\end{lstlisting}
\end{center}
for <var> in <collection>
$
\arrow
$
<ty>
<expr>
collect <expr>
pass
\end{lstlisting}
\\\hline
\end{tabular}
\end{center}
\begin{multicols*}
{
2
}
\subsection
{
The
\tt
{
Iterable
}
typeclass
}
The
\tt
{
Iterable
}
typeclass, unsurprisingly, marks a type as iterable. The class contains an
associated type called
\tt
{
item
}
, which corresponds to the element type of the collection. For an
$
\alpha
$
\tt
{
list
}
,
\tt
{
item
}
is
$
\alpha
$
. For a
\tt
{
string
}
,
\tt
{
item
}
is
\tt
{
char
}
.
The
\tt
{
next
}
method takes a collection, and tries to produce a pair of the collection's next
element with the rest of the collection. If the collection is empty, it returns
\tt
{
None
}
. This
method encodes both loop variable bindings and loop bounds: at each iteration, the loop variable is
bound to the first half of the pair returned by
\tt
{
next
}
. When
\tt
{
next
}
returns
\tt
{
None
}
, we
conclude execution.
\subsection
{
The
\tt
{
Collectible
}
typeclass
}
The
\tt
{
Collectible
}
typeclass is something a little different: it marks a type as able to be built
up piece-by-piece. Like
\tt
{
Iterable
}
, the class contains an associated type
\tt
{
item
}
, which
functions exactly the same as in
\tt
{
Iterable
}
.
\tt
{
default
}
is something unusual: a non-function class member. Its sole purpose is to hold a value
that represents an "empty" collection: for an
$
\alpha
$
\tt
{
list
}
,
\tt
{
default
}
is
\tt
{
[]
}
. For a
\tt
{
string
}
,
\tt
{
default
}
is
\verb
|
""
|
. The purpose of
\tt
{
default
}
is to allow the programmer to
build up a result over individual iterations without having to carry an accumulator around in a
larger scope.
The
\tt
{
insert
}
method takes a collection and an item and returns a new collection containing both
the elements of the collection argument and the item argument.
\subsection
{
The
\tt
{
for
}
keyword construct
}
The
\tt
{
for
}
keyword takes an identifier
\tt
{
<var>
}
, which represents the loop variable.
\tt
{
<var>
}
will be bound to each element of
\tt
{
<collection>
}
in succession before each evaluation of
\tt
{
<expr>
}
. After performing inference the body of
\tt
{
<expr>
}
,
\tt
{
<var>
}
must have a type that
unifies with
\tt
{
<collection>
}
's
\tt
{
item
}
type.
The notation
$
\arrow
\tt
{
<ty>
}$
signifies that the programmer wishes to
\emph
{
build
}
a collection of
type
\tt
{
<ty>
}
: all loops in this discipline must explicitly build a collection.
This may seem restrictive, however given that the programmer can implement the
\tt
{
Collectible
}
typeclass for things that are not traditionally considered "collections", it does not impose undue
restriction.
There are important type restrictions on the various forms in
\tt
{
for
}
:
\tt
{
<collection>
}
must be an
\tt
{
Iterable
}
, and
\tt
{
<ty>
}
must be a
\tt
{
Collectible
}
. For the moment, we will not make any claims
about the type of
\tt
{
<expr>
}
. In the end, we will require a special type of
\tt
{
<expr>
}
, but the
intuitive type restrictions on items being collected will actually be imposed by the
\tt
{
collect
}
keyword.
\subsection
{
The
\tt
{
collect
}
and
\tt
{
pass
}
keyword constructs
}
The
\tt
{
collect
}
keyword takes only an expression
\tt
{
<expr>
}
, which implicitly is assumed to
contain references to the loop variable
\tt
{
<var>
}
; though of course there are situations where it
may not. Here is where we impose the restriction that
\tt
{
<expr>
}
must be of the same type as
\tt
{
<ty>
}
's
\tt
{
item
}
type: that is,
\tt
{
<expr>
}
must be something that can be
\tt
{
insert
}
ed into
an internal accumulator of type
\tt
{
<ty>
}
.
The
\tt
{
pass
}
keyword's sole purpose is to make
\tt
{
filter
}
expressions well-founded. Consider the
following program to filter out all zero elements in a list, which would not be feasible to write
without
\tt
{
pass
}
:
\begin{lstlisting}
[mathescape=true]
for x in [1, 2, 0, 3]
$
\arrow
$
int list
if zero? x
then pass
else collect x
\end{lstlisting}
\tt
{
pass
}
imposes no type restrictions and is defined to unify with any
\tt
{
collect
}
expression.
\section
{
Translation
}
% uncomment the below line to show all citations, even those not explicitly cited
\nocite
{
*
}
\bibliographystyle
{
unsrt
}
\bibliography
{
main
}
\end{multicols*}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment