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.


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]))

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?

Tests are not sufficient

The language does not understand tests

The language can understand types


Statically typed!

Type inference!

Typed holes!


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!


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 :’(