Hi, Annotated type systems have been around for some time in static program analysis. I think this is what you want. For instance, you can design such a system to record possible side effects from a function call, as annotations on the type of the function.
See the book "Principles of Program Analysis", http://www2.imm.dtu.dk/~riis/PPA/ppa.html. Björn Lisper David Roundy: >Hello all, > >I was thinking this morning as I lay on the floor (where I sleep) about >static typechecking, and how much more wonderful Haskell is than any other >language, when it occurred to me that when working with pointers, Haskell >actually has *less* static typechecking than C or C++. It was a very >disturbing thought, so much so that I was almost compelled to arise early >to place this question before this learned audience. > >Why is it that in C++ I can write > >void strcpy(char *dest, const char *src); > >but in Haskell I must import this function as > >> foreign import ccall unsafe "static string.h strcpy" >> strcpy :: Ptr CChar -> Ptr CChar -> IO () > >and lose that wonderful information that the function doesn't modify the >contents of its second argument? > >One could pretty easily create a ConstPtr type which one could peek into, >but not poke to, but then you'd have to explicitely convert a Ptr into a >ConstPtr when passing it as an argument. That feels a bit silly. > >One could get around this by introducing a class to get around this > >> class ReadablePtr p where >> peek :: p a -> IO a >> peekOff ... > >and then make both Ptr and ConstPtr instances of this class, but this still >seems like a very hackish solution. > >Moreover, I'd like to be able to have const objects quite apart from Ptrs, >such as a const Handle, which I can read from, but cannot write to, or a >const IORef--and we wouldn't want to leave out const ForeignPtrs. Of >course, even reading affects a Handle's internal state, so one would need >to be explicit about what "const" indicates. But it seems to me that in >the IO world there are a whole slew of "things that refer to other things" >which could all be grouped together. > >And a "const" attribute ought to be derived, so that if I create a data >type > >> data FooPtr = FooPtr String (Ptr Foo) > >one should ideally be able to automatically understand that a const FooPtr >holds a const (Ptr Foo). > >One could go further, at least when dealing with Ptrs, and create a way of >handling "restricted" pointers--which we could interpret as a const pointer >to an object that cannot be changed by anyone else either. One could >safely create restricted pointers with a function of the type > >> mallocRestrictedPtr :: (Ptr a -> IO ()) -> RestrictedPtr a > >which would allow one to ensure at the typechecking level that >RestrictedPtrs point to memory that cannot be modified. There's still some >unstafety involved, in that you could read out of bounds, but you would >know that apart from that possibility the contents of a RestrictedPtr truly >will never change. > >So my question is, how would one implement such an "annotation" extension? >I'd like to be able to pass a (Ptr a) as a (Const (Ptr a)) without an >explicit typecast, since the Const really isn't changing the type of the >pointer, it's just marking it as one that can't be modified. A function >that accepts a (Const (Ptr a)) should also accept a (Restricted (Ptr >a))--but Restricted pointers are really just pudding, as they only differ >from Const pointers in what optimizations are allowed. On the other hand, >it's not just compiler optimizations that they would allow, but also >user-code optimizations, which could be much more useful. They also have >the advantage of making certain unsafe functions safe. > >The hard part seems to be the lack of a conversion. One could quite easily >implement a > >> data Const a = Const a -- this constructor is *not exported* >> toConst :: x -> Const x >> unsafeAccessConst :: Const x -> x > >> peek :: Const (Ptr a) -> IO a >> peekOff ... > >etc, and everything would work fine, except that you'd always need to >explicitely convert from Ptr to Const Ptr. Perhaps one could make Const be >a class as well as a data type: > >> class (Const a) x where >> toConst :: x -> Const a >> instance (Const x) x where >> toConst = Const >> instance (Const x) (Const x) where >> toConst = id > >and then one could write code like > >> peek :: Const (cp a) => cp a -> IO a > >which would move the typecasting burden out of the calling function and >into the function that accepts a const argument. Perhaps this would be >sufficient, as many data types have only a limited number of "primitive >const" functions, and all the other "const" functions wouldn't actually >need to call toConst. > >What this doesn't allow is deriving of constness, so that a Const >ForeignPtr would automatically hold a Const Ptr. > >This whole class+data type scheme seems like it might be useful, but is >pretty ugly. Is there a better way this could be done? > >Might one be able to extend the language so that one could add "attribute" >such as Const to data type without changing the the type itself (which >would be analogous to what one does in C/C++)? >-- >David Roundy >http://www.darcs.net >_______________________________________________ >Haskell mailing list >Haskell@haskell.org >http://www.haskell.org/mailman/listinfo/haskell _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell