[Haskell-cafe] Re: Lightweight sequent calculus and linear abstractions

[Conor McBride]

Hi Oleg

On 5 Jul 2007, at 07:15, oleg at 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