[Haskell-cafe] Re: A problem with nested regions and higher-order?functions

Chung-chieh Shan ccshan at post.harvard.edu
Mon Sep 8 09:30:16 EDT 2008


Mario Bla??evi?? <mblazevic at stilo.com> wrote in article <23051.1216949255$1220747147 at news.gmane.org> in gmane.comp.lang.haskell.cafe:
> 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



More information about the Haskell-Cafe mailing list