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

[Chung-chieh Shan]

oleg at pobox.com wrote in article <20070705061533.8965EAD43 at Adric.metnet.fnmoc.navy.mil> in gmane.comp.lang.haskell.cafe:
> 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

Hrm!  I don't see the original message where the problem was posed, but
it is indeed interesting.  Here is my solution, but I don't need "P",
"O", and ":$" to be constructors, so I rename them to "p", "o", and
"$:", respectively:

    emmental m = m id
    p x k = k x
    o k = k
    (m $: n) k = m (\f -> n (\x -> k (f x)))

    infixl 0 $:
    test = emmental (p (+) $: (p (*) $: o $: p 10) $: o) 4 2 -- 42

All credit is due to Danvy and Filinski (DIKU TR 89/12, Section 3.4;
later Danvy's "functional unparsing" paper, JFP 8(6)).  One way to
understand this code is that "o" is like the word "what" in a language
like Mandarin ("shenme") or Japanese ("dare") that does not move any
wh-word to the boundary of a clause.  In Japanese, "emmental" would
correspond to the "-ka" that marks the scope of a question and awaits
an answer (in this case the numbers 4 and 2).  Or, we have control
inversion: the argument to emmental is a sandboxed user process that
occasionally requests input.

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Gordon Brown's special advisors:
www.christianaid.org.uk/stoppoverty/climatechange/stories/special_advisers.aspx