[Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Hi ^_^, Let's say we have the following data type and functions: data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read) map f (:↺:) = (:↺:) map f (a :↓: t) = f a :↓: map f t map f (h :↙↘: (l,r)) = map f h :↙↘: (map f l, map f r) filter p (:↺:) = (:↺:) filter p (a :↓: t) | p a = filter p t | otherwise = a :↓: filter p t filter p (h :↙↘: (l,r)) = filter p h :↙↘: (filter p l, filter p r) is it possible to automatically derive map and filter? data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read, Map, Filter) If not, do you think it might be nice to have something like this in the future? Best Regards, Cetin Sert ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Well, it's certainly not possible for filter, at least, not without additional hints to the compiler. For example, consider this type: data Weird a = A | B a (Weird a) (Weird a) filter p A = A filter p (B x w1 w2) | p x = B x (filter p w1) (filter p w2) | otherwise = ? On 5 Jun 2008, at 12:03, Cetin Sert wrote: Hi ^_^, Let's say we have the following data type and functions: data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read) map f (:↺:) = (:↺:) map f (a :↓: t) = f a :↓: map f t map f (h :↙↘: (l,r)) = map f h :↙↘: (map f l, map f r) filter p (:↺:) = (:↺:) filter p (a :↓: t) | p a = filter p t | otherwise = a :↓: filter p t filter p (h :↙↘: (l,r)) = filter p h :↙↘: (filter p l, filter p r) is it possible to automatically derive map and filter? data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read, Map, Filter) If not, do you think it might be nice to have something like this in the future? Best Regards, Cetin Sert ___ 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: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Even deriving an instance of Functor seems rather implausable, what should it do for data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b) Should fmap's function argument operate on 'a's, 'b's, or both? Bob On 5 Jun 2008, at 10:28, Miguel Mitrofanov wrote: Well, it's certainly not possible for filter, at least, not without additional hints to the compiler. For example, consider this type: data Weird a = A | B a (Weird a) (Weird a) filter p A = A filter p (B x w1 w2) | p x = B x (filter p w1) (filter p w2) | otherwise = ? On 5 Jun 2008, at 12:03, Cetin Sert wrote: Hi ^_^, Let's say we have the following data type and functions: data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read) map f (:↺:) = (:↺:) map f (a :↓: t) = f a :↓: map f t map f (h :↙↘: (l,r)) = map f h :↙↘: (map f l, map f r) filter p (:↺:) = (:↺:) filter p (a :↓: t) | p a = filter p t | otherwise = a :↓: filter p t filter p (h :↙↘: (l,r)) = filter p h :↙↘: (filter p l, filter p r) is it possible to automatically derive map and filter? data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read, Map, Filter) If not, do you think it might be nice to have something like this in the future? Best Regards, Cetin Sert ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Thomas Davie wrote: Even deriving an instance of Functor seems rather implausable, what should it do for data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b) Should fmap's function argument operate on 'a's, 'b's, or both? But for many datatypes it is quite natural. Just google for theory of containers. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
It can be even worse: data X a b = X (X b a - b) Here (X a) is certainly a functor, but the implementation must also act on a contravariantly: mapX :: (a - a') - X a' b - X a b mapX f (X h) = X $ h . fmap f instance Functor (X a) where fmap f (X h) = X $ f . h . mapX f On 5 Jun 2008, at 12:39, Thomas Davie wrote: Even deriving an instance of Functor seems rather implausable, what should it do for data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b) Should fmap's function argument operate on 'a's, 'b's, or both? Bob On 5 Jun 2008, at 10:28, Miguel Mitrofanov wrote: Well, it's certainly not possible for filter, at least, not without additional hints to the compiler. For example, consider this type: data Weird a = A | B a (Weird a) (Weird a) filter p A = A filter p (B x w1 w2) | p x = B x (filter p w1) (filter p w2) | otherwise = ? On 5 Jun 2008, at 12:03, Cetin Sert wrote: Hi ^_^, Let's say we have the following data type and functions: data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read) map f (:↺:) = (:↺:) map f (a :↓: t) = f a :↓: map f t map f (h :↙↘: (l,r)) = map f h :↙↘: (map f l, map f r) filter p (:↺:) = (:↺:) filter p (a :↓: t) | p a = filter p t | otherwise = a :↓: filter p t filter p (h :↙↘: (l,r)) = filter p h :↙↘: (filter p l, filter p r) is it possible to automatically derive map and filter? data Tab a = (:↺:) | a :↓: Tab a | Tab a :↙↘: (Tab a,Tab a) deriving (Eq, Show, Read, Map, Filter) If not, do you think it might be nice to have something like this in the future? Best Regards, Cetin Sert ___ 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 ___ 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: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
On Thu, Jun 05, 2008 at 10:39:16AM +0200, Thomas Davie wrote: Even deriving an instance of Functor seems rather implausable, what should it do for data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b) Should fmap's function argument operate on 'a's, 'b's, or both? Generic Haskell can do all that. Read Ralf Hinze's Generic Programs and Proofs for the theory: http://www.informatik.uni-bonn.de/~ralf/publications/habilitation.pdf Edsko ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
On 5 Jun 2008, at 1:39 AM, Thomas Davie wrote: Even deriving an instance of Functor seems rather implausable, what should it do for data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b) Should fmap's function argument operate on 'a's, 'b's, or both? class Functor (f :: * - *) where ... so, 'b's. jcc PS Why isn't Functor derivable? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Hi PS Why isn't Functor derivable? Derive can do it: http://www.cs.york.ac.uk/~ndm/derive I believe that Twan (the author of Functor deriving in Derive) is trying to get this suggested for Haskell' as a proper deriving. As for the original question, Uniplate will certainly do map, and will probably help with filter - as the definition of Filter is not obvious given the type. And you can have automatic deriving with Uniplate (see PlateData in the paper or the module structure) http://www.cs.york.ac.uk/~ndm/uniplate Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] automatically deriving Map and Filter on datatypes etc.
Hi
Statutory mathematics warning: lots.
On 5 Jun 2008, at 15:40, Jonathan Cast wrote:
On 5 Jun 2008, at 1:39 AM, Thomas Davie wrote:
Even deriving an instance of Functor seems rather implausable,
what should it do for
data Wierd a b = Nil | A a (Wierd a b) | B b (Wierd a b)
Should fmap's function argument operate on 'a's, 'b's, or both?
class Functor (f :: * - *) where ...
so, 'b's.
While application remains injective, that seems
appropriate. But wouldn't we want more, eg,
that Wierd is a bifunctor (and, moreover,
bitraversable, bihalfzippable,...)?
Of course, there's a whole ghastly family of
these things for type constructors of varying
arities, together with stuff like the fixpoint
of a bifunctor is a functor.
jcc
PS Why isn't Functor derivable?
It would be very handy, but it's the tip of the
iceberg. Being an Ulsterman, I get nervous
about engineering for machinery-iceberg collisions.
Perhaps it's worth looking for a systematic approach
to the more general situation (not necessarily kind
polymorphism; a systematic library treatment of
n-functors for n in {0,..,pickamax} would be a good
start).
An alterative, perhaps, is to replace arity by
indexing. This may get hairy. Untested stuff...
data Rewired f n where
Nil :: Rewired f Zero
A :: f Zero - Rewired f Zero - Rewired f Zero
B :: f One - Rewired f Zero - Rewired f Zero
data Pick a b n where -- clearly a bit specific
PickA :: a - Pick a b Zero
PickB :: b - Pick a b One
type Wierd a b = Rewired (Pick a b) Zero
Here Rewired :: (* - *) - (* - *), but
(* - *) means *-indexed type not container.
I'd rather be more precise and work with
(i - *) - (o - *), but we have to take
i = o = * for now. The idea is to transform
a bunch of input datatypes indexed by i
to a bunch of output datatypes indexed by o.
In this example, we collect Bob's two element
types into a single GADT which specializes
differently at two distinct input indices.
There's no variation in the output index, so
I just made them all Zero. But here's another
old friend
data Vec f n where
Nil :: Vec f Zero
Cons :: f Zero - Vec f n - Vec f (Suc n)
which has no input variation, but uses the
output index to specify length.
Anyhow, the point is that for these indexed
structures, you get to define much of the
generic kit once and for all, and you get
one obvious notion of map.
type f :-: g = forall x. f x - g x
class IxMap c where
ixMap :: (f :-: g) - (c f :-: c g)
Painless! Well, er, probably not. (Masochists
may choose to generalize this notion by
relaxing the index-preservation requirement
to some sort of index-simulation, thus
heading for Hancock's notion of container
driver. I digress.)
Anyhow, it would be nice if kit developed
once for indexed structures could be lifted
automatically to the indexed encoding of
the more specific types you'd actually
like to work with. Maybe that's a thing to
be deriving.
{--
Exercises for masochists (especially myself):
(1) Show that simply-typed lambda-terms
have IxMap structure (aka type-safe renaming)
over notions of typed variable, just as untyped
(de Bruijn) lambda-terms are an instance of
Functor. It may help to think systematically
about notions of typed variable.
(2) Define an indexed container transformer
IxFix ::
((* - *) - (* - *)) - ((* - *) - (* - *))
in such a way that
instance IxMap c = IxMap (IxFix c)
and present Vec, etc, with IxFix as the only
source of recursive datatype definition. Hint,
the more refined kind should be seen as
(((i + o) - *) - (o - *))
-
((i - *) - (o - *))
so that c has places both for i-indexed inputs
and for o-indexed substructures.
(3) Grok and adapt the rest of Jeremy Gibbons'
origami apparatus.
--}
Meanwhile, if you want to derive filtering,
think about what one-hole contexts for elements
need to look like, especially if you might want
to throw the element away. Fans of bifunctor
fixpoints and multivariate partial differentiation
may be amused to note that
[x] = mu y. 1 + xy
(d/dx) (1 + xy) = y
and that Cetin's
Tab x = mu y. 1 + xy + y^3
(d/dx) (1 + xy + y^3) = y
so perhaps a pattern is emerging...
It's been an interesting day: thanks to all for
the food for thought. It's clear that Haskell
(with recent extensions) can now express very
powerful abstractions such as indexed
container, but not in a way which sits very
comfortably with normal usage. I think that's
a serious concern.
Cheers
Conor
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
