[Haskell-cafe] Re: Type system speculation

[oleg at okmij.org]

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.