I have some type-level sets using fundeps working whereby equality and membership etc are predicate functions. This seems to leads to an explosion of ugly code, with `If' class constraints etc getting out of hand -- I want to treat these as relations instead so providing the definition describes everything that is 'in' and nothing that is 'out'. I've been using Oleg's paper on lightweight static resources [1] as a template for this. I want to do something like this (supposing I have an EQ relation, (:::) for consing): class Member x y instance EQ x y => Member x (y:::ys) instance Member x ys => Member x (y:::ys) But I can certainly see why this isn't possible (It's the equivalent of pattern-matching on the constraints I suppose). Do type families provide a way to do this kind of thing or do I need a different strategy altogether, involving GADTs or whatever? Thanks, [1] http://okmij.org/ftp/Computation/resource-aware-prog/tfp.pdf -- View this message in context: http://www.nabble.com/fundeps-and-overlapping-undecidable-instances-tf496299... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
Hello, You should be able to use fundeps to do exactly what you describe below. Can you make a relatively small self-contained example which exemplifies the ugliness you see? -Jeff haskell-cafe-bounces@haskell.org wrote on 12/07/2007 11:24:35 AM:
I have some type-level sets using fundeps working whereby equality and membership etc are predicate functions. This seems to leads to an
explosion
of ugly code, with `If' class constraints etc getting out of hand -- I want to treat these as relations instead so providing the definition describes everything that is 'in' and nothing that is 'out'. I've been using Oleg's paper on lightweight static resources [1] as a template for this. I want to do something like this (supposing I have an EQ relation, (:::) for consing):
class Member x y instance EQ x y => Member x (y:::ys) instance Member x ys => Member x (y:::ys)
But I can certainly see why this isn't possible (It's the equivalent of pattern-matching on the constraints I suppose). Do type families provide a way to do this kind of thing or do I need a different strategy altogether, involving GADTs or whatever?
Thanks,
[1] http://okmij.org/ftp/Computation/resource-aware-prog/tfp.pdf -- View this message in context: http://www.nabble.com/fundeps-and- overlapping-undecidable-instances-tf4962996.html#a14215583 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
--- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.
On Fri, 2007-12-07 at 12:49 -0500, Jeff Polakow wrote:
Hello,
You should be able to use fundeps to do exactly what you describe below.
Can you make a relatively small self-contained example which exemplifies the ugliness you see?
Hi Jeff, as well as a minor code explosion if Member returns a (phantom type representing a) boolean then you have to decide what to do if the element is already in -- return the set unchanged I should think, but in other cases it might not be obvious so I want this and other things to be relations. So I had class If p x y c | p x y -> c where if :: p -> x -> y -> c instance If True x y x instance If False x y y class Member el set b | el set -> b where member :: el -> set -> b instance x Nil False instance (Eq x y c , Member x ys b , Or c d b) => Member x (y ::: ys) b (Eq and Or being more constraints that return True or False) I want a version that is only defined where the element is in the set -- not a test, an assertion. Jim
-Jeff
haskell-cafe-bounces@haskell.org wrote on 12/07/2007 11:24:35 AM:
I have some type-level sets using fundeps working whereby equality
membership etc are predicate functions. This seems to leads to an explosion of ugly code, with `If' class constraints etc getting out of hand -- I want to treat these as relations instead so providing the definition describes everything that is 'in' and nothing that is 'out'. I've been using Oleg's paper on lightweight static resources [1] as a template for this. I want to do something like this (supposing I have an EQ relation, (:::) for consing):
class Member x y instance EQ x y => Member x (y:::ys) instance Member x ys => Member x (y:::ys)
But I can certainly see why this isn't possible (It's the equivalent of pattern-matching on the constraints I suppose). Do type families
and provide a
way to do this kind of thing or do I need a different strategy altogether, involving GADTs or whatever?
Thanks,
[1] http://okmij.org/ftp/Computation/resource-aware-prog/tfp.pdf -- View this message in context: http://www.nabble.com/fundeps-and- overlapping-undecidable-instances-tf4962996.html#a14215583 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
---
This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.
Hello, Does the following code work for you? -Jeff --------------------------- {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances #-} data Nil = Nil data x ::: xs = x ::: xs infixr 5 ::: data HTrue = HTrue deriving Show data HFalse = HFalse deriving Show class Member x xs b | x xs -> b where member :: x -> xs -> b instance Member x Nil HFalse where member _ _ = HFalse instance Member x xs b => Member x (x ::: xs) HTrue where member _ _ = HTrue instance Member x xs b => Member x (y ::: xs) b where member x (_ ::: xs) = member x xs {- member 'a' (() ::: "a" ::: '1' ::: Nil) ==> HTrue member 'a' (() ::: "a" ::: Nil) ==> HFalse -} --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.
participants (3)
-
Jeff Polakow -
jim burton -
Jim Burton