Moving towards dialogue

Collaborating with your computer using typed holes!

Vaibhav Sagar (@vbhvsgr)

What’s a typed hole?

Typed holes

A placeholder for an expression with a known type and an unknown value.

Why?

They allow the programming language to help us write programs!

Why do holes need to be typed?

Let’s write a program in Python

Is this program correct?

>>> def map(f, ls): return []

What about this one?

>>> def map(f, ls): [f(e) for e in ls]
...
>>> plusOne = lambda i: i + 1
>>> print(map(plusOne, [1, 2, 3]))
None

This one?

>>> def map(f, ls): return (f(e) for e in ls)
...
>>> print(map(plusOne, [1, 2, 3]))
<generator object map.<locals>.<genexpr> at 0x7ffb92103ca8>

How do I write programs that work?

We need tests!

>>> def map(f, ls):
...     print("Where are your tests now?")
...     return [2, 3, 4]
...
>>> map(plusOne, [1, 2, 3]) == [2, 3, 4]
Where are your tests now?
True

Tests are not sufficient

The language does not understand tests

The language can understand types

Haskell

Statically typed!

Type inference!

Typed holes!

Idris

More sophisticated type system!

Weaker type inference :(

Better editor integration!

Fancier typed holes!

We did it!

Typed holes exist!!!

Types are friends, not food!

Programming can be fun and interesting!

Resources

Thank You

Untyped Holes: Program Sketching!

1. Write a program with gaps (a ‘sketch’)

2. Write some test cases

3. Give a SAT/SMT solver your sketch and test cases

4. ???

5. Profit!

Still a research topic for now :’(

Resources