Hi Oleg
On 5 Jul 2007, at 07:15, [EMAIL PROTECTED] 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
