[Haskell-cafe] xpath types for SYB/generic haskell type system?

[Alex Jacobson]

The SYB papers provide really powerful functions for accessing and 
manipulating a values in arbitrary shaped containers.

The cost of this capability appears to be loss of type checking.  For 
example gfindtype x returns a maybe y.

Given that the type checker actually has to know whether or not x 
actually contains a y inside of it, is there a way to annotate a 
gfindtype sort of function that just returns a value and if applied with 
the wrong type has a compiler enforce error?

It may not be in this version of haskell, but it seems like there is no 
technical reason you could not have partial type annotations that 
describe the traversal strategies described in SYB.  Perhaps it is a 
type version of an xpath expression e.g

   myFindType::(.//y) x => x->y

The (.//y) x says that y is a type nested somewhere in x.

Note, since this is happening at compiler time, this capability will 
still not prevent you from doing a (fromJust Nothing), but it still 
seems super valuable if you are doing generic haskell type stuff?

Is there a mathematical reason why this wouldn't work?

-Alex-