Mario Bla??evi??
I'm trying to apply the nested regions (as in Lightweight Monadic Regions by Oleg Kiselyov and Chung-chieh Shan) design pattern, if that's the proper term, in hope to gain a bit more type safety in this little library I'm working on (Streaming Component Combinators, available on Hackage). I guess the problem is that I'm getting too much type safety now, because I can't get the thing to compile. ...
Hi! Thanks for your interest. It sounds like a promising application of region checking. I actually side with the type checker on this problem:
type SingleHandler x y = forall r1s rs. Ancestor r1s rs => Handle r1s x -> Region rs y type DoubleHandler x y z = forall r1d r2d rd. (Ancestor r1d rd, Ancestor r2d rd) => Handle r1d x -> Handle r2d y -> Region rd z
Here a SingleHandler is defined as an operation, in an arbitrary region on an arbitrary handle, that is valid as long as the region of the operation descends from the region of the handle. For example, reading a string from an arbitrary open file is a "SingleHandler File String". However, copying a string from an arbitrary open file to another fixed file is not a SingleHandler, because such an operation is valid only in a region that descends from the destination file handle's region! That's what GHC complained about as it checks your mapD:
mapD :: (SingleHandler x z -> SingleHandler y z) -> DoubleHandler x w z -> DoubleHandler y w z mapD f d = \y w-> f (\x-> d x w) y
So we really need to change the type of mapD if we want it to be accepted by a sound type system. The simplest way is to not require that mapD return a DoubleHandler (a binary operation that works in an arbitrary region): mapD :: ((Handle r1 x -> Region r z) -> (Handle r1 x -> Region r z)) -> ((Handle r1 x -> Handle r2 w -> Region r z) -> (Handle r1 x -> Handle r2 w -> Region r z)) mapD f d = \y w-> f (\x-> d x w) y This type is a special case of the type automatically inferred for mapD by Haskell if you omit the type signature. Haskell doesn't have any trouble type-checking higher-order functions, such as this mapD, but higher-rank types can call for manual annotations, as illustrated below. Another way to get mapD to type-check is to pass it (as its first argument) not a SingleHandler transformer but a transformer of operations that may work only in descendents of a given region r2. We want to write type H r2 x y = forall r1 r. (Ancestor r1 r, Ancestor r2 r) => Handle r1 x -> Region r y mapD :: (forall r2. H r2 x z -> H r2 y z) -> DoubleHandler x w z -> DoubleHandler y w z mapD f d = \y w-> f (\x-> d x w) y ("forall r2" takes scope over both "H r2 x z" and "H r2 y z" above) but GHC doesn't see that we intend to unify the "r2d" in the expansion of "DoubleHandler y w z" with the "r2" in this type signature of "mapD". So, we need to put an explicit type annotation on the use of "f" in the body of "mapD". To do so, we add {-# LANGUAGE ScopedTypeVariables #-} and expand the type synonym "DoubleHandler y w z" in the type signature of "mapD": mapD :: forall x y z w r1d r2d rd. (Ancestor r1d rd, Ancestor r2d rd) => (forall r2. H r2 x z -> H r2 y z) -> DoubleHandler x w z -> Handle r1d y -> Handle r2d w -> Region rd z mapD f d = \y w-> (f :: H r2d x z -> H r2d y z) (\x-> d x w) y Not so pretty anymore, but it does pass the type checker (GHC 6.8.2). -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig ----- Ken Shan