Automating injections: adding a type parameter
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.pdfhttp://www.cse.chalmers.se/%7Ewouter//Publications/DataTypesALaCarte.pdf http://www.cse.chalmers.se/~wouter//Misc/LaCarte.hshttp://www.cse.chalmers.se/%7Ewouter//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"
Am Donnerstag 15 April 2010 19:19:15 schrieb Romulus:
Hello everyone,
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.
The expression (Land' x y) can have the type (Land' q (Mu (f p))) for all q. But there's only an instance for the p used in Mu (f p) provided, so Could not deduce (LAnd' p :<: f p1) from the context (LAnd' p1 :<: f p1) The solution is to tell the compiler that this expression should have the type LAnd' p (Mu (f p)) for the f and p from the type signature, add {-# LANGUAGE ScopedTypeVariables #-} and modify land' to land' :: forall f p. ((LAnd' p) :<: (f p)) => Mu (f p) -> Mu (f p) -> Mu (f p) land' = \x y -> inject (LAnd' x y :: LAnd' p (Mu (f p))) to be greeted by [1 of 1] Compiling Prop ( PropSample.hs, interpreted ) PropSample.hs:31:16: Warning: Declaration of `In' uses deprecated syntax Instead, use the form In :: {out :: f (Mu f)} -> Mu f Ok, modules loaded: Prop. *Prop> by 6.12.1 and $ ghci-6.10.3 PropSample GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Prop ( PropSample.hs, interpreted ) Ok, modules loaded: Prop. *Prop> from the older GHC.
Cheers,
PS: haskellers rulez ;)
+1
[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
Clear and concise answer.
Thank you.
On Thu, Apr 15, 2010 at 21:24, Daniel Fischer
Am Donnerstag 15 April 2010 19:19:15 schrieb Romulus:
Hello everyone,
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.
The expression (Land' x y) can have the type (Land' q (Mu (f p))) for all q. But there's only an instance for the p used in Mu (f p) provided, so
Could not deduce (LAnd' p :<: f p1) from the context (LAnd' p1 :<: f p1)
The solution is to tell the compiler that this expression should have the type LAnd' p (Mu (f p)) for the f and p from the type signature, add
{-# LANGUAGE ScopedTypeVariables #-}
and modify land' to
land' :: forall f p. ((LAnd' p) :<: (f p)) => Mu (f p) -> Mu (f p) -> Mu (f p) land' = \x y -> inject (LAnd' x y :: LAnd' p (Mu (f p)))
to be greeted by
[1 of 1] Compiling Prop ( PropSample.hs, interpreted )
PropSample.hs:31:16: Warning: Declaration of `In' uses deprecated syntax Instead, use the form In :: {out :: f (Mu f)} -> Mu f Ok, modules loaded: Prop. *Prop>
by 6.12.1 and
$ ghci-6.10.3 PropSample GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Prop ( PropSample.hs, interpreted ) Ok, modules loaded: Prop. *Prop>
from the older GHC.
Cheers,
PS: haskellers rulez ;)
+1
[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"
participants (2)
-
Daniel Fischer -
Romulus