Hello *, I am trying to extend the finite-domain (FD) constraint solver proposed by David Overton (http://overtond.blogspot.com/2008/07/pre.html) with arithmetic constraints by means of an embedded DSL. In principle, this is a very natural thing to do in a functional language; it is basically a matter of defining some suitable operators: data FDVar = FDVar Int deriving Show -- the type of FD variables data AExp = --the type of arithmetic expression over FD variables and integers IntegerConstant Int | Variable FDVar | Addition AExp AExp | Subtraction AExp AExp | Multiplication AExp AExp | IntegerDivision AExp AExp deriving Show infixl 7 #* -- multiplication infixl 7 #/ -- integer division infixl 6 #+ -- addition infixl 6 #- -- subtraction (#+), (#-), (#*), (#/) :: (MakeAExp a, MakeAExp b) => a -> b -> AExp (#+) = parseArgs Addition (#-) = parseArgs Subtraction (#*) = parseArgs Multiplication (#/) = parseArgs IntegerDivision with class MakeAExp a where makeAExp :: a -> AExp instance MakeAExp Int where makeAExp = IntegerConstant instance MakeAExp FDVar where makeAExp = Variable instance MakeAExp AExp where makeAExp = id parseArgs :: (MakeAExp a, MakeAExp b) => (AExp -> AExp -> c) -> a -> b -> c parseArgs f x y = f (makeAExp x) (makeAExp y) So far, so good. To avoid that FD variables escape their constraint stores, David employed a phantom type variable s leading to newtype FDVar s = FDVar { unFDVar :: Int } deriving (Ord, Eq) Trying to thread the phantom variable through my DSL implementation, I ended up with the following code: data AExp s = IntegerConstant Int | Variable (FDVar s) | Addition (AExp s) (AExp s) | Subtraction (AExp s) (AExp s) | Multiplication (AExp s) (AExp s) | IntegerDivision (AExp s) (AExp s) class MakeAExp a s where makeAExp :: a -> AExp s instance MakeAExp Int s where makeAExp = IntegerConstant instance MakeAExp (FDVar s) s where makeAExp x = Variable x instance MakeAExp (AExp s) s where makeAExp = id parseArgs :: (MakeAExp a s, MakeAExp b s) => (AExp s -> AExp s -> c s) -> a -> b -> c s parseArgs f x y = f (makeAExp x) (makeAExp y) infixl 7 #* -- multiplication infixl 7 #/ -- integer division infixl 6 #+ -- addition infixl 6 #- -- subtraction (#+), (#-), (#*), (#/) :: (MakeAExp a s, MakeAExp b s) => a -> b -> AExp s (#+) = parseArgs Addition (#-) = parseArgs Subtraction (#*) = parseArgs Multiplication (#/) = parseArgs IntegerDivision This code works if only one operator is applied: *FD> :type let x = (1::Int) in x #+ x let x = (1::Int) in x #+ x :: AExp s but *FD> :type let x = (1::Int) in x #+ x #+ x let x = (1::Int) in x #+ x #+ x :: (MakeAExp (AExp s) s1) => AExp s1 It appears to me that ghci generates two phantom types s and s1 and fails to unify them. Only the extensive use of type constraints seems to help like in the following example, where I used Int as phantom type: *FD> :type ((((1::Int) #+ (1::Int)) :: AExp Int) #+ (2::Int))::AExp Int ((((1::Int) #+ (1::Int)) :: AExp Int) #+ (2::Int))::AExp Int :: AExp Int But this approach only works on the command line and is out of question anyway. Any idea how to make my code work? I am using ghc 6.8.2 with {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} Thanks, Michael
Michael Marte <marte@pms.informatik.uni-muenchen.de> wrote in article <200810232156.19080.marte@pms.informatik.uni-muenchen.de> in gmane.comp.lang.haskell.general:
*FD> :type let x = (1::Int) in x #+ x #+ x let x = (1::Int) in x #+ x #+ x :: (MakeAExp (AExp s) s1) => AExp s1
It appears to me that ghci generates two phantom types s and s1 and fails to unify them.
Because you may define other MakeAExp instances elsewhere, ghc can't unify s and s1. For example, if you were to define instance MakeAExp (FDVar s) [s] ... instance MakeAExp (AExp [s]) s ... then s could be [s1] in your type! You can probably add functional dependencies to fix this problem, but I would suggest that you get rid of MakeAExp altogether. Just give (#+) and its friends the type "AExp s -> AExp s -> AExp s", with no type-class constraint. You need to explicitly inject FDVar into AExp, but most of the time you probably just need to handle AExp values without caring that they are constructed with Variable. You also need to inject Int into AExp, unless you simply make "instance Num (AExp s)". -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig Lemonade was a popular drink and it still is.
Hi Michael, You need a functional depenency in the class to make this work. Something like class MakeAExp a s | a -> s where makeAExp :: a -> AExp s should work, although I haven't tested it with your code. I did actually extend my FD constraint solver with arithmetic constraints myself, but I never got time to post it on my blog. It's also very inefficient at the moment, at least compared to the clp(fd) solver in GnuProlog. I took a slightly different approach to you. Instead of using an algebraic data type for expressions, I represent each node in the expression as a new FDVar in the constraint store. I've attached a copy of my code if you're interested. Let me know how you get on. David 2008/10/24 Michael Marte <marte@pms.informatik.uni-muenchen.de>:
Hello *,
I am trying to extend the finite-domain (FD) constraint solver proposed by David Overton (http://overtond.blogspot.com/2008/07/pre.html) with arithmetic constraints by means of an embedded DSL. In principle, this is a very natural thing to do in a functional language; it is basically a matter of defining some suitable operators:
data FDVar = FDVar Int deriving Show -- the type of FD variables
data AExp = --the type of arithmetic expression over FD variables and integers IntegerConstant Int | Variable FDVar | Addition AExp AExp | Subtraction AExp AExp | Multiplication AExp AExp | IntegerDivision AExp AExp deriving Show
infixl 7 #* -- multiplication infixl 7 #/ -- integer division
infixl 6 #+ -- addition infixl 6 #- -- subtraction
(#+), (#-), (#*), (#/) :: (MakeAExp a, MakeAExp b) => a -> b -> AExp (#+) = parseArgs Addition (#-) = parseArgs Subtraction (#*) = parseArgs Multiplication (#/) = parseArgs IntegerDivision
with
class MakeAExp a where makeAExp :: a -> AExp
instance MakeAExp Int where makeAExp = IntegerConstant
instance MakeAExp FDVar where makeAExp = Variable
instance MakeAExp AExp where makeAExp = id
parseArgs :: (MakeAExp a, MakeAExp b) => (AExp -> AExp -> c) -> a -> b -> c parseArgs f x y = f (makeAExp x) (makeAExp y)
So far, so good.
To avoid that FD variables escape their constraint stores, David employed a phantom type variable s leading to
newtype FDVar s = FDVar { unFDVar :: Int } deriving (Ord, Eq)
Trying to thread the phantom variable through my DSL implementation, I ended up with the following code:
data AExp s = IntegerConstant Int | Variable (FDVar s) | Addition (AExp s) (AExp s) | Subtraction (AExp s) (AExp s) | Multiplication (AExp s) (AExp s) | IntegerDivision (AExp s) (AExp s)
class MakeAExp a s where makeAExp :: a -> AExp s
instance MakeAExp Int s where makeAExp = IntegerConstant
instance MakeAExp (FDVar s) s where makeAExp x = Variable x
instance MakeAExp (AExp s) s where makeAExp = id
parseArgs :: (MakeAExp a s, MakeAExp b s) => (AExp s -> AExp s -> c s) -> a -> b -> c s parseArgs f x y = f (makeAExp x) (makeAExp y)
infixl 7 #* -- multiplication infixl 7 #/ -- integer division
infixl 6 #+ -- addition infixl 6 #- -- subtraction
(#+), (#-), (#*), (#/) :: (MakeAExp a s, MakeAExp b s) => a -> b -> AExp s (#+) = parseArgs Addition (#-) = parseArgs Subtraction (#*) = parseArgs Multiplication (#/) = parseArgs IntegerDivision
This code works if only one operator is applied:
*FD> :type let x = (1::Int) in x #+ x let x = (1::Int) in x #+ x :: AExp s
but
*FD> :type let x = (1::Int) in x #+ x #+ x let x = (1::Int) in x #+ x #+ x :: (MakeAExp (AExp s) s1) => AExp s1
It appears to me that ghci generates two phantom types s and s1 and fails to unify them.
Only the extensive use of type constraints seems to help like in the following example, where I used Int as phantom type:
*FD> :type ((((1::Int) #+ (1::Int)) :: AExp Int) #+ (2::Int))::AExp Int ((((1::Int) #+ (1::Int)) :: AExp Int) #+ (2::Int))::AExp Int :: AExp Int
But this approach only works on the command line and is out of question anyway.
Any idea how to make my code work?
I am using ghc 6.8.2 with
{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-}
Thanks, Michael _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Hello David, thank you, the functional dependency solved the problem! Nevertheless, I think it is worth considering the phantom type variable a second time. It makes easy things quite hard and requires a lot of not-(yet?)-standard features of the type system. As there is usually no second problem instance a variable could escape to, the price for the theoretical safety is probably too high. I studied your solver for arithmetic constraints and, after some thinking, I prefer your approach over mine because it is more natural (no posting function required that implements the compiler) though it does not allow for automatic analysis and transformations. For example, with the ADT approach a system of linear equalities and inequalities could be recognized as a linear program and replaced by a specialized global lp constraint. However, as the lp constraint can be applied directly as well, omitting the transformation stage does not hurt. Concering bad performance, there are several things that come to my mind: * Domain access in not O(1). varMap should be replaced by an array. * Pruning IntSet domains is inefficient: filterLessThan and filterGreaterThan are O(n) due to the use of IntSet.filter which should be replaced by IntSet.split. * No search strategy: One should always try to label one of the "most constrained" variables. A proven way to do this is to label one of the variables with the smallest domain. * Splitting domains instead of labelling: Depending on the problem, on the way it is modelled, and on the operational properties of the constraints employed in the model, it may be better to split domains, i.e. choose a non-ground variable x and generate two subproblems, one with x .=<. a and one with x .>. a where a is some element between the lower and upper bound of x, usually the middle. * Correctness: The implementation of .*. is faulty; its pruning is too strong: *FD> clp (do x <- newNamedVar (0, 9) "x"; 10 .*. x .==. 90) _1: (10,10) _2: (90,90) _3: (90,90) x: (9,9) ? ; no *FD> clp (do x <- newNamedVar (0, 9) "x"; 10 .*. x .==. 80) no (The clp and newNamedVar functions are described on http://mmartedp.blogspot.com/ and contained in the patch I attached to this mail.) That's why sendMoreMoney has no solutions and, of course, bugs like this one may render easy problems difficult by pruning solutions resulting in long runtimes. Michael On Friday 24 October 2008 01:17:07 am you wrote:
Hi Michael,
You need a functional depenency in the class to make this work. Something like
class MakeAExp a s | a -> s where makeAExp :: a -> AExp s
should work, although I haven't tested it with your code.
I did actually extend my FD constraint solver with arithmetic constraints myself, but I never got time to post it on my blog. It's also very inefficient at the moment, at least compared to the clp(fd) solver in GnuProlog.
I took a slightly different approach to you. Instead of using an algebraic data type for expressions, I represent each node in the expression as a new FDVar in the constraint store. I've attached a copy of my code if you're interested. Let me know how you get on.
David
participants (3)
-
Chung-chieh Shan -
David Overton -
Michael Marte