# Lightweight sequent calculus and linear abstractions

 Classic List Threaded
4 messages
Reply | Threaded
Open this post in threaded view
|

## Lightweight sequent calculus and linear abstractions

 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. 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). The test takes the form > test_McBride = dt ((ih *! (10::Int)) +! ih) 4 2 >  where ih = holet (undefined::Int) and gives the predictable answer. Another test, which shows that we can pile up holes (aka hypotheses) at will, and they all line up: > test7 = let exp = l1 (map succ) ((1::Int) !: ih !: ih !: ih !: [5]) >      ih = holet (undefined::Int) >      deduced = dt exp >         in deduced 11 12 13 > -- [2,12,13,14,6] > test_order = dt( (ih `p` ih) `p` (ih `p` ih) ) 1 2 3 4 >  where ih = holet (undefined::Int) > -- ((1,2),(3,4)) It is clear from our examples that our holes are monomorphically typed; the lifted functions don't have to be. We could have implemented things the other way around. We could have played with more complex inferences when applying polymorphic functions to polymorphic sequents. At present, we chose the simplest solution. Here it is. {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} {-# OPTIONS -fallow-overlapping-instances #-} -- the extensions are merely for the sake of IsHypothetical below -- Lightweight sequent calculus: computations on sequents module SEQ where -- Hypothetical value: one formula in the antecedent newtype H a = H a -- The primitive sequent: a |- a hole :: H a -> a hole (H x) = x -- The version of the above to make it easy to assign a specific type to it holet :: a -> H a -> a holet _ = hole -- This class proves, by construction, the Deduction Theorem -- x |- b ==> x -> b class DeductionTh seq r | seq -> r where     dt :: seq -> r instance (IsHypothetical seq f, DeductionTh' f seq r)     => DeductionTh seq r where     dt = dt' (undefined::f) class DeductionTh' f seq r | f seq -> r where     dt' :: f -> seq -> r instance DeductionTh y r => DeductionTh' HTrue (H x -> y) (x->r) where     dt' _ hf = \x -> dt (hf (H x)) instance DeductionTh' HFalse a a where     dt' _ = id -- Lifting an a->b function to sequents class Lift1 a b arg res | a b arg -> res where     l1 :: (a->b) -> (arg->res) instance (IsHypothetical arg f, Lift1' f a b arg res)     => Lift1 a b arg res where     l1 = l1' (undefined::f) class Lift1' f a b arg res | f a b arg -> res where     l1' :: f -> (a->b) -> (arg->res) instance Lift1 a b y b' => Lift1' HTrue a b (H x -> y) (H x -> b') where     l1' _ fn arg = \hx -> l1 fn (arg hx) -- here we assert a local functional dependency instance TypeCast arg a => Lift1' HFalse a b arg b where     l1' _ fn arg = fn (typeCast arg) test1 = dt True test2 :: Int -> Int test2 = dt hole test2' = dt (holet (1::Int)) test3 = dt (l1 not True) test4 = dt (l1 not (holet False)) -- expected type error -- test4' = dt (l1 not (holet (1::Int))) test4'' = test4 False -- Lifting an a->b->c function to two sequents -- we should keep the order of formulas in the combined antecedent -- The following is just a funnily written `append' of two sequences class Lift2 a b c arg1 arg2 res | a b c arg1 arg2 -> res where     l2 :: (a->b->c) -> (arg1->arg2->res) instance (IsHypothetical arg1 f1,           IsHypothetical arg2 f2,           Lift2' f1 f2 a b c arg1 arg2 res)     => Lift2 a b c arg1 arg2 res where     l2 = l2' (undefined::f1) (undefined::f2) class Lift2' f1 f2 a b c arg1 arg2 res | f1 f2 a b c arg1 arg2 -> res where     l2' :: f1 -> f2 -> (a->b->c) -> (arg1->arg2->res) -- First, drain the antecedent formulas from arg1 instance Lift2 a b c y1 arg2 r     => Lift2' HTrue f2 a b c (H x1 -> y1) arg2 (H x1 -> r)  where  l2' _ _ fn arg1 arg2 = \hx1 -> l2 fn (arg1 hx1) arg2 -- now, add the antecedent formulas from arg2, if any instance Lift2 a b c x1 y2 r     => Lift2' HFalse HTrue a b c x1 (H x2 -> y2) (H x2 -> r)  where  l2' _ _ fn arg1 arg2 = \hx2 -> l2 fn arg1 (arg2 hx2) instance (TypeCast x1 a, TypeCast x2 b)     => Lift2' HFalse HFalse a b c x1 x2 c  where  l2' _ _ fn arg1 arg2 = fn (typeCast arg1) (typeCast arg2) -- Time for tests 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 test5  = dt ((1::Int) +! (2::Int)) test51 = dt (holet (1::Int) +! (2::Int)) test51' = test51 10     -- 12 test52 = dt (holet (undefined::Int) `p` holet True) test52' = test52 5 False  -- (5,False) test_McBride = dt ((ih *! (10::Int)) +! ih) 4 2  where ih = holet (undefined::Int) test6 = dt( l1 sum (ih !: ih !: ih !: [5]) ) 1 2 3  where ih = holet (undefined::Int) -- 11 test7 = let exp = l1 (map succ) ((1::Int) !: ih !: ih !: ih !: [5])             ih = holet (undefined::Int)             deduced = dt exp         in deduced 11 12 13 -- [2,12,13,14,6] -- Testing the proper ordering of formulas in the antecedent test_order = dt( (ih `p` ih) `p` (ih `p` ih) ) 1 2 3 4  where ih = holet (undefined::Int) -- ((1,2),(3,4)) -- see http://okmij.org/ftp/Haskell/typecast.html#deep-joindata HTrue data HFalse   class IsHypothetical a b | a -> b instance TypeCast f HTrue => IsHypothetical (H x->y) f instance TypeCast f HFalse => IsHypothetical a f class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' instance TypeCast'' () a a where typeCast'' _ x  = x _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Lightweight sequent calculus and linear abstractions

 Hi Oleg On 5 Jul 2007, at 07:15, [hidden email] 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Lightweight sequent calculus and linear abstractions

 In reply to this post by oleg-7 [hidden email] wrote in article <[hidden email]> 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/sigGordon Brown's special advisors: www.christianaid.org.uk/stoppoverty/climatechange/stories/special_advisers.aspx _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Re: Lightweight sequent calculus and linear abstractions

 On 5 Jul 2007, at 18:35, Chung-chieh Shan wrote: > [hidden email] wrote in article   > <[hidden email]> 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 Very nice! Thanks Conor _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe