search

robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
83 stars 2 forks source link

Type-directed program synthesis #35

Open robrix opened 5 years ago

robrix commented 5 years ago

We should use the elaborator to provide terms to fill typed holes.

Even better, it should take resources into account so that it e.g. elides term-level use of 0-resourced parameters.

robrix commented 5 years ago

I think we could model this by treating typed holes as a resumable exception (or similar effect) and then providing a handler which nondeterministically tries a bunch of things, with pruning/runNonDetOnce behaviour.