haskell-cafe@haskell.org
[Top] [All Lists]

[Haskell-cafe] Re: Type system speculation

Subject: [Haskell-cafe] Re: Type system speculation
From:
Date: Wed, 9 Dec 2009 23:40:27 -0800 PST
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.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/haskell-cafe

<Prev in Thread] Current Thread [Next in Thread>