Traversable Functor Data,or: X marks the spot
Dear Generics;-) this is a repost from cvs-libraries of an experiment which you might find of interest, and on which I'd welcome feedback. One impact being that SYB can implement your GMap test (on which it currently defaults), among other things (see message 1 below, the technique probably applies to Uniplate as well?). One issue being that Data instances for non-algebraic types that default to doing nothing render this technique unsafe (see message 2 below). Btw, the announcement of the unified generics library project was so long ago that I had forgotten about it and about this list (thanks to Simon PJ for reminding me). My interest in this is partially from my past with HaRe, partially from wanting generic traversal support over GHC AST types, so I'm more interested in generic traversal/analysis style libraries. Claus --------- message 1 The issue at hand: can we use Data/Typeable to do what Functor and Traversible do so easily, namely type-changing maps? Or should there be support for deriving all of Data/Typeable/Functor/Traversible over GHC's AST? A drastically simplified example from David's Haddock 2 code (Haddock.Interface.Rename) needs to do a kind of mapM renameDoc :: Monad m => HsDoc Name -> m (HsDoc DocName) which is straightforward with Traversible, but that is not derivable yet (David has been working on that, though), while the usual basis of SYB, Data/Typeable, is derivable, but all SYB transformations are based on gfoldl, the type of which does not permit type-changing maps: gfoldl :: (Data a) =>(forall a1 b. (Data a1) => c (a1 -> b) -> a1 -> c b) -> (forall g. g -> c g) -> a-> c a One could probably go from heterogeneous Data types to a homogeneously typed tree representation, do the map there, then transform back, but that would require additional overhead and a type coercion for the backtransform. Also, it seems a pity that the derived code for gfoldl can handle such maps - it is just gfoldl's type that gets in the way (and trying to generalize that type is a whole different kind of headache..). While boilerplate scrappers around the globe eagerly await the release of "Generalizing the type of gfold, or: to braindamage and beyond" (author: unknown; release date: unknown; release: unlikely;-) I thought I'd have a go at the smaller problem of finding a way to bypass gfoldl's type systematically in order to use its derivable code for things like fmap and traverse. This message summarizes how far I've got so far, and asks for comments (does this do what it should? is it safe? assuming it can be cleaned up to do what it should in a safe way, does this mean that deriving Data/ Typeable for GHCs AST types will be sufficient, or should we still have Traversible as well? etc.). First, here is an implementation of renameDoc in terms of gfoldl and unsafeCoerce (slightly cleaned up version of what I sent in the other thread earlier): data Name = Name String deriving (Show,Data,Typeable) data DocName = DocName String deriving (Show,Data,Typeable) renameDoc :: Monad m => HsDoc Name -> m (HsDoc DocName) renameDoc (DocIdentifier ids) = mapM (\(Name n)->return (DocName n)) ids >>= return . DocIdentifier renameDoc hsDoc = n2d (gfoldl k return hsDoc) where k c x = ap c (mkM (d2n . renameDoc) x) n2d :: Monad m => m (HsDoc Name) -> m (HsDoc DocName) n2d = unsafeCoerce d2n :: Monad m => m (HsDoc DocName) -> m (HsDoc Name) d2n = unsafeCoerce 'DocIdentifier :: [id] -> HsDoc id' is the only constructor in HsDoc that involves the parameter type 'id', so renameDoc either does the parameter type conversion or -for other constructors- recurses into the subexpressions, using gfoldl to build a monadic map. The important insight here is that gfoldl's code can handle the task, we just pretend that our map is type-preserving to conform to gfoldl's restrictive type, by coercing the result types (inside gfoldl, we pretend that renameDoc returns a (HsDoc Name), which outside gfoldl, we coerce back to (HsDoc DocName)). Assuming that noone looks at the return types inside gfoldl (at least, not in a way that would be affected by this change in type - SYB does support adhoc overloading, after all, as in mkM here), this seems to work: testDoc = DocAppend (DocParagraph (DocAppend (DocIdentifier [Name "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [Name "don't",Name "go",Name "anywhere"])) *Main> renameDoc testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [DocName "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [DocName "don't",DocName "go",DocName "anywhere"])) But can we generalize this, and what about those coercions? Can we -ideally- define something like fmap and traverse in terms of gfoldl, and hide the uglyness in their implementations? Well, I'll spare you (and me;-) the details of my struggle with the type system, and just show the results, with some comments. First, the simpler fmap: -- "X marks the spots";-) X should be private data X = X deriving (Data,Typeable) fmap' :: (Data (f X)) => (a -> b) -> f a -> f b fmap' f x = markTheSpots (rec (wrap f)) x where markTheSpots :: (f X -> f X) -> (f a -> f b) markTheSpots f = unsafeCoerce . f . unsafeCoerce rec :: (Data a) => (X -> X) -> a -> a rec f x = (gmapT (rec f) `extT` f) x wrap :: (a -> b) -> (X -> X) wrap f = unsafeCoerce . f . unsafeCoerce Surprisingly simple for something that seemed impossible at first, isn't it?-) Since we're already committed (for this experiment, at least) to some type fiddling, we can make more constructive use of unsafeCoerce, for two purposes: 1. We wrap the function parameter f, to make it look like a type-preserving function, on some private type X. 2. We mark the occurrences of the type constructor f's parameter type, by coercing 'f a' to 'f X' and 'f X' to 'f b'. Then, we simply use SYB to apply f, when its type matches the parameter, or to recurse into the subexpressions using gmapT, otherwise. If X is private, f will only be applied to the "functor parameter" _positions_ in 'f a', not to other "functor parameter" _type_ occurrences in 'f a': *Main> fmap' not $ (True,True) (True,False) *Main> fmap' not $ [True,True] [False,False] *Main> fmap' (\(Name s)->(DocName s)) testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [DocName "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [DocName "don't",DocName "go",DocName "anywhere"])) Note how we use one kind of recursion where a manual implementation of fmap would use two: handling subexpressions (which we'd usually do by pattern matching and expression construction) and functor type recursion. Ecouraged by this success, we are ready to tackle the slightly more tricky traverse, using the same techniques: mark the spot, wrap the worker, one kind of recursion. Only this time, we need to take care of the applicative plumbing as well, so it's gfoldl instead of gmapT, and some more complex types. We need the usual SYB type extension support, but for Applicative, not Monad (SYB was defined before Applicative existed, it seems..): -- type extension over Applicative f mkF :: forall f a b . (Applicative f,Typeable a,Typeable b) => (b -> f b) -> a -> f a mkF f x = case gcast (F f) of { Just (F f) -> f x; Nothing -> pure x } extF :: forall t f a b . (Typeable a,Typeable b) => (a -> f a) -> (b -> f b) -> (a -> f a) (f `extF` fspec) x = case gcast (F fspec) of { Just (F fspec) -> fspec x; Nothing -> f x } newtype F f x = F { unF :: x -> f x } And here we go: traverse' :: forall f t a b . (Applicative f,Typeable1 f, Typeable1 t,Data (t X), Typeable a) => (a -> f b) -> t a -> f (t b) traverse' f x = markTheSpots (rec (wrap f)) x where markTheSpots :: forall a b . (t X -> f (t X)) -> (t a -> f (t b)) markTheSpots f = unsafeCoerce . f . unsafeCoerce wrap :: forall a b . (a -> f b) -> (X -> f X) wrap f = unsafeCoerce . f . unsafeCoerce rec :: forall x . Data x => (X -> f X) -> x -> f x rec f x = (gfoldl (k f) z `extF` f) x k :: forall a b . Data a => (X -> f X) -> f (a -> b) -> a -> f b k f c x = c <*> (mkF (rec f :: Data a => a -> f a) `extF` f) x z c = pure c This does seem to do the right thing, so I don't seem to be completely on the wrong track: *Main> traverse' (pure . not) (True,True) (True,False) *Main> traverse' (pure . not) [True,True] [False,False] *Main> traverse' print testDoc Name "well-typed" Name "don't" Name "go" Name "anywhere" DocAppend (DocParagraph (DocAppend (DocIdentifier [()]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [(),(),()])) *Main> traverse' (pure) testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [Name "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [Name "don't",Name "go",Name "anywhere"])) *Main> traverse' (pure . (\(Name s)->DocName s)) testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [DocName "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [DocName "don't",DocName "go",DocName "anywhere"])) but I'm too battered from trying to coerce gfoldl to analyze this properly at the moment, so I'm sending this in the hope of (a) not having to look at gfoldl's type for a while !-) and (b) getting some feedback (is this useful? does the extra overhead matter?..), caveats (cyclic programs, nested traversals, escaping Xs, ..?), etc. Over to you, Claus PS. the "X marks the spot" trick reminds me of the popular medicine topic: delivery system plus targeted activation (SYB plus unsafeCoerce). ------------- message 2
fmap' :: (Data (f X)) => (a -> b) -> f a -> f b fmap' f x = markTheSpots (rec (wrap f)) x where markTheSpots :: (f X -> f X) -> (f a -> f b) markTheSpots f = unsafeCoerce . f . unsafeCoerce rec :: (Data a) => (X -> X) -> a -> a rec f x = (gmapT (rec f) `extT` f) x wrap :: (a -> b) -> (X -> X) wrap f = unsafeCoerce . f . unsafeCoerce .. 1. We wrap the function parameter f, to make it look like a type-preserving function, on some private type X.
2. We mark the occurrences of the type constructor f's parameter type, by coercing 'f a' to 'f X' and 'f X' to 'f b'.
Then, we simply use SYB to apply f, when its type matches the parameter, or to recurse into the subexpressions using gmapT, otherwise. If X is private, f will only be applied to the "functor parameter" _positions_ in 'f a', not to other "functor parameter" _type_ occurrences in 'f a'
..but f might not be applied at all, which leads to the first issue with this technique: I was surprised to see Data instances for (a->b) and IO a, since for such non-algebraic types, there isn't anything to gfoldl or gmap over. And those instances do indeed seem to offer very little functionality (not to mention the runtime errors..). For fmap'/traverse', this means that f will not be applied, and so it is not a good idea to coerce the types as if f had been applied (because the hidden parameter could be exposed after traversal, with changed type and unchanged representation!).. So we need to restrict the types of fmap'/traverse'. Which leads to two questions: - what is the rationale for having these non-functional Data instances? If one is to have 'instance Data (a->b)', is there a way to make it more functional? - how can we capture algebraic types in a type (class)? I thought that Data would do just that, being designed to gfoldl over concrete data constructors, but apparently not. And I don't really want to have a separate list of all the types for which Data works, or of all the types for which Data doesn't quite work. Claus ps. What is the right list for this topic?
Hi Claus!
We have a deadline coming soon, so this is only a brief comment about your
GMap implementation.
I played a bit with your fmap' function to see whether I could find an
obvious problem with the implementation. For instance, I used this datatype:
data Tricky a = Tricky a Char deriving (Data,Typeable)
and tried to transform a value of type "Tricky Char" to "Tricky Bool". I
wanted to see whether the second argument of Tricky would be (incorrectly)
transformed to Bool. But it turned out that fmap' behaved as expected. So I
think that SYB can pass the GMap test.
On the other hand, I think that using unsafeCoerce as a way to define
generic functions is inelegant and probably bad practice due to possible
runtime failures. However, I must admit that I was surprised when I saw your
trick :).
Probably we'll get back to you around next week. Meanwhile, you may find
useful to look at the paper we wrote on comparing generic programming
libraries[1]. In particular, you can look at caveats that apply to SYB.
Cheers,
Alexey
[1]
http://www.cs.uu.nl/wiki/bin/view/Alexey/ComparingLibrariesForGenericProgram...
On Tue, Jun 24, 2008 at 8:45 PM, Claus Reinke
Dear Generics;-)
this is a repost from cvs-libraries of an experiment which you might find of interest, and on which I'd welcome feedback. One impact being that SYB can implement your GMap test (on which it currently defaults), among other things (see message 1 below, the technique probably applies to Uniplate as well?). One issue being that Data instances for non-algebraic types that default to doing nothing render this technique unsafe (see message 2 below).
Btw, the announcement of the unified generics library project was so long ago that I had forgotten about it and about this list (thanks to Simon PJ for reminding me). My interest in this is partially from my past with HaRe, partially from wanting generic traversal support over GHC AST types, so I'm more interested in generic traversal/analysis style libraries.
Claus
--------- message 1
The issue at hand: can we use Data/Typeable to do what Functor and Traversible do so easily, namely type-changing maps? Or should there be support for deriving all of Data/Typeable/Functor/Traversible over GHC's AST?
A drastically simplified example from David's Haddock 2 code (Haddock.Interface.Rename) needs to do a kind of mapM
renameDoc :: Monad m => HsDoc Name -> m (HsDoc DocName)
which is straightforward with Traversible, but that is not derivable yet (David has been working on that, though), while the usual basis of SYB, Data/Typeable, is derivable, but all SYB transformations are based on gfoldl, the type of which does not permit type-changing maps:
gfoldl :: (Data a) =>(forall a1 b. (Data a1) => c (a1 -> b) -> a1 -> c b) -> (forall g. g -> c g) -> a-> c a
One could probably go from heterogeneous Data types to a homogeneously typed tree representation, do the map there, then transform back, but that would require additional overhead and a type coercion for the backtransform. Also, it seems a pity that the derived code for gfoldl can handle such maps - it is just gfoldl's type that gets in the way (and trying to generalize that type is a whole different kind of headache..).
While boilerplate scrappers around the globe eagerly await the release of "Generalizing the type of gfold, or: to braindamage and beyond" (author: unknown; release date: unknown; release: unlikely;-)
I thought I'd have a go at the smaller problem of finding a way to bypass gfoldl's type systematically in order to use its derivable code for things like fmap and traverse. This message summarizes how far I've got so far, and asks for comments (does this do what it should? is it safe? assuming it can be cleaned up to do what it should in a safe way, does this mean that deriving Data/ Typeable for GHCs AST types will be sufficient, or should we still have Traversible as well? etc.).
First, here is an implementation of renameDoc in terms of gfoldl and unsafeCoerce (slightly cleaned up version of what I sent in the other thread earlier):
data Name = Name String deriving (Show,Data,Typeable) data DocName = DocName String deriving (Show,Data,Typeable)
renameDoc :: Monad m => HsDoc Name -> m (HsDoc DocName) renameDoc (DocIdentifier ids) = mapM (\(Name n)->return (DocName n)) ids >>= return . DocIdentifier renameDoc hsDoc = n2d (gfoldl k return hsDoc) where k c x = ap c (mkM (d2n . renameDoc) x)
n2d :: Monad m => m (HsDoc Name) -> m (HsDoc DocName) n2d = unsafeCoerce d2n :: Monad m => m (HsDoc DocName) -> m (HsDoc Name) d2n = unsafeCoerce
'DocIdentifier :: [id] -> HsDoc id' is the only constructor in HsDoc that involves the parameter type 'id', so renameDoc either does the parameter type conversion or -for other constructors- recurses into the subexpressions, using gfoldl to build a monadic map. The important insight here is that gfoldl's code can handle the task, we just pretend that our map is type-preserving to conform to gfoldl's restrictive type, by coercing the result types (inside gfoldl, we pretend that renameDoc returns a (HsDoc Name), which outside gfoldl, we coerce back to (HsDoc DocName)).
Assuming that noone looks at the return types inside gfoldl (at least, not in a way that would be affected by this change in type - SYB does support adhoc overloading, after all, as in mkM here), this seems to work:
testDoc = DocAppend (DocParagraph (DocAppend (DocIdentifier [Name "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [Name "don't",Name "go",Name "anywhere"]))
*Main> renameDoc testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [DocName "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [DocName "don't",DocName "go",DocName "anywhere"]))
But can we generalize this, and what about those coercions? Can we -ideally- define something like fmap and traverse in terms of gfoldl, and hide the uglyness in their implementations?
Well, I'll spare you (and me;-) the details of my struggle with the type system, and just show the results, with some comments. First, the simpler fmap:
-- "X marks the spots";-) X should be private data X = X deriving (Data,Typeable)
fmap' :: (Data (f X)) => (a -> b) -> f a -> f b fmap' f x = markTheSpots (rec (wrap f)) x where markTheSpots :: (f X -> f X) -> (f a -> f b) markTheSpots f = unsafeCoerce . f . unsafeCoerce rec :: (Data a) => (X -> X) -> a -> a rec f x = (gmapT (rec f) `extT` f) x wrap :: (a -> b) -> (X -> X) wrap f = unsafeCoerce . f . unsafeCoerce
Surprisingly simple for something that seemed impossible at first, isn't it?-) Since we're already committed (for this experiment, at least) to some type fiddling, we can make more constructive use of unsafeCoerce, for two purposes:
1. We wrap the function parameter f, to make it look like a type-preserving function, on some private type X.
2. We mark the occurrences of the type constructor f's parameter type, by coercing 'f a' to 'f X' and 'f X' to 'f b'.
Then, we simply use SYB to apply f, when its type matches the parameter, or to recurse into the subexpressions using gmapT, otherwise. If X is private, f will only be applied to the "functor parameter" _positions_ in 'f a', not to other "functor parameter" _type_ occurrences in 'f a':
*Main> fmap' not $ (True,True) (True,False) *Main> fmap' not $ [True,True] [False,False]
*Main> fmap' (\(Name s)->(DocName s)) testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [DocName "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [DocName "don't",DocName "go",DocName "anywhere"]))
Note how we use one kind of recursion where a manual implementation of fmap would use two: handling subexpressions (which we'd usually do by pattern matching and expression construction) and functor type recursion.
Ecouraged by this success, we are ready to tackle the slightly more tricky traverse, using the same techniques: mark the spot, wrap the worker, one kind of recursion. Only this time, we need to take care of the applicative plumbing as well, so it's gfoldl instead of gmapT, and some more complex types.
We need the usual SYB type extension support, but for Applicative, not Monad (SYB was defined before Applicative existed, it seems..):
-- type extension over Applicative f mkF :: forall f a b . (Applicative f,Typeable a,Typeable b) => (b -> f b) -> a -> f a mkF f x = case gcast (F f) of { Just (F f) -> f x; Nothing -> pure x }
extF :: forall t f a b . (Typeable a,Typeable b) => (a -> f a) -> (b -> f b) -> (a -> f a) (f `extF` fspec) x = case gcast (F fspec) of { Just (F fspec) -> fspec x; Nothing -> f x }
newtype F f x = F { unF :: x -> f x }
And here we go:
traverse' :: forall f t a b . (Applicative f,Typeable1 f, Typeable1 t,Data (t X), Typeable a) => (a -> f b) -> t a -> f (t b) traverse' f x = markTheSpots (rec (wrap f)) x where markTheSpots :: forall a b . (t X -> f (t X)) -> (t a -> f (t b)) markTheSpots f = unsafeCoerce . f . unsafeCoerce wrap :: forall a b . (a -> f b) -> (X -> f X) wrap f = unsafeCoerce . f . unsafeCoerce
rec :: forall x . Data x => (X -> f X) -> x -> f x rec f x = (gfoldl (k f) z `extF` f) x k :: forall a b . Data a => (X -> f X) -> f (a -> b) -> a -> f b k f c x = c <*> (mkF (rec f :: Data a => a -> f a) `extF` f) x z c = pure c
This does seem to do the right thing, so I don't seem to be completely on the wrong track:
*Main> traverse' (pure . not) (True,True) (True,False)
*Main> traverse' (pure . not) [True,True] [False,False]
*Main> traverse' print testDoc Name "well-typed" Name "don't" Name "go" Name "anywhere" DocAppend (DocParagraph (DocAppend (DocIdentifier [()]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [(),(),()]))
*Main> traverse' (pure) testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [Name "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [Name "don't",Name "go",Name "anywhere"]))
*Main> traverse' (pure . (\(Name s)->DocName s)) testDoc DocAppend (DocParagraph (DocAppend (DocIdentifier [DocName "well-typed"]) DocEmpty)) (DocAppend (DocString "programs") (DocIdentifier [DocName "don't",DocName "go",DocName "anywhere"]))
but I'm too battered from trying to coerce gfoldl to analyze this properly at the moment, so I'm sending this in the hope of (a) not having to look at gfoldl's type for a while !-) and (b) getting some feedback (is this useful? does the extra overhead matter?..), caveats (cyclic programs, nested traversals, escaping Xs, ..?), etc.
Over to you, Claus
PS. the "X marks the spot" trick reminds me of the popular medicine topic: delivery system plus targeted activation (SYB plus unsafeCoerce).
------------- message 2
fmap' :: (Data (f X)) => (a -> b) -> f a -> f b
fmap' f x = markTheSpots (rec (wrap f)) x where markTheSpots :: (f X -> f X) -> (f a -> f b) markTheSpots f = unsafeCoerce . f . unsafeCoerce rec :: (Data a) => (X -> X) -> a -> a rec f x = (gmapT (rec f) `extT` f) x wrap :: (a -> b) -> (X -> X) wrap f = unsafeCoerce . f . unsafeCoerce
..
1. We wrap the function parameter f, to make it look like a type-preserving function, on some private type X.
2. We mark the occurrences of the type constructor f's parameter type, by coercing 'f a' to 'f X' and 'f X' to 'f b'.
Then, we simply use SYB to apply f, when its type matches the parameter, or to recurse into the subexpressions using gmapT, otherwise. If X is private, f will only be applied to the "functor parameter" _positions_ in 'f a', not to other "functor parameter" _type_ occurrences in 'f a'
..but f might not be applied at all, which leads to the first issue with this technique:
I was surprised to see Data instances for (a->b) and IO a, since for such non-algebraic types, there isn't anything to gfoldl or gmap over. And those instances do indeed seem to offer very little functionality (not to mention the runtime errors..). For fmap'/traverse', this means that f will not be applied, and so it is not a good idea to coerce the types as if f had been applied (because the hidden parameter could be exposed after traversal, with changed type and unchanged representation!).. So we need to restrict the types of fmap'/traverse'. Which leads to two questions:
- what is the rationale for having these non-functional Data instances?
If one is to have 'instance Data (a->b)', is there a way to make it more functional?
- how can we capture algebraic types in a type (class)?
I thought that Data would do just that, being designed to gfoldl over concrete data constructors, but apparently not. And I don't really want to have a separate list of all the types for which Data works, or of all the types for which Data doesn't quite work.
Claus
ps. What is the right list for this topic?
_______________________________________________ Generics mailing list Generics@haskell.org http://www.haskell.org/mailman/listinfo/generics
Hi Alexey,
We have a deadline coming soon, so this is only a brief comment about your GMap implementation.
Thanks, the silence had me worried! I'll wait till next week, then, meanwhile just a few comments on your comments;-)
wanted to see whether the second argument of Tricky would be (incorrectly) transformed to Bool. But it turned out that fmap' behaved as expected. So I
That's the idea - the wrapped function parameter will be delivered everywhere by the SYB framework, but will only be applied to the marked type. The marker type should play no other role.
On the other hand, I think that using unsafeCoerce as a way to define generic functions is inelegant and probably bad practice due to possible runtime failures. However, I must admit that I was surprised when I saw your trick :).
Haskell is full of odd corners (eg, the IO model is not backed up by a uniqueness type system, so is really unsafe under the abstraction, and neither the implementation nor the optimizer are verified by the type system; the Typeable stuff only works by convention for the instances; ..). Ideally, the language/type system will be extended to be able to express all the capabilities of gfoldl's code in gfoldl's type. But as long as that isn't the case, unsafeCoerce allows us to extend the type system, just as unsafePerformIO allows us to extend the evaluator. But since we are dealing in extensions, it is up to us to demonstrate that we haven't broken anything (well, me, in this case, but after staring at gfoldl's type and its implication for several days, I felt like calling for a little outside perspective:-). My assumption was roughly that 'everywhere f' would apply 'f' to all occurences typed 'a' provided that 'f' has 'a' generic special case for type 'a'. That assumption is violated by the Data instances for (a->b) and (IO a), so as long as those instances exist, it is easy to come up with counterexamples for fmap'. That is why I was asking for the rationale for those instances - if it was just convenience, they should be dropped, especially since SYB doesn't permit overloading to polymorpic types, so those default instances are not easily bypassed. Once that is sorted, the next issue is whether the private marker type can escape and be observed by other means. fmap' is constructed in such a way that neither 'f' nor the calling context see 'X', so as long as the generic scaffolding provided by 'Data' doesn't mess up, that should be fine. For things like traverse', other operators might be applied to things coerced to 'X', so that needs to be looked into and perhaps improved.
Probably we'll get back to you around next week. Meanwhile, you may find useful to look at the paper we wrote on comparing generic programming libraries[1]. In particular, you can look at caveats that apply to SYB.
Yep, I guess I'll have to look through some more of the generic papers on my reading heap:-) Btw, the overall idea behind my experiment is whether we can use 'Data/Typeable', which can be derived in GHC, to avoid the need for deriving support for other generic instances (such as Functor, Traversable). Again, a very pragmatic perspective (what can we do with the basis we have now, rather than: what better basis would be like to have?), but closely related to this list's aim of a unified generic programming framework. Btw, expanding SYB's invariant maps to variant ones raises the whole issue of co- vs contra-variance: if one really wants to fmap over types containing the parameter type in function types, one would need to handle both positive and negative occurrences, presumably by a pair of dual functions (a->b, b->a)? Looking forward to more feedback after that deadline. Thanks, Claus
Hey Claus! Sorry for the delay, just after the deadline I got into two more
deadlines so I was very busy with paper writing these last weeks!
On Fri, Jun 27, 2008 at 10:48 PM, Claus Reinke
wanted to see whether the second argument of Tricky would be (incorrectly)
transformed to Bool. But it turned out that fmap' behaved as expected. So I
That's the idea - the wrapped function parameter will be delivered everywhere by the SYB framework, but will only be applied to the marked type. The marker type should play no other role.
Yes, it looks like sort of defining a local type constant which should not be visible after the transformation.
On the other hand, I think that using unsafeCoerce as a way to define
generic functions is inelegant and probably bad practice due to possible runtime failures. However, I must admit that I was surprised when I saw your trick :).
Haskell is full of odd corners (eg, the IO model is not backed up by a uniqueness type system, so is really unsafe under the abstraction, and neither the implementation nor the optimizer are verified by the type system; the Typeable stuff only works by convention for the instances; ..).
Ideally, the language/type system will be extended to be able to express all the capabilities of gfoldl's code in gfoldl's type. But as long as that isn't the case, unsafeCoerce allows us to extend the type system, just as unsafePerformIO allows us to extend the evaluator. But since we are dealing in extensions, it is up to us to demonstrate that we haven't broken anything (well, me, in this case, but after staring at gfoldl's type and its implication for several days, I felt like calling for a little outside perspective:-).
As I said before, I don't consider this an elegant use of unsafeCoerce. The reason is that if you later want to generalize other functions over type constructors (for example, zipWith), you have to again deal with unsafeCoerce. It would already be a slight improvement if this trick can be encapsulated into a reusable combinator. If you want to make SYB support definitions that abstract over type constructors, you may want to have a look at "Scrap your Boilerplate Revolutions". Although, I don't immediately see a way to generalize gfoldl in order to encode the "lifted spine view".
My assumption was roughly that 'everywhere f' would apply 'f' to all occurences typed 'a' provided that 'f' has 'a' generic special case for type 'a'. That assumption is violated by the Data instances for (a->b) and (IO a), so as long as those instances exist, it is easy to come up with counterexamples for fmap'. That is why I was asking for the rationale for those instances - if it was just convenience, they should be dropped, especially since SYB doesn't permit overloading to polymorpic types, so those default instances are not easily bypassed.
Yes, I think I would also prefer those instances to reside in a separate module, so that you can choose not to import them.
Once that is sorted, the next issue is whether the private marker type can escape and be observed by other means. fmap' is constructed in such a way that neither 'f' nor the calling context see 'X', so as long as the generic scaffolding provided by 'Data' doesn't mess up, that should be fine.
Probably this is something you have to prove whenever you define a generic function in this style.
For things like traverse', other operators might be applied to things coerced to 'X', so that needs to be looked into and perhaps improved.
Probably we'll get back to you around next week. Meanwhile, you may find
useful to look at the paper we wrote on comparing generic programming libraries[1]. In particular, you can look at caveats that apply to SYB.
Yep, I guess I'll have to look through some more of the generic papers on my reading heap:-) Btw, the overall idea behind my experiment is whether we can use 'Data/Typeable', which can be derived in GHC, to avoid the need for deriving support for other generic instances (such as Functor, Traversable). Again, a very pragmatic perspective (what can we do with the basis we have now, rather than: what better basis would be like to have?), but closely related to this list's aim of a unified generic programming framework.
I think it's good to see how far the limits of SYB and other libraries can be pushed. But I would personally avoid using gmap as you proposed, until there is a cleaner way to do things or the corner cases are well understood.
Btw, expanding SYB's invariant maps to variant ones raises the whole issue of co- vs contra-variance: if one really wants to fmap over types containing the parameter type in function types, one would need to handle both positive and negative occurrences, presumably by a pair of dual functions (a->b, b->a)?
That gives rise to another type transforming map, namely bimap. You can look at its Generic Haskell definition at this URL: https://svn.cs.uu.nl:12443/repos/Generic-Haskell/trunk/Generic-Haskell/lib/G... Cheers, Alexey
Hello! It has occurred to me a year ago that the type-changing gMap is easily possible in SYB. The recent discussion has prompted me to implement that solution. I have committed a patch to http://darcs.haskell.org/generics/comparison/SYB1_2/GMap.lhs with the implementation. I hope this is OK: the previous version of that file was a stub saying that gMap is not supported. The function gMap has the expected type gmap :: (Data a, Data b, Data x, Data y) => (a -> b) -> x -> y There are no unsafe operations used; there is not a single occurrence of insafePerformIO and the ilk. Incidentally, Data.Generics could, in principle at least, be implemented using a safe cast. Of course gmap is not a total operation: one can't really expect (gmap id True) to produce a character. It seems that gunfold is not total anyway. Regarding the instance of Data for functions: SmashA does define (co-variant) traversal `under lambda'. For example, we can (gmap fromEnum) on a function and convert (Bool->Bool) to (Bool->Int). Please see testt3 in http://darcs.haskell.org/generics/comparison/SmashA/Syb4A.hs I do not claim to have any use for that transformation, but it was easy to implement... I will be out of town for two weeks and so unlikely to participate in further discussions until I come back. Cheers, Oleg
Hi Oleg!
It has occurred to me a year ago that the type-changing gMap is easily possible in SYB. The recent discussion has prompted me to implement that solution. I have committed a patch to
http://darcs.haskell.org/generics/comparison/SYB1_2/GMap.lhs
with the implementation. I hope this is OK: the previous version of that file was a stub saying that gMap is not supported. The function gMap has the expected type gmap :: (Data a, Data b, Data x, Data y) => (a -> b) -> x -> y
Thanks, looks nice. I suspected there had to be a gfoldl+gunfoldl- based approach, but I couldn't quite wrap my head around it. So simple in hindsight (given the proper auxiliary type constructors), and I might have got there in the end, but it was certainly not "easily possible" for me - so thank you for freeing me from the daily headache of trying yet another approach!-) A slight issue: this version does not distinguish functor parameter from equivalent types: *GMap> gmap not (True,True)::(,) Bool Bool (False,False) Perhaps we can combine our versions to get the best of both?
There are no unsafe operations used; there is not a single occurrence of insafePerformIO and the ilk. Incidentally, Data.Generics could, in principle at least, be implemented using a safe cast. Of course gmap is not a total operation: one can't really expect (gmap id True) to produce a character. It seems that gunfold is not total anyway.
The latter is the reason why this version is safer than mine, I think: 'instance Data (a->b)' implements a fake gfoldl, but turns uses of gunfoldl into runtime errors. Yet another reason why those instances are dubious, but any attempt to fake gunfoldl would have to involve error anyway, it seems (something like 'z (const (error "no such function"))' when grabbing an (a->b) out of thin air). So your version does at least get a proper runtime error in the cases where mine runs right out of type safety..
Regarding the instance of Data for functions: SmashA does define (co-variant) traversal `under lambda'. For example, we can (gmap fromEnum) on a function and convert (Bool->Bool) to (Bool->Int). Please see testt3 in
http://darcs.haskell.org/generics/comparison/SmashA/Syb4A.hs
I do not claim to have any use for that transformation, but it was easy to implement...
I was just surprised that the comparison seemed to make no mention of higher-order (as opposed to higher-kinded) types. Cheers, Claus
It has occurred to me a year ago that the type-changing gMap is easily possible in SYB. The recent discussion has prompted me to implement that solution. I have committed a patch to
http://darcs.haskell.org/generics/comparison/SYB1_2/GMap.lhs
gmap :: (Data a, Data b, Data x, Data y) => (a -> b) -> x -> y
Perhaps we can combine our versions to get the best of both?
To wit: data X = X deriving (Data,Typeable) data Y = Y deriving (Data,Typeable) fmap'' :: (Data (f X), Data (f Y)) => (a -> b) -> f a -> f b fmap'' f = markTheSpots (gmap (wrap f)) where wrap :: (a->b) -> (X->Y) wrap = unsafeCoerce markTheSpots :: (f X -> f Y) -> (f a -> f b) markTheSpots = unsafeCoerce so that: *GMap> gmap not (True,True) :: (,) Bool Bool (False,False) *GMap> fmap'' not (True,True) :: (,) Bool Bool (True,False) fmap'' is safer than the original fmap', in that trying to map over functions will run into the gunfold runtime error, eg: *GMap> fmap'' (\True->'c') (id::Bool->Bool) True *** Exception: gunfold I keep worrying that I should do something more to hide X/Y, perhaps similar to the runST trick, but (a) while it was easy to show type-unsafety in fmap' in the presence of non-traversing Data instances, I have yet to find an example exposing X/Y in fmap'', and (b) pretending to be fully polymorphic is not necessarily appropriate in a generic programming context;-) So using specific, but unknown types doesn't feel entirely wrong. gmap doesn't know about X/Y, so can only treat them generically, and the same goes for f, if X/Y aren't exported. Of course, the generic toolbox allows to recover the types, but f never sees X/Y, and gmap doesn't seem to care: *GMap> fmap'' dataTypeOf (True,True) :: (,) Bool DataType (True,DataType {tycon = "Prelude.Bool", datarep = AlgRep [False,True]}) *GMap> fmap'' (\X->Y) (True,True) :: (,) Bool Y <interactive>:1:21: Couldn't match expected type `X' against inferred type `Bool' In the expression: True In the second argument of `fmap''', namely `(True, True)' In the expression: fmap'' (\ X -> Y) (True, True) :: (,) Bool Y *GMap> fmap'' (fmap'' not) [(True,Just True,True)] [(True,Just True,False)] *GMap> fmap'' (gmap not) [(True,Just True,True)]::[(Bool,Maybe Bool,Bool)] [(False,Just False,False)] Still, the problem with these kinds of proofs is not to show that the cases one has thought of are safe, but to be sure that there are no unsafe cases one hasn't thought of. So, more minds/eyeballs are welcome!-) Claus ps. gmap itself is somewhat tricky to use, depending on type information from the context, and failing with runtime errors if that type information doesn't match. *GMap> gmap not (True,True) :: (Bool,Char) (False,*** Exception: gunfold But then, SYB generally operates at the borders of type safety (what one would expect to be a type error often just leads to unexpected behaviour - there are so few gaps between well-typed SYB programs that the type system, instead of noting that things go wrong, can only cause things to go elsewhere). Are the other generic programming libraries better behaved in this area?
Hello! Claus wrote:
Perhaps we can combine our versions to get the best of both?
I have done so. I have committed a new version of /comparison/SYB1_2/GMap.lhs with gmap2 of the type
gmap2 :: forall a b c . (Data a, Data b, Data (c a), Data (c b), Data (c X)) => (a -> b) -> c a -> c b
The compositionality tests seem to pass. There are no unsafe operations or any unsafe extensions. Only standard Data.Typeable and Generics.Data operations are being used. The code also contains an optimization: if it is determined that a structured value has no components to map, no traversal is performed and the value is returned as it is. That should speed things up a little. The trick is producing something out of nothing. Too bad that the deadline to amend a Haskell workshop paper has passed, and so has the deadline for the generics workshop. Perhaps we should write a separate paper? I'm afraid I would be out of town again for two weeks and so would not be able to follow the discussion closely. Cheers, Oleg
I have done so. I have committed a new version of /comparison/SYB1_2/GMap.lhs with gmap2 of the type
Interesting.
gmap2 :: forall a b c . (Data a, Data b, Data (c a), Data (c b), Data (c X)) => (a -> b) -> c a -> c b
The compositionality tests seem to pass. There are no unsafe operations or any unsafe extensions. Only standard Data.Typeable and Generics.Data operations are being used. The code also contains an optimization: if it is determined that a structured value has no components to map, no traversal is performed and the value is returned as it is. That should speed things up a little. The trick is producing something out of nothing.
Too bad that the deadline to amend a Haskell workshop paper has passed, and so has the deadline for the generics workshop. Perhaps we should write a separate paper?
We're thinking about extending the Haskel Symposium paper to a journal version, in which we would also take efficiency into account (i.e., also try to set up something like a benchmark for generic programming). Would something like that be suitable you think? -- Johan
On Tue, Jul 29, 2008 at 9:51 AM,
Hello!
Claus wrote:
Perhaps we can combine our versions to get the best of both?
I have done so. I have committed a new version of /comparison/SYB1_2/GMap.lhs with gmap2 of the type
gmap2 :: forall a b c . (Data a, Data b, Data (c a), Data (c b), Data (c X)) => (a -> b) -> c a -> c b
The compositionality tests seem to pass. There are no unsafe operations or any unsafe extensions. Only standard Data.Typeable and Generics.Data operations are being used. The code also contains an optimization: if it is determined that a structured value has no components to map, no traversal is performed and the value is returned as it is. That should speed things up a little. The trick is producing something out of nothing.
That's a clever combination of both techniques. You are passing around an explicit type representation at run-time, to ensure that the transforming function applies only to X-positions. Also you don't pretend that there are X-values in there (as Claus' version did) so there is no need for unsafeCoerce. One question: the runtime checks in traverse are for internal consistency only, right?. I could not think of runtime errors arising from gmap2-calls. Furthermore, I think the issue of unfold errors is solved, right? (Although these properties are not known by the type system.)
Too bad that the deadline to amend a Haskell workshop paper has passed, and so has the deadline for the generics workshop. Perhaps we should write a separate paper?
Yes, that's a pity. I will mention this in the presentation though (and update the technical report, which admittedly is rather delayed).
I'm afraid I would be out of town again for two weeks and so would not be able to follow the discussion closely.
Cheers, Alexey
Hello!
Hello again!-)
Claus wrote:
Perhaps we can combine our versions to get the best of both?
I have done so. I have committed a new version of /comparison/SYB1_2/GMap.lhs
[for readers of libraries@: that is in the generics code repo at http://darcs.haskell.org/generics/comparison/SYB1_2/GMap.lhs , look for gmap2/gmapt and comments; the topic is defining Functor fmap generically (hence gmap) in terms of Data/Typeable] Ah, of course! Silly me, if I had followed my own choice of metaphor to the end, I would have known that X marks the spot only on a map, not on the real thing (or else everyone could find the treasure..). Your shallow, incrementally built not-quite copy is just another representation of a map, and since both map and X are hidden from users of the function, everyone is happy. That something out of nothing trick is also used in the PlateData optimization and in my adaptation of it. The difference, apart from choice of representation, is mainly in whether to extract substructure placeholders/types on a type basis once per traversal or on a value basis, incrementally. Here is a re-run of the technique, for defining traverse in terms of Data/Typeable. Apart from being useful for Data.Traversable library users, the type of 'traverse id' is similar to the type of transpose, which should interest the generics readers. {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} import Control.Applicative import Data.Generics data X = X deriving (Data,Typeable) traverseData :: forall f a b t . (Applicative f,Typeable1 f,Typeable a,Typeable b, Data (t a),Data (t b),Data (t X)) => (a -> f b) -> t a -> f (t b) traverseData f = traverseWithMap f (Dyn (undefined::t X)) where traverseWithMap :: forall f a b x y . (Applicative f,Typeable1 f,Typeable a,Typeable b,Data x,Data y) => (a -> f b) -> Dyn -> x -> f (y) traverseWithMap f (Dyn t) x | typeOf t==typeOf X = maybe (error "traverseData: non-applicable type marked") ($x) (cast f) | otherwise = rebuildWith (traverseWithMap f) t1 x where t1 = Dyn (fromConstr (toConstr x) `asTypeOf` t) rebuildWith :: forall f x y . (Applicative f,Data x,Data y) => (forall x y . (Data x,Data y) => Dyn -> x -> f y) -> Dyn -> x -> f y rebuildWith f (Dyn t) x = case gunfold (k f) (\g -> UnfldStateF2 (pure g) tkids kids) con of UnfldStateF2 a [] [] -> a where (tcon,tkids) = dynamize t (con,kids) = dynamize x k :: forall a b . (Data a) => (forall x y . (Data x,Data y) => Dyn -> x -> f y) -> UnfldStateF2 f (a->b) -> UnfldStateF2 f b k f (UnfldStateF2 ca (tkid:tkids) ((Dyn kid):kids)) = UnfldStateF2 (ca <*> (f tkid kid)) tkids kids data UnfldStateF2 f a = UnfldStateF2 (f a) [Dyn] [Dyn] data Dyn = forall a. Data a => Dyn a data Kids a = Kids{growUp:: [Dyn]} dynamize :: Data a => a -> (Constr,[Dyn]) dynamize x = (toConstr x, growUp $ gfoldl f (const (Kids [])) x) where f (Kids l) a = Kids (l ++ [Dyn a]) test = do print $ traverseData (Just . not) tuple print $ traverseData (Just . not) list traverseData print tuple >>= print traverseData print list >>= print where tuple = (True,True) list = [True,True] Btw, while the type of 'traverseData id' matches that of transpose, its behavious doesn't quite, depending on example: *Main> :t traverseData id traverseData id :: (Data (t X), Data (t b), Data (t (f b)), Typeable b, Typeable1 f, Applicative f) => t (f b) -> f (t b) *Main> traverseData id [Just x|x<-[1..3]] Just [1,2,3] *Main> traverseData id [[1..3],[4..6]] [[1,4],[1,5],[1,6],[2,4],[2,5],[2,6],[3,4],[3,5],[3,6]]
optimization: if it is determined that a structured value has no components to map, no traversal is performed and the value is returned as it is. That should speed things up a little. The trick is producing something out of nothing.
That optimization is another indication of the relation to the substructure types map building, although pleasingly different in form (always nice to learn new tricks;-).
Too bad that the deadline to amend a Haskell workshop paper has passed, and so has the deadline for the generics workshop. Perhaps we should write a separate paper?
Sounds like a good idea. When you're back.
I'm afraid I would be out of town again for two weeks and so would not be able to follow the discussion closely.
Ah, you're just trying to hide the two-week round trips for lightspeed messages resulting from your space travels!-) Thanks for yet another useful contribution, Claus
Hello! Alexey wrote:
One question: the runtime checks in traverse are for internal consistency only, right?. I could not think of runtime errors arising from gmap2-calls. Furthermore, I think the issue of unfold errors is solved, right? (Although these properties are not known by the type system.)
Yes, this is correct. Although gmap2 could be given a more general type, like (a -> b) -> f x -> f y in which case the run-time errors are significant. Such errors will arise when mapping id on [Int] and expect [Bool] in the result. The mapping will succeed btw on empty lists. Alexey wrote:
I will mention this in the presentation though (and update the technical report, which admittedly is rather delayed).
Thank you! Perhaps the journal version of the comparison paper (which several people suggested) could discuss the issue in some detail (at least from the perspective of performance and static-dynamic trade-off). It seems there might be a possibility of a five-minute presentation about gmap during the `Hot Topics' discussion at the Generic Programming Workshop in Victoria in September -- provided the organizers will schedule the hot topics session and deem gmap hot enough. Should we inquire the workshop organizers? I will be back on Aug 18. I was in Japan and Taiwan in July, and will be in Germany (Hamburg) in August. I guess I get a chance to compare German trains with Japanese ones. Claus wrote:
if I had followed my own choice of metaphor to the end, I would have known that X marks the spot only on a map, not on the real thing (or else everyone could find the treasure..).
I really like that metaphor! Cheers, Oleg
Hi Claus,
On Wed, Jul 2, 2008 at 12:11 PM, Claus Reinke
ps. gmap itself is somewhat tricky to use, depending on type information from the context, and failing with runtime errors if that type information doesn't match.
*GMap> gmap not (True,True) :: (Bool,Char) (False,*** Exception: gunfold
But then, SYB generally operates at the borders of type safety (what one would expect to be a type error often just leads to unexpected behaviour - there are so few gaps between well-typed SYB programs that the type system, instead of noting that things go wrong, can only cause things to go elsewhere).
Are the other generic programming libraries better behaved in this area?
A small (and late) reaction to this point. The reason that this particular SYB gmap behaves badly is that deserialization is partial. You will have a runtime error (or exceptional return value) if you deserialize an input as a value of type X while it has been serialized as a value of type Y. Since this version of gmap is based on serialization followed by deserialization, you will obtain such errors when demanding incompatible types (as in your example). I think that Oleg's latest version enforces additional type safety (by means of the gmap2 wrapper) so this problem is no longer present. Other libraries (for example EMGM and RepLib) represent type constructors explicitly, so gmap can be implemented directly without the need of serialization/deserialization. There are no such runtime problems in those approaches. There are other examples of serialization-based generic functions: the implementation of generic transpose by Norell and Jansson [1], and also the generic conversion work by Atanassow and Jeuring[2]. Cheers, Alexey [1] http://citeseer.ist.psu.edu/649955.html [2] http://citeseer.ist.psu.edu/583900.html
Hi Oleg!
On Tue, Jul 1, 2008 at 1:46 PM,
Hello!
It has occurred to me a year ago that the type-changing gMap is easily possible in SYB. The recent discussion has prompted me to implement that solution. I have committed a patch to
http://darcs.haskell.org/generics/comparison/SYB1_2/GMap.lhs
with the implementation. I hope this is OK: the previous version of that file was a stub saying that gMap is not supported. The function gMap has the expected type gmap :: (Data a, Data b, Data x, Data y) => (a -> b) -> x -> y
I have tried the following code:
data Tricky a = Tricky a Char deriving (Data,Typeable,Show) mapTricky :: (Data a,Data b) => (a -> b) -> Tricky a -> Tricky b mapTricky = gmap tricky1 = Tricky 'a' 'b' tr_test1 = mapTricky (=='a') tricky1 tr_test2 = mapTricky (chr . (+1) . ord) tricky1
The expression tr_test1 prints *GMap> tr_test1 Tricky True 'b' as one would expect. However, tr_test2 prints: *GMap> tr_test2 Tricky 'b' 'c' Here the transforming function is applied to *both* the functor argument and the Char value. The argument of gmap is not only applied to the functor argument but also to 'b' in "tricky1". This problem was already pointed out by Claus. It is important to remark that although gmap passes the test in the benchmark, it does not behave like a functorial map. Furthermore, this trick cannot be reused to implement the crush test. Nevertheless, it is surprising (to me at least) that you can implement something close to type changing map, using only SYB's cast operation. I am going to update the "Comparing libraries" paper to refer to your and Claus' variants of gmap.
There are no unsafe operations used; there is not a single occurrence of insafePerformIO and the ilk. Incidentally, Data.Generics could, in principle at least, be implemented using a safe cast. Of course gmap is not a total operation: one can't really expect (gmap id True) to produce a character. It seems that gunfold is not total anyway.
Yes. The more flexible type turns what would have been type errors into strange runtime behaviour: *GMap> gmap (id::Maybe () -> Maybe ()) (Just ()) :: Bool *** Exception: SYB1_2/GMap.lhs:(20,26)-(21,45): Non-exhaustive patterns in case *GMap> gmap (id::Maybe () -> Maybe ()) (Nothing::Maybe ()) :: Bool False Cheers, Alexey
participants (4)
-
Alexey Rodriguez -
Claus Reinke -
Johan Jeuring -
oleg＠okmij.org