Hi, I'm running in errors that, I think, is related with functional dependence. But I don't know how to interpret or solve them. I have basically 3 types: Edge, Face and Simplex (Tetrahedron) and I want to combined them in a class type such that: - Edge and Face will produce a convex hull - Face and Simplex will produce a Delaunay triangulation under the same MCB (Marriage Before Conquer) algorithm. I first tried to use Multiparameter type class with functional dependence relation: class SubUnit subUnit unit | subUnit -> unit, unit -> subUnit where buildUnit :: ActiveSubUnit subUnit -> [Point] -> Maybe unit build1stUnit :: Plane -> [Point] -> [Point] -> [Point] -> Maybe unit getAllSubUnits :: unit -> [ActiveSubUnit subUnit] subUnitPos :: BoxPair -> subUnit -> Position but then I decide to go for a GADT form (If someone wants to try to compile it, one can get the complete code on GitHub: http://github.com/EdgarGomes/DeUni) : class SubUnit subUnit where type Unit subUnit :: * buildUnit :: ActiveSubUnit subUnit -> [Point] -> Maybe (Unit subUnit) build1stUnit :: Plane -> [Point] -> [Point] -> [Point] -> Maybe (Unit subUnit) getAllSubUnits :: Unit subUnit -> [ActiveSubUnit subUnit] subUnitPos :: BoxPair -> subUnit -> Position In both cases I get a couple of errors like: src/DeUni.hs:265:39: Couldn't match type `Unit subUnit3' with `Unit subUnit2' NB: `Unit' is a type function, and may not be injective Expected type: Unit a Actual type: Unit subUnit2 In the expression: un In the expression: [un] In the first argument of `return', namely `(([un], fromList $ getAllSubUnits un) :: SubUnit a => ([Unit a], SetActiveSubUnits a))' src/DeUni.hs:265:39: Couldn't match type `Unit (ActiveSubUnit subUnit3)' with `Unit subUnit2' NB: `Unit' is a type function, and may not be injective Expected type: Unit a Actual type: Unit subUnit2 In the expression: un In the expression: [un] In the first argument of `return', namely `(([un], fromList $ getAllSubUnits un) :: SubUnit a => ([Unit a], SetActiveSubUnits a))' src/DeUni.hs:265:44: Could not deduce (a1 ~ ActiveSubUnit subUnit3) from the context (SubUnit a) bound by the type signature for mbc :: SubUnit a => [Point] -> SetActiveSubUnits a -> Box -> StateMBC a [Unit a] at src/DeUni.hs:(260,1)-(317,53) or from (SubUnit a1) bound by an expression type signature: SubUnit a1 => ([Unit a1], SetActiveSubUnits a1) at src/DeUni.hs:265:37-117 `a1' is a rigid type variable bound by an expression type signature: SubUnit a1 => ([Unit a1], SetActiveSubUnits a1) at src/DeUni.hs:265:37 Expected type: SetActiveSubUnits a Actual type: Set (ActiveSubUnit subUnit3) In the expression: fromList $ getAllSubUnits un In the first argument of `return', namely `(([un], fromList $ getAllSubUnits un) :: SubUnit a => ([Unit a], SetActiveSubUnits a))' ..... ..... Any help is more than welcome! Cheers, Edgar Gomes (LambdaSteel)
For the specific error at line 265 I think you should be using ScopedTypeVariables and properly qualifying the type signature at the function level with a forall. The local annotation { ::(SubUnit a)=> } is presumably introducing another type variable unrelated to 'a' in the function level type signature. Note, my suggestion is "by eye" - I haven't run the code, so it may not work or there may be other errors.
Unfortunately it didn't work.
The error message is not so clear to me and my understanding in advanced
Haskell type system is yet to weak to figure out what is going on.
Looking at the error messages seems that the type inference analyzes the
code in two different direction and finds some inconsistency at some
junction point.
Couldn't match type `Unit subUnit3' with `Unit subUnit2'
NB: `Unit' is a type function, and may not be injective
How can I say that "Unit subUnit3" is "Unit subUnit2"?
The type of error message seems be caused by a very similar problem
Could not deduce (a1 ~ ActiveSubUnit subUnit3)
.......
Expected type: SetActiveSubUnits a
Actual type: Set (ActiveSubUnit subUnit3)
since "SetActiveSubUnits a" and "Set (ActiveSubUnit subUnit3)" should have
the same type.
Any new idea ?
Cheers,
Edgar Gomes
On 26 March 2011 16:13, Stephen Tetley
For the specific error at line 265 I think you should be using ScopedTypeVariables and properly qualifying the type signature at the function level with a forall.
The local annotation { ::(SubUnit a)=> } is presumably introducing another type variable unrelated to 'a' in the function level type signature.
Note, my suggestion is "by eye" - I haven't run the code, so it may not work or there may be other errors.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi Edgar What did you try? My intuition is that this specific bit (there may be other problems) is because the type checker is introducing a new type variable. Thus you don't actually want the type operator (~) to say the new type variable is equal to the type variable in the function signature, you want to use scoped type variables so that the local type annotation is *the same type* type variable. Best wishes Stephen
Hi Edgar
On 26 March 2011 20:19, Stephen Tetley
... you want to use scoped type variables so that the local type annotation is *the same type* type variable.
Ahem ...
so that the local type annotation is *the same type variable*.
Where is Data.Vec coming from so I can try to compile it myself? Best wishes Stephen
Hi Stephen,
I've have done the following:
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
...
mbc :: forall a . (SubUnit a)=>[Point] -> SetActiveSubUnits a -> Box ->
StateMBC a [Unit a]
mbc p afl box = do
cleanAFLs
if (null afl)
then do
(unit, afl') <- case build1stUnit plane p1 p2 p of
Just un -> return (([un], fromList $ getAllSubUnits
un)::(SubUnit a)=>([Unit a], SetActiveSubUnits a))
_ -> return ([] , empty)
analyze1stUnit unit afl'
.....
I hope that is right. Does it?
Edgar
On 26 March 2011 21:19, Stephen Tetley
Hi Edgar
What did you try?
My intuition is that this specific bit (there may be other problems) is because the type checker is introducing a new type variable. Thus you don't actually want the type operator (~) to say the new type variable is equal to the type variable in the function signature, you want to use scoped type variables so that the local type annotation is *the same type* type variable.
Best wishes
Stephen
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Saturday 26 March 2011 21:35:13, Edgar Gomes Araujo wrote:
Hi Stephen, I've have done the following:
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} ... mbc :: forall a . (SubUnit a)=>[Point] -> SetActiveSubUnits a -> Box -> StateMBC a [Unit a] mbc p afl box = do cleanAFLs if (null afl) then do (unit, afl') <- case build1stUnit plane p1 p2 p of Just un -> return (([un], fromList $ getAllSubUnits un)::(SubUnit a)=>([Unit a], SetActiveSubUnits a))
Remove the context, that's given in the signature: return (([un], fromList ...) :: ([Unit a], SetActiveSubUnits a))
_ -> return ([] , empty) analyze1stUnit unit afl' .....
I hope that is right. Does it?
@ Stephem: here is my build-depends: Vec -any, array -any, base -any,
containers -any, mtl -any.
You also can find a cabal file on my GitHub:
http://github.com/EdgarGomes/DeUni
http://github.com/EdgarGomes/DeUni@Daniel: In fact, I've inserted that
context trying to fix the problem but it affected nothing. I'll remove it.
Thank you guys, in advanced, for the collaboration!
Edgar
On 26 March 2011 21:50, Daniel Fischer
On Saturday 26 March 2011 21:35:13, Edgar Gomes Araujo wrote:
Hi Stephen, I've have done the following:
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} ... mbc :: forall a . (SubUnit a)=>[Point] -> SetActiveSubUnits a -> Box -> StateMBC a [Unit a] mbc p afl box = do cleanAFLs if (null afl) then do (unit, afl') <- case build1stUnit plane p1 p2 p of Just un -> return (([un], fromList $ getAllSubUnits un)::(SubUnit a)=>([Unit a], SetActiveSubUnits a))
Remove the context, that's given in the signature:
return (([un], fromList ...) :: ([Unit a], SetActiveSubUnits a))
_ -> return ([] , empty) analyze1stUnit unit afl' .....
I hope that is right. Does it?
Hi Edgar I think you have some errors of construction rather than just a problem with the type families / fun deps. Note, I've knocked off the class constraints on the data declarations on the copy I'm working with (e.g ActiveSubUnit) , this may or may not change things. This change to splitAF will type check, whether or not it does what you want:
splitAF::(SubUnit a, Ord a)=> BoxPair -> a -> StateMBC a () splitAF pairBox e = case subUnitPos pairBox e of
Your code was:
splitAF::(SubUnit a)=>BoxPair -> a -> StateMBC a () splitAF pairBox e = case subUnitPos pairBox (activeUnit e) of
getUnitsOnPlane will compile if you comment out the type sig, but GHC generates this type sig: getUnitsOnPlane :: (Unit su1 ~ Unit su, SubUnit (ActiveSubUnit su), SubUnit su1, SubUnit su, Ord su) => [Point] -> BoxPair -> t -> StateT (SubUnitsSets (ActiveSubUnit su)) Data.Functor.Identity.Identity [Unit su] -- Defined at DeUni.hs:324:1-15 Note the class constraints are introducing a type variable *su1* that isn't mentioned in the function arguments, this strongly makes me think the function body isn't doing what it should. Also GHC infers a type var *t* rather than Plane for the second arg, again this makes me think the function body is not right. I'm a bit at a loss with the mbc function, if I comment out the function type sig and local type sigs GHC generates some errors mentioning Edge - as Edge is one of the instances of SubUnit, I think the function body is less polymorphic than you expect. Best wishes Stephen
Dear Stephan,
Finally!!!! It's alive and working, huhhuu! After 3 long days...
As predictable, it was my fault. There was basically two big mistakes:
- splitAF::(SubUnit a b, Ord a)=>BoxPair -> ActiveSubUnit a -> StateMBC a
()
instead of "splitAF::(SubUnit a, Ord a)=> BoxPair -> a -> StateMBC a ()"
- type SetActiveSubUnits a = Set (ActiveSubUnit a)
instead of "type SetActiveSubUnits a = Set a"
After those corrections there was one error remaining:
src/DeUni.hs:264:39:
Could not deduce (Unit a ~ Unit subUnit0)
from the context (SubUnit a, Ord a)
bound by the type signature for
mbc :: (SubUnit a, Ord a) => [Point] -> SetActiveSubUnits
a -> Box -> StateMBC a [Unit a]
at src/DeUni.hs:(253,1)-(310,53)
NB: `Unit' is a type function, and may not be injective
Expected type: [Unit a]
Actual type: [Unit subUnit0]
Then I decided to go back to Fun Dep instead of GADT due the "injective"
complain.
class SubUnit subUnit unit | subUnit -> unit, unit -> subUnit where
.....
instead of
class SubUnit subUnit where
type Unit subUnit :: *
.....
And ... Bingo!
My last question, how can I make it work using GADT?
Thank so much for your kindly assistance.
Edgar
On 26 March 2011 23:13, Stephen Tetley
Hi Edgar
I think you have some errors of construction rather than just a problem with the type families / fun deps.
Note, I've knocked off the class constraints on the data declarations on the copy I'm working with (e.g ActiveSubUnit) , this may or may not change things.
This change to splitAF will type check, whether or not it does what you want:
splitAF::(SubUnit a, Ord a)=> BoxPair -> a -> StateMBC a () splitAF pairBox e = case subUnitPos pairBox e of
Your code was:
splitAF::(SubUnit a)=>BoxPair -> a -> StateMBC a () splitAF pairBox e = case subUnitPos pairBox (activeUnit e) of
getUnitsOnPlane will compile if you comment out the type sig, but GHC generates this type sig:
getUnitsOnPlane :: (Unit su1 ~ Unit su, SubUnit (ActiveSubUnit su), SubUnit su1, SubUnit su, Ord su) => [Point] -> BoxPair -> t -> StateT (SubUnitsSets (ActiveSubUnit su)) Data.Functor.Identity.Identity [Unit su] -- Defined at DeUni.hs:324:1-15
Note the class constraints are introducing a type variable *su1* that isn't mentioned in the function arguments, this strongly makes me think the function body isn't doing what it should. Also GHC infers a type var *t* rather than Plane for the second arg, again this makes me think the function body is not right.
I'm a bit at a loss with the mbc function, if I comment out the function type sig and local type sigs GHC generates some errors mentioning Edge - as Edge is one of the instances of SubUnit, I think the function body is less polymorphic than you expect.
Best wishes
Stephen
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Daniel Fischer -
Edgar Gomes Araujo -
Stephen Tetley