►
From YouTube: Type-Driven Development in Idris — Edwin Brady
Description
Idris is a general purpose pure functional programming language with dependent types. In Idris, types are a first class language construct, meaning that they can be manipulated and computed like any other language construct. It encourages a type-driven style of development, in which programmers give types first and use interactive editing tools to derive programs. Introductory examples typically involve length-preserving operations on lists, or ordering invariants on sorting.
Realistically, though, programming is not so simple: programs interact with users, communicate over networks, manipulate state, deal with erroneous input, and so on. In this talk I will show how advanced type systems allow us to express such interactions precisely, and how they support verification of stateful systems as a result.
The talk will include several examples, leading to a verified implementation of a word game (Hangman). I will show how Type-driven Development allows programmers to specify the game rules in a direct and concise style, and how it leads to an implementation, guaranteed to correctly follow the rules by typechecking.
A
A
It's
a
very
enthusiastic
I,
see
favors
for
a
dependent
type
system,
called
it
white
space.
Indeed,
that
was
it
then
you're
ahead
of
the
curve
he's
also
famous
for
white
space
and
interest,
is
called
T
mmm-hmm
complete,
no
detrás
complete
very
good.
Why
is
the
call
takers
complete
well
we'll
come
to
that.
B
B
B
B
B
Programmers
I'm
really
here
because
I
want
you
to
steal
my
ideas.
So
if
you
can
pick
up
some
ideas
that
you
see
in
a
dress
that
you
think
you
can
apply
to
your
scale
of
programs
or
more
widely,
then
please
do
just
to
say
another
thing
about
about
that
talk
with
with
miles
what
what
actually
haven't
is?
Yes,
yes,
here,
so
what
we?
What
we
did
was
I
wrote
a
couple
of
idiots
programs
and,
and
they
were
basically
challenges
for
miles-
I
wrote
programs
using
the
full
dependent
type
system
in
Icarus
and
said
okay
miles.
B
B
So
so
we'll
see
what
happens
excellent
challenge
accepted
said
miles.
Look
the
video
didn't
get
that
so
internet
miles,
step,
challenge
accepted
right.
So
a
few
people
have
asked
over
the
last
couple
days
where
I'm
from
I'm
from
st.
Andrews
and
so
now
he's
in
Scotland,
and
one
thing
that
you
may
or
may
not
know
about
Scotland
is
that
it
is.
It
is,
in
some
sense
the
spiritual
home
of
functional
programming
in
that
Haskell
arose
from
Scotland
ml.
B
It
was
a
Scottish
programming,
language
and-
and
we
now
fly
the
flag
in
Scotland
to
reflect
this
important
bit
of
the
nation's
history.
So
it
seems
only
right
that
you
know
I
should
present
another
Scottish
programming,
a
Scottish,
functional
programming,
language,
okay,
so
I'm
gonna
talk
about
a
dress,
it's
a
pacman,
complete
functional
programming
language
and
by
pac-man,
complete
I,
basically
mean
that
there
is
enough
available
there
that
if
you
wanted
to,
you
could
implement
pac-man.
So
people
talk
about
you
know
if
a
new
language
appears
people
think
is
it
your
people
asked?
B
Is
it
your
incomplete?
They
might
worry
if
it's
not
quite
your
incomplete
but
I.
Think
that's
not
really
that
not
really
that
useful
thing
to
say
about
something
wide
space,
for
example,
is
steering
complete,
but
it's
not
pac-man
complete
again.
Maybe
someone
will
accept
that
as
a
challenge
to
prove
that,
but
I
think
it's
far
more
useful
to
say
something
as
pac-man
company
simply
because
if
you
have
the
ability
to
take
your
fancy
language
and
talk
to
system
libraries
and
do
system
interaction,
then
you
have
something
that
is
potentially
truly
useful.
B
I
also
have
you
know
right
at
the
beginning,
the
instructions
on
how
to
install
the
thing.
If
you
have
the
Haskell
platform
installed
over
the
room
like
this
is
likely
to
have
the
Haskell
platform
installed.
Maybe
they
shouted
a
bit
a
few
times,
but
there
are,
there
are
binaries
available.
You
can
go
and
download
and
all
of
the
examples
I'm
going
to
present
in
this
talk.
All
of
them
are
available
online
for
you
to
play
with
and
just
try
out
for
yourself.
B
B
You
know
when
you
when
you're
writing
your
your
fancy,
scala
programs
with
with
your
type
level,
extensions
you'll
at
least
be
thinking.
Okay.
How
might
this
work
if
I
was
able
to
express
it
with
first-class
types
and
and
maybe
get
a
better
understanding
of
what's
going
on
underneath
so
the
example
I
want
to
show
you
are
the
sort
of
things
that
the
sort
of
places,
what
I
think
verification
has
a
good
chance
of
being
useful
in
the
short
term.
So,
realistically
we're
not
going
to
be
able
to
say
in
the
near
future.
B
I've
written
the
program,
it
type
checks
ship
it
it's
okay,
but
we
are
going
to
be
able
to
sit.
There
are
gonna,
be
fragments
of
our
programs,
so,
where
we're
working
on
network
infrastructure-
or
you
know
the
core
components
of
our
programs-
that
we
really
have
to
be
confident,
I
will
running
avionics
software.
We
want
to
be
fairly
sure
that
it
it's
doing
the
right
thing,
so
those
core
components
I
think
in
the
near
future.
We
have
a
reasonable
chance
of
being
able
to
use
these
kinds
of
dependent
type
techniques
to
work
in
those
spaces.
B
I'm
gonna
give
you
some
idea
of
how
we
might
be
able
to
do
this
using
a
language
like
address
so
I
wanna,
say
a
little
bit
about
what
I
see
types
is
being
useful
for
so
I've
titled.
This
talk
type
development
in
Idris
for
two
reasons:
I've
come
to
the
second
reason
later
on.
The
first
reason
is
that
I've
seen
a
lot
of
types
over
the
last
day
or
so,
and
a
lot
of
people
have
said
types
are
for
giving
us
confidence
that
the
program
is
correct.
B
If
we,
if,
if
the
program
type
checks,
we
know
that
it's
going
to
work
to
a
certain
level
of
work,
and
that's
great-
that
is
absolutely
true
thing-
is
there's
so
much
more.
You
can
do
with
types
we
should
be
using
types,
not
so
much
as
a
way
of
having
the
machine
tell
us
when
we've
done
something
right.
We
should
also
be
using
types
as
a
means
of
guiding
us
towards
the
program.
That's
going
to
work.
So
it's
too
easy
to
think
of
you
write
your
long
program.
You
submit
it
to
the
type
checker.
B
You
know
you
send
it
to
your
teacher
for
grading
and
it
comes
back
and
says
you
know
three
type
errors
see
me
after
class.
What
we
want
to
be
doing
instead
is
thinking
of
the
type
checker
as
your
lab
assistant.
So
if
you
write
the
type
first
and
say
okay
lab
assistant,
this
is
what
we're
going
to
do.
Let's
work
on
it
together,
every
so
often
you
might
be
able
to
say:
okay,
I'm,
not
sure
how
this
program
works.
B
Can
you
give
me
a
clue,
rather
than
rather
than
you
know,
generate
some
code
and
test
because
it
looks
like
it
might
be
right
and
see
if
the
type
checker
accepts
it
so
we'll
see
some
examples
of
how
that
goes
as
we
get
on
to
the
examples
shortly
and
that's
the
sort
of
mantra
that
I've
started
using
we're
gonna
see
throughout
his
life.
Test-Driven
development
has
a
red
green
refactor.
We
have
type
defined
refine
I'm,
very
sad
that
I
couldn't
find
a
word
for
type
that
rhymes
with
defined
and
refined
by
the
way.
B
So
if
anybody
has
one,
let
me
know
so,
everything
we
do
is
going
to
be
either
right
or
inspector
type
define
a
function
and
we
can
define
functions
that
are
possibly
incomplete.
We
can
say:
okay,
we
have
most
of
our
function
and
I'm
going
to
leave
a
hole
for
the
bit
of
the
function.
I
haven't
written
yet
and
then
another
thing
we
can
do
is
refine,
so
I'm
gonna,
say
I'm.
Gonna
use
the
word
refine
a
lot,
we're
going
to
take
a
definition.
That's
possibly
incomplete
and
refine
it.
B
So
it
either
has
a
more
complete
definition
or
a
slightly
more
informative
type
and
basically
everything
we
do
comes
into
into
one
of
these
three
headings.
So
every
time
all
the
time
think
is
it
a
type.
Are
we
defining?
Are
we
refining
and
I
suppose
we
can
add
refactor
at
the
end,
once
we
have
a
working
pro,
we
can
safely
refactor,
knowing
that
if
it
continues
to
type-check
it
continues
to
be
okay.
B
So
just
before
I
get
on
to
the
demo,
don't
do
a
quick
rundown
of
some
of
the
features
Idris
has
because
it's
kind
of
a
kind
of
an
FAQ
people
always
ask
me.
Firstly,
first
class
dependent
types
so
I,
say
first
class
here,
meaning
that
the
syntax
and
and
semantics
at
the
type
level
and
the
value
level
are
the
same.
So
there's
no
there's
no
difference.
There's
no
sort
of
barrier
there's
no
barrier
between
the
two
languages.
It
really
is
completely
the
same
language.
B
Anything
you
can
write
in
an
expression
you
can
write
in
the
type
and
vice
versa,
long
as
it
type
checks.
So
when
you
introduce
functional
programming
to
people,
we
often
say
that
functions
are
first
class
because
it
means
we
can
pass
them
around.
Just
like
any
other
value,
we
can
compete
them
just
like
any
other
value.
B
Well,
in
the
first
class
type
system
same
goes
for
types
we
can
compute
them
build
them
just
like
any
other
value,
although
Haskell
inspired
syntax
I,
sometimes
regret
that,
because
it
means
people
think
it
should
work
like
Haskell
various
ways
in
which
it
doesn't
I
just
happened
to
like
Haskell
syntax,
there's
a
few
things
that
have
changed
a
little
bit
that
I
didn't
like
too
much
like
you
know:
single
:
4
types.
Instead
of
a
double
colon,
that
kind
of
thing:
it's
a
compiled
language.
B
There
are
two
code
generators
that
you
get
when
you
install
it
one
via
C,
just
running
native
code,
one
via
JavaScript
does
have
a
pluggable
back-end
system.
So
you
can
you
can
plug
in
if
you,
if
you,
if
you
have
it's,
exporting
an
interface
to
the
intermediate
language.
So
if
you
want
a
JVM
back-end,
then
by
all
means
go
ahead
and
write
it
I'm
happy
to
help
having
having
precise
types
means
that
we
get
optimizations
too.
So
we
can
read
your
aggressive,
inlining
aggressive
eurasia.
B
It
seems
to
me
that
if,
if
the
compiler
knows
more
about
the
program,
what
the
program
supposed
to
do,
it
should
be
able
to
do
more
work
at
compile
time
to
make
that
program
more
efficient.
So
things
like
removing
dynamic
tests
that
are
unnecessary
and
so
on
has
tied
classes.
I
bravely
put
like
trait
in
Scala,
hoping
that
was
correct.
B
It
has
tied
masses,
it's
essentially
a
way
of
defining
interfaces
to
a
type
interfaces
that
say
what
a
type
is
able
to
do,
unlike
Haskell
strict
evaluation.
But
if
you
want
lazy
evaluation,
you
can
have
laziness
as
a
type
we
won't
actually
get
to
that
in
this
talk,
I'm
just
saying
that,
because
somebody
always
asks
so
strict
evaluation
and
there's
various
bits
and
pieces
to
do
foreign
functions
system,
interaction,
okay,
so
mostly
what
I'm
going
to
do,
though,
is
it's
a
bit
of
live
hacking
because
it's
more
fun?
B
If,
if
I
actually
show
you
things
happening,
and
it's
also
more
fun,
if,
instead
of
me
just
doing
stuff
you
you
shout
out
questions
of
the
forum,
what
if
you
do
this
that
or
the
other
just
to
prove
that
I
haven't
made
this
up?
If
you
want
to
shout
out
suggestions
and
take
this
in
a
different
direction,
all
right?
Okay!
So
what's
the
answer
for
this
question?
B
Yes,
good,
let's
move
on
to
something
else,
then
I
guess
actually
I
could
just
to
just
to
show
you
things
compiling
and
running,
because
I
know
how
familiar
you
are
with
the
sort
of
theoretical
end
of
dependent
types,
but
sometimes
there
are
genuinely
people
who
think
it
type
checks.
I,
don't
need
to
bother
testing
it
because
I
already
know
it
works
and,
to
some
extent
that's
true,
but
we
do
actually
want
to
ship
these
and
sell
these
at
some
point.
B
So
I
can
sell
you,
my
hello
world
program,
right,
I
kind
of
compile
it
to
an
executable
and
there
we
go
so
it's
we
have
a
batch
compiler
that
works
in
the
usual
way.
We
also
have
a
read
eval
print
loop,
so
again
all
that
all
the
tools
that
you're
I
guess
you're
familiar
with
from
from
other
languages.
B
So
the
first
thing
I
want
to
show
you
is
the
simplest
first-class
type.
So
if
you
don't
get
what
I
mean
by
first-class
types,
this
will
hopefully
make
it
more
clear
to
you
what,
where
the
distinction
really
is
between
types
and
values,
there
isn't
one
so
I'm,
gonna
start
by
writing
a
function
that
takes
a
this,
is
in
the
a
from
text
editor
by
the
way,
so
I've
I've
started
using
the
Adam
text
editor
because
I've
been
using
vim
for
talks
and
people
say
to
me
afterwards.
B
That's
very
nice,
but
I
wish
I
didn't
have
to
use
vim,
so
I'm
using
Adam,
just
you
don't
have
to
use
it
in
I,
will
probably
get
my
fingers
in
a
tangle
at
some
point
so
Weiss
when
we
do
when
we
do
type
driven
development,
it's
always
types
first.
So
what
I've
got
in
this
file?
Is
it
a
couple
of
types
and
we're
going
to
use
the
types
to
lead
us
to
a
program
so
type?
B
First,
this
this
type
here
it's
going
to
be
the
type
we
calculate
it's
gonna,
be
if
the
boolean
is
true,
we're
gonna
have
it
return
for
boolean
means
singleton
if
it's
true
we're
going
to
return
a
singleton
natural
number
and
if
it's
false,
not
a
singleton,
we're
going
to
return
list
of
natural
numbers.
So
what
I
do
in
assam
is
is,
is
I
say,
okay,
I've
got
the
type,
give
me
a
skeleton
definition.
So
this
is
a
ctrl
alt,
a
for
add
definition,
and
it
gives
me
a
skeleton
definition.
B
So
this
thing
here
list
I
bar
HS.
This
is
a
whole,
so
this
is
syntactically
valid.
I
can.
I
can
load
this
into.
If
I
will
load
it
into
the
intro
0
to
unity,
so
I
can
load
this
into
the
repple
and
and
it
will
happily
load
it
and
it
will
say:
okay,
you've
got
a
couple
of
holes.
Is
that
color
legible?
It's
not
really.
This
I'll
turn
the
color
off
there
is.
There
is
a
you
in
color
by
the
way.
B
B
B
All
the
work
here
by
the
way
this
is
Adam
is
very
thin,
has
a
very
thin
wrapper,
and
this
means
that
you
can
easily
adapt
this
to
your
favorite
text
editor
and
there
are
vim
and
Emacs
modes
okay,
so
we
can
also
inspect
where
we
write
programs
by
inspecting
the
possible
values
for
for
input.
So
so
there
singleton
the
possible
values
for
singleton
here,
since
it's
a
bool,
in
fact,
we
can
have
a
look
at
what
they
are
they're.
The
possible
values
are
false
and
true.
B
So
if
I
hit
ctrl
alt
c4k
splits
over
singleton,
it
will
split
back
into
the
two
possibilities
and
if
you
remember
I
said
before,
if
it's
false,
not
a
singleton,
that's
going
to
be
a
list
of
NAT,
and
if
it's
true
it
is
a
singleton,
it's
a
NAT.
So
why
would
we
do
this?
Why
would
we
write
functions
to
calculate
types?
Well,
it's
if
we
want
to
use
it
in
types.
So
something
we
can
do
is
let
let
the
types
of
later
inputs
be
calculated
from
the
types
of
earlier
inputs.
B
So
we're
going
to
run
this
function
because
this
function
returns
a
type
we're
going
to
run
it
in
the
context
in
a
context
where
it's
a
type
is
needed.
So
some
list
here
this
is
going
to
sum
either
a
list
of
things
or
give
the
value
of
a
natural
number
depending
on
the
value
of
singleton
and
the
next
input.
So
if
I,
look
at
the
type
of
this
hole
will
see
that
the
inputs
we
have
our
singleton,
which
is
a
boolean
and
X,
which
is
a
list
type
calculated
from
the
value
of
that
singleton.
B
So
I
can't
really
make
any
progress
here
or
the
only
interesting
thing
I
can
do.
The
only
thing
I
have
available
is
to
inspect
singleton
I
can't
inspect
X.
Yet
because
I
don't
know
what
type
it
is
I
don't
know
what
type
it
is
until
I
run
this
function,
so
I'll
do
a
case
split
on
singleton
and
if
I
now
inspect
that
I'm
going
look
at
the
type
of
some
list,
RHS
one.
So
that's
one
of
the
holes
that's
been
created.
We
know
that
singleton
is
false.
X
has
typed
this
type
singleton.
B
Sorry,
if
I
look
at
the
type
of
this
now
you'll
see
that
it's
refined
the
type
of
X,
given
that
it
now
knows
that
in
this
context,
singleton
is
false.
X
must
be
a
list
of
NAT,
and
you
know
correspondingly.
If
I
do
a
case
split,
it
will
give
me
the
cases
for
lists,
and
in
this
other
case,
if
I
do
the
K
split,
it
will
give
me
the
cases
from
that.
So
what's
happening
here
is
from
one
from
the
type
of
the
value
of
one
input.
B
The
machine
has
worked
out
the
value
of
the
next
input.
So
I'm
not
going
to
complete
this
definition,
but
I'm
going
to
show
you
a
definition
where
this
this
sort
of
thing
happens
in,
for
example,
see
you've
all
if
you've
ever
done.
Any
C
programming
you've
used
exactly
this
trick
when
you
use
the
printf
so
I
have
also
in
this
file.
I'll
show
you
the
type
of
printf,
so
the
type
of
printf.
This
is
exactly
the
same
trick.
We've
just
seen.
B
So
it
takes
a
format
string
as
an
input
and
the
return
type
is
calculated
from
this
format.
String
so
ready
the
type
of
printf
descend,
s
it'll,
say:
okay,
that's
a
string
to
string
or
%
F
identity;
okay,
that's
it
straight
to
industry,
and
so
C
compilers
have
to
do
this
through
some
compiler
hacks
to
make
sure
you've
got
the
right,
formatted
string.
This
is
just
an
imperious.
So
this
is
the
kind
of
the
kind
of
thing
you
might
use.
B
First-Class
types
for
is:
if
you
have
some,
maybe
some
schema
description
and
that
schema
description
will
calculate
the
valid
types
of
your
database.
Queries,
for
example,
so
just
scaling
this
up.
Okay,
so
that's
hello
world
example
1
hello
world
example.
2
is
going
to
be
vectors
because
it's
always
vectors
groans.
The
reason
we
use
vectors
so
vectors
are
lists
parametrized
by
their
length.
B
The
reason
we
use
vectors
as
a
hello
world
example
is
because,
unlike
printf
they're
genuinely
useful,
so
so
I'm
always
writing
programs,
certainly
in
Haskell,
where
I
make
the
assumption
that
a
list
I
have
is
non-empty
and
that
assumption
is
completely
valid
for
the
program.
I've
just
written
and
then
12
months
later
violate
that
assumption
in
some
other
file
and
I
get
a
crash.
That
was,
that
was
unexpected.
So
this
is
the
kind
of
thing
that
I
would
love
to
have
available.
You
know
it
straightforwardly
when
I
write
my
Haskell
programs.
B
So
what
happens
with
a
vector?
Is
you?
Can
you
declare
types
basically
by
giving
a
type
constructor
that
says
how
to
build
that
type
and
some
data
constructors
to
say
how
to
build
the
values
in
that
type.
So
nil
here
is
a
vector
with
zero
things
and
cons
is
a
vector
which,
given
a
thing
and
K
things
came
or
things
will
have
successor
of
casings.
So
its
successor
of
pay
s
of
K,
you
can
read
that
as
1
plus
K,
basically
so
in
native
a
datatype
defined
with
constructors,
a
0
and
1
plus
than.
B
Sort
of
thing
you
can
do
once
you
have
that
is,
is
well
you
you
can
express
in
variants
on
the
functions
you
have
over
the
list.
So
if
I
have
a
function,
that
I
want
to
apply
a
function
to
two
corresponding
vectors.
So
this
is
the
zip
width
function
that
do
you
have
any
put.
You
presume
you
must
have
an
equivalent
in
Scala.
You've
got
everything.
B
It's
got
its
bit
a
called
zip
with
yes
good,
so
this
is
taking
to
corresponding
this,
and
there
is
a
question
of
what
do
you
do
if
the
lists
of
different
lengths,
so
there's
some
perfectly
reasonable
things
you
could
do
here,
but
it
quite
often
other
than
what
you
certainly
when
I
use
this
I
make
the
assumption
that
the
lists
really
are
the
same
length
and
if
they're
not
I
should
be
doing
you
know.
I
should
do
something
about
that
beforehand.
B
So
here
I've
expressed
in
the
type
that
the
two
vectors
are
coming
in
are
the
same
length
and
the
vectors
going
out
is
the
same
length
and
the
the
the
wonderful
thing
about
a
time
driven
development.
Is
that,
given
that
I've,
given
that
I've
put
a
precisely
enough
type
for
that
function,
the
machine
can
tell
me
how
this
function
is
going
to
be
or
give
me
some
hints
about
how
this
function
is
going
to
be
written.
So
what
I'll
do
first
is
I'll
make
the
skeleton
definition.
B
So
this
is
control
of
a
as
we
did
before.
I
could
do
a
case
split
on
the
on
the
possible
input,
so
I'll
do
a
case
split
on
X's
here
and
if
I
look
at
the
type
of
zip
with
RHS,
we'll
see
that
wise,
so
we've
we've
got
X's
was
an
empty
vector
and
wise
must
be
a
vector
with
zero
things
in
it,
because
X
was
so
it's
the
only
thing
Weis
can
be.
So
if
I
do
a
case
split,
it
will
only
give
me
the
one
possibility
it
won't.
B
It
won't
even
suggest
that
I
have
to
deal
with
the
non
empty
vector
because
it
won't
type
check
and
the
fun
thing
about
this
is
if
I
look
at
the
time
to
the
right
hand,
side
now,
you'll
see
I'm
looking
for
a
vector,
zero
things
kind
of
fun.
That
I
can
just
say
to
the
Machine:
okay,
just
search
for
a
possible
solution
and
well
it's
dead,
easy
in
this
case.
B
B
B
B
You
know
it's
just
if
the
sort
of
problem
I
set
to
my
data
structures
and
algorithms
class
I
give
them
that
two-dimensional
linked
list
and
make
them
transpose
it,
and
they
hate
me
for
the
rest
of
the
university
career
and
I.
Don't
really
blame
them,
especially
given
that
we
teach
in
Java
there
I
said
it.
That's
nothing.
I
shouldn't
say
on
the
top:
that's
videoed
for
the
Internet
is
gonna,
be
a
trouble
man,
I
read
it
okay,
so
transpose
we're.
B
Gonna
do
the
same
thing,
so
we've
got,
we've
got
an
N
by
M
vector
and
we
want
to
give
back
an
N
by
n
vector.
So
this
X
is
is
a
vector
of
stuff.
I
mean
the
only
reasonable
thing
I
can
do
at
this
point.
The
only
thing
I
have
is
X's,
so
I'll
do
a
case
split
on
it
and
in
the
first
case,
so
if
X's
is
an
empty
vector
of
so
if
X
yeah,
if
the
input
was
an
empty
vector
of
stuff,
I
have
to
transpose
to
a
vector
of
empty
vectors.
B
So
I
can
look
at
the
type
just
to
see
what
the
type
of
thing
so
I
should
do.
It
says
I
need
to
produce
a
vector
of
M
empty
vectors.
Now
I
can't
be
bothered
to
do
that
immediately.
I'm
gonna,
but
I'm
gonna,
I'm
gonna,
put
empties
I'm,
gonna,
say
you're
right,
I'm,
going
to
rename
this
whole
two
empties
and
hit
ctrl
of
L,
and
what
that
does.
B
Is
it
lifts
the
function
lifts
a
new
top
level
function
with
the
type
I
need
to
fill
in
that
gap
and
I'm
going
to
come
to
this
later
then
I'm
gonna
move
on
to
the
interesting
case.
So
in
the
interesting
case,
what
have
I
got
so
step?
Is
it's
always
you
know
type
define
refine
write.
The
type
do
some
definition.
Look
at
any
more
types,
refine
the
definition,
so
I've
I've
done
the
type
in
a
defined
step.
I've
done
a
bit
of
refinement
here.
B
So
let's
look
at
the
type
again,
so
don't
make
any
progress
until
you've
seen
the
types
that
you're
that
you
need
to
be
working
with.
So
let's
look
at
the
type
of
transpose
of
vector,
RHS
too
so
I
have
a
vector
of
n
things
that
are
X,
so
this
is
the
first.
This
is
the
first
row,
so
in
fact
you
can
rename
it
because
I
gave
a
talk.
Awhile
back
and
someone
afterwards
turn
with
me
and
said:
they're
very
nice
talk.
But
why
do
you
functional
program
is
always
cool
things.
B
X
there's
a
very
good
question,
but
here
it's
clearly
a
run.
It's
a
row
things!
So,
let's
call
it
row
and
we
have.
We
have
a
vector
of
K
by
vector
of
anything.
So
it's
going
to
be
much
more
useful.
Given
that
rogue
is
a
vector
of
n
things
and
I
need
to
produce
a
vector
event,
it
would
be
much
more
helpful
if
X's
with
also
a
vector
of
n
things.
Now
we
know
how
to
turn
a
K
by
n
thing
into
an
N
by
K
thing.
We
make
a
recursive
call.
B
B
So
the
type
now
is
so
there
we
are
I
have
a
vector
of
N
Things,
another
vector
of
N,
Things
and
I
need
to
make
a
vector
of
n
things,
but
I
tell
you
what
we
did
in
zip
with
actually
isn't
it
week.
We
took
two
vectors
of
N
Things.
We
made
a
vector
of
n
things
and
I.
Don't
really
want
to
worry
about
filling
in
the
details
here,
so
I'm
just
going
to
lift
out
to
a
top
level
function.
B
So
I'm
gonna
write
a
helper
function
and
it's
given
me
the
type
which
is
which
is
nice
obvious.
So
so
it's
it's
it's
it's
filled
in
the
call
to
this
function,
I'm
about
to
write
and
now
I'd.
Given
me
a
type
and
I
could
do
the
usual
thing,
as
skeleton
definition
case
split
before
I
happen
to
know
that
I'm
not
gonna
need
X's,
so
I'm
gonna
delete
it
and.
B
B
And
that'll
help
there
and
similarly
for
empties,
so
you'll
notice
here
that
there's
a
there's
an
M
in
that
there's
a
type
variable
M
and
that's
awkward,
because
I
want
to
use
M
&
M's
in
the
type,
but
hang
on
types
are
first
class.
So
what
can
I
just
bring
it
into
scope,
since
its
types
are
first
class
I
can
I
can
just
bring
this
value
from
the
type
into
the
program
and
again
case
place
on
there,
and
this
is
just
going
to
recursively
build
an
appropriately
length
list
of
empty
vectors.
B
So
you
may
not
have
followed
exactly
what
was
going
on
in
the
program
there,
mostly
cuz.
The
machine
was
just
doing
the
thinking
for
us.
But
if
you
look
at
the
tights
here,
you
can
see
exactly
what's
going
on
from
from
the
top
here.
You
can
see
that
if
we
can
only
be
making
a
transpose
vector
here,
I
mean
there's.
We
we
could.
If
we
tried
quite
hard,
we
could
make
a
transpose
vector
containing
the
wrong
things
except
we
couldn't,
because
we
haven't
said
anything
about
LM.
Lm
is
just
a
type.
B
We
know
nothing
about
it,
except
that
it's
a
thick,
so
I
guess
we
could
be
reversing
things
or
making
them.
You
know
making
a
mess
of
the
structure
at
the
same
time,
but
really
the
only
natural
thing
we're
going
to
be
doing
here
is
transposing
again.
If
you
look
at
the
type
2
you'll
see
that
we
have
a
row
which
is
a
vector
of
n
things,
we
have
a
transpose
thing,
which
is
a
vector
of
n
things,
and
you
can
sort
of
if
you
squint
a
bit
at
the
type
you
can
see.
B
Well
got
an
n
look,
I've
got
a
thing
and
I've
got
K
things.
I
need
to
make
successor
of
casing.
So
essentially,
there's
gluing
the
road
on
to
the
front
of
the
vector.
Okay,
so
I
should
try.
I
mean
I
should
test
that
shouldn't
I,
because
I
mean
a
type
checked.
So
we
know
it's
going
to
work,
but
I've
created
a
main
program
that
takes
some
dimensions
of
a
vector,
invent
a
vector
and
then
transposes
it
for
us,
and
so.
B
B
So
if
you
ever
need
it,
this
is
I
actually
wrote
that
PHP
backend
for
a
bet,
but
but
you
know
almost
genuinely,
if
you
happen
to
be
writing
a
wordpress
plugin
as
I'm
sure
you
do
every
day,
and
you
want
to
have
some
kind
of
confidence
that
the
function
there
is
some
functional
correctness
to
your
WordPress
plugin.
Would
you
rather
write
it
in
PHP
or
in
a
functional
language?
I,
don't
know
well,
I
do
know,
I'd
rather
write
it
in
a
functional
language,
okay,
so
so
much
for
the
introductory
stuff.
How
are
you
for
time?
B
Ten
minutes.
Okay,
so
that's
a
couple
of
hello
world
examples.
What
I
want
to
show
you
to
finish
off
is
is
something
a
little
bit
more
think.
Realistic
of
the
sort
of
things
you
might
want
to
do
is
writing
down
state
machines
or
state
transition
systems
and
making
sure
that
you're
properly
following
the
appropriate
state
transition.
So
this
is
the
simplest
one.
I
could
think
of
that
demonstrates
the
point:
it's
the
door
open
and
close
state
machine,
so
a
door
can
either
be
in
the
open,
State
or
the
closed
State.
B
So
we'll
start
in
the
closed
State.
If
the
doors
closed
were
allowed
to
knock
on
it,
but
that
doesn't
change
the
state
and
if
the
doors
closed,
we're
allowed
to
open
it
and
that
changes
the
door
state,
it
opened
this
particular
door
you're
not
allowed
to
knock
on
it.
If
it's
open,
this
is
a
sliding
door,
so
the
door
vanishes
and
if
the
doors
open
you're
allowed
to
close
it.
B
So
this
is
this
might
seem
a
slightly
familiar
kind
of
API
I
mean
like
file
handling,
takes
this
this
this
kind
of
so
you
open
the
file.
There's
certain
things
that
you
can
do
to
file
when
it's
open,
there's
certain
things
you
can
do
to
follow
into
closed
and
they're,
not
necessarily
the
same,
and
it
would
be
nice
if,
in
your
API,
you
could
properly
express
this
kind
of
property
of
when
you're
allowed
to
do
certain
actions
and
what
those
actions
do
to
the
state.
B
If
you
can
characterize
the
state
of
your
system
and
in
some
abstract
way,
then
you
have
some
hope
of
reasoning
that
it's
that
it's
doing
the
right
thing.
So
I'm
not
going
to
go
through
the
details
of
how
this
works
exactly
in
a
dress.
I'm
just
going
to
show
you
the
types
and
hopefully
the
types
will
be
clear
enough.
That
you'll
believe
that
they
really
are
expressing
this
door
system
and
for
this
I'm
going
to
switch
back
to
them.
Just
to
show
that
you
can
have
multiple.
A
B
Also,
because
we're
going
to
see
error
messages
and
I
haven't
figured
out
how
to
get
the
error
message,
font
they
shouldn't
ask
them
yet.
But
that's
one
nice
thing
about
this
type,
driven
approach
by
the
way,
you
generally
don't
get
a
lot
of
error
messages,
because
the
Machine
is
only
giving
you
correct
programs
and
when
you
do
get
error
messages,
you
know
exactly
where
the
error
is
because
it's
in
the
tiny
bit
that
you
just
wrote
so
I
find
it
very
useful.
Even
when.
B
Okay,
so
this
is
a
representation
of
the
door
state
machine
using
so
it's
a
library
called
effect.
It's
distributed
with
Idris
and
F
here,
I'm
going
to
describe
f
as
a
kind
of
device
specific
language
for
building
your
own
monad
with
as
F
is
actually
I'm
on
earth
it
and
it's
it's.
It's
allow
it's
a
library
that
allows
you
to
compose
different
kinds:
different
bits
of
stateful
systems,
different
bits
of
effects
in
your
system
without
having
to
worry
about
the
the
plumbing
of
mono
transformers.
B
It
also
allows
you
to
change
the
that'ss
effects
that
you
have
available
as
the
system
of
the
system
progresses.
So
here
we've
said,
we've
said
in
the
type
of
open
door
that
it's
an
effectual
program.
It
returns
unit.
It
starts
with
a
door
in
the
closed
State
and
it
ends
with
a
door
in
the
open,
State
and
closed
door
is
the
other
way
around
and
then
Nakia
says
you
can
only
run
it
to
the
doors
in
the
closed
State
and
it
doesn't
change.
B
B
So
yeah,
if
I
try
to
open
it
twice.
This
is
a
slightly
more
readable
error
message.
We
we
have
a
weight,
something
with
the
error.
Messages
are
sometimes
a
bit
more
helpful
depending
on.
If
the
system
recognizes
the
structure
of
what's
going
on
so
here
it
says:
well,
you
you
did
something
that
required
the
door
to
be
closed
and
actually
the
door
was
open.
So
you
can
only
open
the
door
when
it's
closed
so
now
it
type
checks
again
because
I'm
following
the
protocol
properly.
So
what
sorts
of
things
this
is.
B
This
is
great
that
we
can
follow
the
state
machine,
but
the
problem
here
is:
we
have
specified
what
those
state
transitions
were
and
we
don't
always
have
control
over
the
world.
For
example,
the
door
might
Jam
they
might.
There
might
be
a
problem
with
the
door
it
might
eat,
you
know
oiling
or
something,
so
they
don't
like
Jam,
so
I,
don't
necessarily
know
when
I
open
the
door
if
I'm
in
an
open
door
state.
B
B
B
Do
so
now
my
open
door
site
says:
okay,
I've
started
in
the
closed
door
state
and
instead
of
instead
of
moving
on
to
the
open,
State
I'm
going
to
return,
the
jamb
status
of
the
door
ran
into
function
from
this
Jambres
of
type
of
jam
and
I
will
inspect
that
in
the
type
and
if
it
comes
back
with
jammed,
then
the
door
is
closed.
If
it
comes
back
with
okay,
then
the
door
is
open
so
down
here,
I
have
a
valid.
B
If
I'd,
if
I
try
the
thing
like
before
it's
gonna
say
no
sorry,
you
can't
do
that.
Looks
like
you've
slightly
worse
error
message
than
I
was
expecting,
but
the
the
point
the
things
to
look
at
is
we
have
a
door,
that's
open
and
it's
well.
We
need
to
have
a
door,
that's
open
and
we
have
a
door
that
isn't
when
we
close
it.
So,
instead,
what
we'll
do
is
get
we'll.
Take
the
the
return
value
of
opening
the
door.
B
I'll
sticker
I'll
stick
a
hole
in
here
for
the
rest
of
the
program
and
if
we
look
at
the
type
of
that
hole,
so
vim
has
all
the
interactive
editing.
Gadgets
too.
So
I
do
backslash
T
to
get
the
type
so
I
have
this
okay
of
type,
jamb
and
you'll
see
that
ok
appears
in
the
type.
So
this
is
a
hint
there
to
make
some
progress
here.
If
we
inspect
the
result
of
ok
with
any
luck,
this
type
is
going
to
refine
to
something
useful
that
we
can
work
with.
B
B
Yeah
yeah
Idris
is
doing
all
of
the
work
here,
which
is
good
news
for
editor
plugin
writers,
because
you
don't
really
want
your
when
you're
writing
an
IDE,
you
don't
really
want
to
have
to
be
re-implemented
the
entire
type
system.
Again,
especially
if
the
type
system
is
you
know
an
evaluator
too,
so
yeah
that
what
happened
here
is
that
in
in
this
branch
we
know
because
the
case
analysis
went
through
the
jammed
case.
B
We
know
that
we
have
to
calculate
the
the
state
where
the
door
is
jammed,
so
so
the
doors
closed
and
we
need
to
be
in
a
door
closed
state
by
the
way,
you'll
notice
that
I
thought
I
put
stood
I/o
here
as
well.
So
when
we
have
effect
'fl
programs,
we
can
list
the
effects
that
are
available,
so
it
means
I
can
do
something
like
you.
B
So,
in
the
okay
case,
if
we
look
at
the
type
here,
we'll
see
that
we're
in
the
door
open
state,
we
need
to
get
to
the
door
closed
state.
So
there's
no
way
this.
This
program
is
going
to
type-check
unless
we
actually
close
the
door
behind
us.
So
we
were
not
born
in
a
field,
so
we'll
close
the
door
behind
us
and
that
type
checked.
So
now
this
this
is
a
valid
use,
a
correct
use
of
the
of
the
door
protocol
under
the
possible
situation
of
the
door
not
closing
properly.
B
Just
one
more
thing
before
my
final
quick
bit
of
code,
quick
example
that
I
want
to
show
you
is
that
this,
this
kind
of
this
kind
of
thing
where
you're
you're
testing
for
errors
and
dealing
with
the
error
and
error
case
and
dealing
with
a
success
case.
You
could
imagine
some
very
deeply
nested
code
if
this
gets
longer-
and
you
know
that
you
might,
you
might
think,
how
can
you
throw
an
exception
and
have
a
handler
so
what
I
did
instead
is
I
I
decided
to
borrow
a
feature
from
Perl
I.
B
B
So
you
know
the
open
file
or
die
syntax
in
Perl,
any
Perl,
programmers
yeah.
You
know
that
syntax.
So
this
is.
This
is
kind
of
the
same
idea
that
you
have.
You
have
a
main
path
that
you
work
through
and
then
this
alternative
is
it
this.
This
is
only
called
it
in
the
event
that
open
door
doesn't
match.
Okay,
so
I
can
quite
happily
have
a
load
of
opening
and
closing
the
door
and.
B
So
the
idea
is
you're
guessing
letters
and
you're
getting
letters
in
a
word,
and
if
you
guess
correctly,
you
want
to
get
down
to
no
letter
still
to
guess
and
you
don't
want
to
get
down
to
no
guesses
available.
So
I
have
captured
the
possible
state
of
the
hangman
game
by
saying:
okay,
a
game
is
either
running
with
some
guesses
and
some
letters
or
it's
not
running
so
this
is
kind
of
like
our
door
opened
or
closed.
We've
got
two
different
states.
B
It's
just
that
one
of
the
states
has
has
a
bit
more
information
in
it.
So
that's
not
what
to
worry
too
much
about
the
exact
details
of
how
that's
represented.
But
the
important
point
of
this.
The
important
function
in
this
system
is,
if
we
get
a
letter,
that
letter
is
either
going
to
be
in
the
word
or
not
in
the
word,
and
that's
going
to
change
the
state
of
the
game
depending
on
whether
we
were
right
or
not
so
guess,
isn't
guessing
a
character
is
an
effect
FFEL
program
that
returns
true
or
false.
B
It
can
only
work
if
we
have
some
guesses
available.
It
can
only
work
if
we
have
things
still
to
guess
and
it
will
either
come
back
with
guests
still
available
and
a
letter
gone
or
a
guest,
gone
and
and
the
same
number
of
the
same
number
of
things
to
guess,
and
eventually
we
get
down
to
the
main
program
we
get
down
to
the
main
program.
We
see
that
a
hangman
game
is
something
which
starts
in
the
running
state,
with
some
guesses
available
and
maybe
some
words
and
it
ends
in
the
not
running
state
so
soon.
B
Somehow
this
program
is
going
to
have
to
get
to
a
game:
that's
either
won
or
lost
or
or
abandoned.
There's
no
other
way.
Out
of
this
we
have
to.
We
have
to
do
one
of
the
other
one
of
the
other.
By
the
way,
when
I
first
wrote,
this
I
gave
it
a
slightly
different
type.
I
gave
it
this
type,
and
so
this
this
is.
This
is
a
slightly
different
precondition.
B
That
says
the
words
that
we
give
it
has
to
have
at
least
one
letter
in
it,
and
there
was
nowhere
in
the
program
that
I
bothered
checking
that
the
strings
I
was
reading
had
one
letter
in
it,
and
so
the
Machine
said
sorry,
you
can't
have
rest
I
thought
that
was
actually
quite
lovely,
because
that's
the
kind
of
silly
mistake
I
make
all
the
time,
and
it's
the
sort
of
thing
that
you
think
well
types
can't
help
you
with
that.
Well,
I
think
they
can.
B
Another
mistake
I
made
is
to
given
that
the
two
things
number
of
letters
and
a
number
of
guesses
are
numbers.
So
here
we've
got
a
guest.
If
it's
true,
then
it
prints
the
message
false
and
prints
a
message.
This
really
happened
as
well:
I
got
the
wrong.
I
got
the
wrong
variable
and
because
they've
changed
the
wrong
bit
of
state,
it
told
me:
well
it
told
me
it
went
wrong,
but
if
you,
if
you
period
this
for
a
minute
or
so
you
can
see
exactly
what
went
wrong
and
actually
it
should
have.
B
I
want
a
list
of
words
just
to
show
that
there's
some
type
inference
available,
so
that
I
can't
be
bothered
to
give
the
list
of
this
word
I'm
just
waiting
patiently
for
someone
to
complain
at
me
there
this
that
so
there's
a
length
of
the
string
and
the
Machine
of
the
cell
tower
what
you
say
to
the
Machine.
You
work
out
the
length
of
this
list,
so
I
spotted
the
problem
with
this
list
of
words.
Yes,
scarlet,
isn't
it.
A
B
B
You'll
get
an
impression
for
the
speed
of
the
address
system
when
I
do
this,
not
necessarily
in
a
good
way.
So
this
is.
This
is
a
program
that
uses
the
effects
library
to
to
manage
the
state
of
a
space
invaders
game
so
that
where
the
aliens
are
where
the
scrotie
star
field
is
where
the
bombs
are
all
of
that,
the
bottleneck
here
by
the
way
is
GCC.
B
B
So
why
do
we
care
safety?
Safety
is
something
that
people
always
talk
about
with
types
we
care
about
safety,
but
there's
so
much
more.
We
can
write
expressive
api's.
We
can
write
generic
programs,
we
can
use
the
types
to
help
us
get
to
the
right
program.
That's
what
types
are
really
for
and
if
you're
interested
in
learning
more,
you
can
learn
more,
even
have
a
special
secret
code.
If
you
want
to
know
the
special
secret
code,
which
is
39
Brady
by
the
way,
then
you
can
get
a
discount
on
this.