Hi Oleg On 5 Jul 2007, at 07:15, oleg@pobox.com wrote:
Conor McBride has posed an interesting problem:
implement constructors P v for embedding pure values v O for holes f :$ a for application, left-associative and an interpreting function emmental such that emmental (P (+) :$ (P (*) :$ O :$ P 10) :$ O) 4 2 = 42
I believe one can do better. There is no need for the :$ operation, and there is no need for of lifting non-functional constants.
I was hoping for something of the sort. I'm glad you could oblige.
The following code demonstrates a more economical notation. The code essentially implements Hypothetical Reasoning, considering an expression with holes as an (intuitionistic) sequent. Each hole is one formula in the antecedent. The formulas in the antecedent are ordered, so our logic is actually the relevance, substructural intuitionistic logic. The function emmental takes the form of the Deduction Theorem (and its implementation is the proof of the theorem).
That's what I had in mind.
The test takes the form
test_McBride = dt ((ih *! (10::Int)) +! ih) 4 2 where ih = holet (undefined::Int)
and gives the predictable answer.
But perhaps you are cheating a bit...
infixl 6 +! infixl 7 *! infixr 5 !:
x +! y = l2 (+) x y x *! y = l2 (*) x y x `p` y = l2 (,) x y
x !: y = l2 (:) x y
...with lifting defined per arity. Of course you can use arity-specific overloading to hide the Ps and :$s, but you haven't given a closed solution to the general problem. By the way, we should, of course, also permit holes in function positions... *Emmental> emmental (O :$ P 3) (2 +) 5 ...but I don't imagine that's a big deal. So neither situation is particularly satisfying. I have a noisy but general solution; you have a technique for delivering less noisy solutions in whatever special cases might be desirable. I wonder if we can somehow extract the best from both. You've certainly taught me some useful tricks! Many thanks Conor