[Haskell-cafe] Re: Lightweight sequent calculus and linear
abstractions
Conor McBride
ctm at Cs.Nott.AC.UK
Thu Jul 5 06:26:22 EDT 2007
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
More information about the Haskell-Cafe
mailing list