[Haskell-cafe] Lightweight sequent calculus and linear abstractions

[oleg at pobox.com]

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-join

data 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