Hello everyone,

It's my very first post to this mailing list, though i read it for several months.

I'm very interested in Swiertra's automatic injection technique [1].
http://www.cse.chalmers.se/~wouter//Publications/DataTypesALaCarte.pdf
http://www.cse.chalmers.se/~wouter//Misc/LaCarte.hs

As a first exercise, i've tried to write an interpreter/transformer for propositional logic, in the spirit of [2].
http://www.haskell.org/sitewiki/images/6/6a/TMR-Issue11.pdf

data LProp r = LProp String
instance Functor LProp where
    fmap _ (LProp x) =  LProp x
data LAnd r = LAnd r r
instance Functor LAnd where
    fmap f (LAnd x y) = LAnd (f x) (f y)


Automatic injections are cool things to write helpers that work with any type for formulae extending LProp with coproducts:

-- not very expressive, but it's not the point
type ConjLogicF = LProp :+: LAnd
type ConjLogic = Mu ConjLogicF

lprop :: (LProp :<: f) => String -> Mu f
lprop = \s -> inject (LProp s)
land :: (LAnd :<: f) => Mu f -> Mu f -> Mu f
land = \x y -> inject (LAnd x y)


However, i'd like to parameterize the type of propositionnal variables for the logic, that is, not only strings, but a given type parameter p. For instance (that should make LProp' and LAnd' bifunctors i guess):

data LProp' p r = LProp' p
instance Functor (LProp' p) where
    fmap _ (LProp' x) =  LProp' x
data LAnd' p r = LAnd' r r
instance Functor (LAnd' p) where
    fmap f (LAnd' x y) = LAnd' (f x) (f y)

type ConjLogicF' p = (LProp' p) :+: (LAnd' p)
type ConjLogic' p = Mu (ConjLogicF' p)

lprop' :: ((LProp' p) :<: (f p)) => p -> Mu (f p)
lprop' = \x -> inject (LProp' x)

I'm stuck with the definition of the helper for LAnd'. I expect :

land' :: ((LAnd' p) :<: (f p)) =>  Mu (f p) ->  Mu (f p) ->  Mu (f p)
land' = \x y -> inject (LAnd' x y)

... but ghci 6.10.4 does not really like this definition...

    Could not deduce (LAnd' p :<: f p1)
      from the context (LAnd' p1 :<: f p1)
      arising from a use of `inject' at PropSample.hs:128:16-33
    Possible fix:
      add (LAnd' p :<: f p1) to the context of
        the type signature for `land''
      or add an instance declaration for (LAnd' p :<: f p1)
    In the expression: inject (LAnd' x y)
    In the expression: \ x y -> inject (LAnd' x y)
    In the definition of `land'': land' = \ x y -> inject (LAnd' x y)
Failed, modules loaded: none.



Does anybody have a clue for this problem ?
I don't really understand where is the trouble actually.

Cheers,

PS: haskellers rulez ;)


[1]
Swierstra, W.
Data types à la carte
J. Funct. Program.
Cambridge University Press, 2008, 18, 423-436

[2]
Knowles, K.
First-Order Logic à la Carte
The Monad.Reader, 2008, issue 11


--
Romuald THION
Docteur level 1.0 - Great master access control, +3 against half-dead
"la vie, c'est comme un jeu mal foutu dont on ne connait pas les règles et où il n'y a pas de sauvegardes"