Re: [Haskell-cafe] A type class puzzle
On 11/2/06, Yitzchak Gale [EMAIL PROTECTED] wrote: GHC says: Functional dependencies conflict between instance declarations: instance Replace Zero a a (a - a - a) instance (...) = Replace (Succ n) a [l] f' Not true. The type constraints on the second instance prevent any overlap. GHC doesn't take constraints into account when checking fundeps. You're looking for Sulzmann's Chameleon, which does all sorts of constraint magic. http://www.comp.nus.edu.sg/~sulzmann/chameleon/ Also, I'd be surprized if Oleg didn't have a work-around in GHC. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
On Tue, Oct 31, 2006 I wrote:
Consider the following sequence of functions
that replace a single element in an n-dimensional
list:
replace0 :: a - a - a
replace1 :: Int - a - [a] - [a]
replace2 :: Int - Int - a - [[a]] - [[a]]
Generalize this using type classes.
Thanks to everyone for the refernces about the
variadic composition operator.
However, that technique only provides a variable
number of arguments at the end of the argument
list (like in C, etc.). The puzzle as stated requires
them at the beginning.
Below is a proposed full solution. Unfortunately,
it compiles neither in Hugs nor in GHC. But I don't
understand why not.
GHC says:
Functional dependencies conflict between instance declarations:
instance Replace Zero a a (a - a - a)
instance (...) = Replace (Succ n) a [l] f'
Not true. The type constraints on the second instance
prevent any overlap.
Hugs says:
ERROR ./Replace.hs:63 - Instance is more general than a dependency allows
*** Instance : Replace (Succ a) b [c] d
*** For class: Replace a b c d
*** Under dependency : a b - c d
Not true. The type constraints limit the scope to within the fundeps.
Here is the program:
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
We will need ordinals to count the number of initial function arguments.
data Zero = Zero
data Succ o = Succ o
class Ordinal o where
ordinal :: o
instance Ordinal Zero where
ordinal = Zero
instance Ordinal n = Ordinal (Succ n) where
ordinal = Succ ordinal
Args is a model for functions with a variable number of
initial arguments of homogeneous type.
data Args a b = Args0 b | ArgsN (a - Args a b)
instance Functor (Args a) where
fmap f (Args0 x) = Args0 $ f x
fmap f (ArgsN g) = ArgsN $ fmap f . g
constN is a simple example of an Args. It models a variation
on const (well, flip const, actually) that ignores a variable
number of initial arguments.
class Ordinal n = ConstN n where
constN :: n - b - Args a b
instance ConstN Zero where
constN _ = Args0
instance ConstN n = ConstN (Succ n) where
constN (Succ o) = ArgsN . const . constN o
We can convert any Args into the actual function that it represents.
(The inverse is also possible, but we do not need that here.)
class Ordinal n = ArgsToFunc n a b f where
argsToFunc :: n - Args a b - f
instance ArgsToFunc Zero a b b where
argsToFunc _ (Args0 b) = b
instance ArgsToFunc n a b f = ArgsToFunc (Succ n) a b (a - f) where
argsToFunc (Succ o) (ArgsN g) = argsToFunc o . g
When the return type is itself a function, we will need to flip
arguments of the internal function out of the Args.
flipOutArgs :: Args a (b - c) - b - Args a c
flipOutArgs (Args0 f) = Args0 . f
flipOutArgs (ArgsN f) x = ArgsN $ flip flipOutArgs x . f
flipInArgs is the inverse of flipOutArgs. It requires an ordinal, because
we need to know how far in to flip the argument.
class Ordinal n = FlipInArgs n where
flipInArgs :: n - (b - Args a c) - Args a (b - c)
instance FlipInArgs Zero where
flipInArgs _ f = Args0 $ argsToFunc Zero . f
instance FlipInArgs n = FlipInArgs (Succ n) where
flipInArgs (Succ o) f = ArgsN $ flipInArgs o . g
where g x y = let ArgsN h = f y in h x
Now we are ready to construct replace.
class ArgsToFunc n Int (a - l - l) f =
Replace n a l f | n a - l f, f - n a l
where
replaceA :: n - Args Int a
replace :: f
instance Replace Zero a a (a - a - a) where
replaceA _ = Args0 const
replace = const
instance (Replace n a l f, FlipInArgs n, ConstN n,
ArgsToFunc (Succ n) Int (a - [l] - [l]) f') =
Replace (Succ n) a [l] f' where
replaceA (Succ o) = ArgsN mkReplace
where
mkReplace i = flipInArgs o $ flipInArgs o . mkRepl o i
mkRepl o i x xs
| null t= constN o h
| otherwise = fmap (h ++) $ fmap (: tail t) $
flipOutArgs (flipOutArgs (replaceA o) x) xs
where (h, t) = splitAt i xs
replace = argsToFunc ordinal $ replaceA ordinal
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A type class puzzle
Consider the following sequence of functions that replace a single element in an n-dimensional list: replace0 :: a - a - a replace0 = const replace1 :: Int - a - [a] - [a] replace1 i0 x xs | null t= h | otherwise = h ++ (replace0 x (head t) : tail t) where (h, t) = splitAt i0 xs replace2 :: Int - Int - a - [[a]] - [[a]] replace2 i0 i1 x xs | null t= h | otherwise = h ++ (replace1 i1 x (head t) : tail t) where (h, t) = splitAt i0 xs etc. Generalize this using type classes. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
On Tue, Oct 31, 2006 at 11:02:03AM +0200, Yitzchak Gale wrote: Consider the following sequence of functions that replace a single element in an n-dimensional list: replace0 :: a - a - a replace1 :: Int - a - [a] - [a] replace2 :: Int - Int - a - [[a]] - [[a]] Generalize this using type classes. It's quite easy if you allow the indices to be put in a single compound value. If you insist that each index should be given as a separate function argument, it may be possible to achieve it using the tricks that allow to write the variadic composition operator. Here's my version using MPTCs and fundeps: data Index t = I Int t class Replace i l a | i a - l where replace :: i - a - l - l instance Replace () a a where replace _ = const instance Replace i l a = Replace (Index i) [l] a where replace (I i0 is) x xs | null t= h | otherwise = h ++ (replace is x (head t) : tail t) where (h, t) = splitAt i0 xs Example use: *Nested :t replace (I 0 $ I 2 $ I 3 $ ()) qweqwe replace (I 0 $ I 2 $ I 3 $ ()) qweqwe :: Char - Char Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
Tomasz Zielonka wrote: It's quite easy if you allow the indices to be put in a single compound value. Hmm. Well, I guess I don't need to insist on the exact type that I gave in the statement of the puzzle - although something like that would be the nicest. This is actually a function that is useful quite often in practice. But I would rather not be forced to write things like replace (I 0 $ I 2 $ I 3 $ ()) in my code. My first attempt was very similar to yours, except I used replace (0, (2, (3, ( instead of your Index type. I don't like my solution, either. So I guess I would define a full solution as something nice enough to be used in practice. Let's be more concrete - it has to be nice enough that most people who need, say, replace2 or replace3, in real life, would actually use your function instead of writing it out by hand. Maybe others would disagree, but so far, I personally do not use either your solution or my solution. I write it out by hand. If you insist that each index should be given as a separate function argument, it may be possible to achieve it using the tricks that allow to write the variadic composition operator. I am not familiar with that. Do you have a reference? Is that the best way to do it? (Is that a way to do it at all?) Thanks, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
Yitzchak Gale wrote: Tomasz Zielonka wrote: If you insist that each index should be given as a separate function argument, it may be possible to achieve it using the tricks that allow to write the variadic composition operator. I am not familiar with that. Do you have a reference? Is that the best way to do it? (Is that a way to do it at all?) You might find these articles somewhat related... Functions with the variable number of (variously typed) arguments http://okmij.org/ftp/Haskell/types.html#polyvar-fn Deepest functor [was: fmap for lists of lists of lists of ...] http://okmij.org/ftp/Haskell/deepest-functor.lhs ...That first article is the strangest. I couldn't reconcile the fact that if our type signature specifies two arguments, we can pattern match on three arguments in the function definition. Compare the number of arguments in the first and second instances... class BuildList a r | r- a where build' :: [a] - a - r instance BuildList a [a] where build' l x = reverse$ x:l instance BuildList a r = BuildList a (a-r) where build' l x y = build'(x:l) y ...if you try something like... foo :: [a] - a - r foo l x y = undefined ...you'll get an error message like... The equation(s) for `foo' have three arguments, but its type `[a] - a - r' has only two YMMV, Greg Buchholz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] A type class puzzle
See Connor McBride's Faking It: Simulating Dependent Types in Haskell http://citeseer.ist.psu.edu/mcbride01faking.html It might help; your example makes me think of the nthFirst function. If it's different, I'md wager the polyvariadic stuff and nthFirst can be reconciled on some level. Nick On 10/31/06, Greg Buchholz [EMAIL PROTECTED] wrote: Yitzchak Gale wrote: Tomasz Zielonka wrote: If you insist that each index should be given as a separate function argument, it may be possible to achieve it using the tricks that allow to write the variadic composition operator. I am not familiar with that. Do you have a reference? Is that the best way to do it? (Is that a way to do it at all?) You might find these articles somewhat related... Functions with the variable number of (variously typed) arguments http://okmij.org/ftp/Haskell/types.html#polyvar-fn Deepest functor [was: fmap for lists of lists of lists of ...] http://okmij.org/ftp/Haskell/deepest-functor.lhs ...That first article is the strangest. I couldn't reconcile the fact that if our type signature specifies two arguments, we can pattern match on three arguments in the function definition. Compare the number of arguments in the first and second instances... class BuildList a r | r- a where build' :: [a] - a - r instance BuildList a [a] where build' l x = reverse$ x:l instance BuildList a r = BuildList a (a-r) where build' l x y = build'(x:l) y ...if you try something like... foo :: [a] - a - r foo l x y = undefined ...you'll get an error message like... The equation(s) for `foo' have three arguments, but its type `[a] - a - r' has only two YMMV, Greg Buchholz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] A type class puzzle
Rearranging... Nicolas Frisby wrote: On 10/31/06, Greg Buchholz [EMAIL PROTECTED] wrote: ...That first article is the strangest. I couldn't reconcile the fact that if our type signature specifies two arguments, we can pattern match on three arguments in the function definition. Compare the number of arguments in the first and second instances... See Connor McBride's Faking It: Simulating Dependent Types in Haskell http://citeseer.ist.psu.edu/mcbride01faking.html It might help; your example makes me think of the nthFirst function. If it's different, I'md wager the polyvariadic stuff and nthFirst can be reconciled on some level. Does that explain how, why, or when you can use more arguments than you are allowed to use? Or is it just another example of using more arguments than you are allowed to use? Is this a Haskell 98 thing, or is it related to MPTCs, or fun deps, or something else? Greg Buchholz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
Greg Buchholz wrote: ...That first article is the strangest. I couldn't reconcile the fact that if our type signature specifies two arguments, we can pattern match on three arguments in the function definition. Compare the number of arguments in the first and second instances... class BuildList a r | r- a where build' :: [a] - a - r instance BuildList a [a] where build' l x = reverse$ x:l instance BuildList a r = BuildList a (a-r) where build' l x y = build'(x:l) y I'm not sure I'm getting your point, but this is just because in the second instance, the second parameter of BuildList is 'a - r', so the specific type of 'build\'' is '[a] - a - (a - r)' which is just '[a] - a - a - r' (currying at work). Regards, Arie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: Re: [Haskell-cafe] A type class puzzle
Does that explain how, why, or when you can use more arguments than you are allowed to use? Or is it just another example of using more arguments than you are allowed to use? Is this a Haskell 98 thing, or is it related to MPTCs, or fun deps, or something else? I don't understand you can use more arguments than you are allowed to use. I doubt the work in Faking It is Haskell 98 because I'm pretty sure it uses MPTCs, fundeps and undecidable instances. I think it does a bit to introduce these concepts too if you're unfamiliar with them. Nick ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
On Tue, Oct 31, 2006 at 03:12:53PM +0200, Yitzchak Gale wrote: But I would rather not be forced to write things like replace (I 0 $ I 2 $ I 3 $ ()) in my code. My first attempt was very similar to yours, except I used replace (0, (2, (3, ( instead of your Index type. I started with it too, but I had to disambiguate the numeric type, eg. by saying: (0 :: Int, (2 :: Int, (3 :: Int, (. Hmmm... I could solve it without creating a new type. I don't like my solution, either. So I guess I would define a full solution as something nice enough to be used in practice. Let's be more concrete - it has to be nice enough that most people who need, say, replace2 or replace3, in real life, would actually use your function instead of writing it out by hand. I think that in pracice I would still prefer the version with indices gathered in a single argument - it is a bit more uniform, more first-class, etc. Hmmm... Haskell's Arrays are a good example. Maybe others would disagree, but so far, I personally do not use either your solution or my solution. I write it out by hand. Well, I didn't yet have a need for such a function... If you insist that each index should be given as a separate function argument, it may be possible to achieve it using the tricks that allow to write the variadic composition operator. I am not familiar with that. Do you have a reference? I think it's in one of Oleg's articles mentioned in other replies. Is that the best way to do it? (Is that a way to do it at all?) I am not sure. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
Arie Peterson wrote: ] I'm not sure I'm getting your point, but this is just because in the ] second instance, the second parameter of BuildList is 'a - r', so the ] specific type of 'build\'' is '[a] - a - (a - r)' which is just '[a] - ] a - a - r' (currying at work). I guess it just looks really strange to my eyes. For example, foo and bar are legal, but baz isn't. That's what I was thinking of the situation, but I guess the type classes iron out the differences. foo :: Int - Int - Int - Int foo 0 = (+) bar :: Int - Int - Int - Int bar 1 x = succ baz :: Int - Int - Int - Int baz 0 = (+) baz 1 x = succ Greg Buchholz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
Greg Buchholz wrote: I guess it just looks really strange to my eyes. For example, foo and bar are legal, but baz isn't. That's what I was thinking of the situation, but I guess the type classes iron out the differences. foo :: Int - Int - Int - Int foo 0 = (+) bar :: Int - Int - Int - Int bar 1 x = succ baz :: Int - Int - Int - Int baz 0 = (+) baz 1 x = succ This could be understood as a weakness in the de-sugaring of pattern-matching, because bong :: Int - Int - Int - Int bong 0 = (+) bong 1 = \x - succ is just fine. Jacques ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
