Andrew Coppin wrote:
What we're really trying to do here is attach additional information to a value - information which exists only in the type checker's head, but has no effect on runtime behaviour (other than determining whether we *get* to runtime). As far as I can tell, Haskell does not provide any way to take an existing type and attach additional information to it in such a way that code which cares about the new information can make use of it, but existing code which doesn't care continues to work. Any comments on this one?
Haskell has had the ability to attach arbitrary many pieces of (type-level) data to arbitrary types for a long time -- ever since multi-parameter type classes and functional dependencies have been introduced. Nowadays, type families accomplish the same with fewer keystrokes. One merely needs to define a type family type family Attrib n index :: * which maps the existing type n and the index to an arbitrary type. Chung-chieh Shan and I have explored the technique to annotate data types with attributes describing alignment of the corresponding data, location in ROM or RAM, etc. http://okmij.org/ftp/Haskell/types.html#ls-resources Here is a sample annotation, from http://okmij.org/ftp/Computation/resource-aware-prog/VideoRAM.hs -- A Screen on old PC type ScreenCharT = Pair AWord8 AWord8 -- attribute and char proper scrchar_attr r = afst r scrchar_char r = asnd r type ScreenT = Array N25 (Array N80 ScreenCharT) data Screen = Screen instance Property Screen APInHeap HTrue instance Property Screen APARef (ARef N8 ScreenT) instance Property Screen APReadOnly HFalse instance Property Screen APOverlayOK HTrue -- many more can be added, perhaps in other modules type SmallScreenT = Array N5 (Array N80 ScreenCharT) -- we can place the Screen area at a fixed absolute address data ScreenAbs = ScreenAbs instance Property ScreenAbs APInHeap HFalse instance Property ScreenAbs APARef (ARef N8 ScreenT) instance Property ScreenAbs APReadOnly HFalse instance Property ScreenAbs APFixedAddr HTrue If we forget to assign property APReadOnly=HFalse, an operation write_area that uses a pointer in the area raises a type error.