home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / gofer230.zip / Progs / Gofer / Demos / Lamvar / readme.lvr < prev    next >
Text File  |  1994-06-23  |  7KB  |  246 lines
  1. ------------------------------------------------------------------------------
  2. This document contains a brief introduction to the use of the current
  3. experimental features for imperative programming in Gofer.  These
  4. features can only be used if the Gofer interpreter is compiled with
  5. the LAMBDAVAR symbol #defined, for example, by adding a -DLAMBDAVAR
  6. to the CFLAGS line in the Makefile.
  7.  
  8. These notes were written by Martin Odersky ... I have made a couple
  9. of changes to reflect the current syntax used in the Gofer version;
  10. I believe that this document correctly reflects the current set of
  11. features provided by Gofer.
  12.  
  13. I should also emphasise that, as experimental features, these
  14. extensions are subject to change in later releases.  For example,
  15. the Glasgow Haskell system uses the type constructor IO where we
  16. have used Proc here.  The first of these names seems to be gaining
  17. a consensus and Gofer may well be modified to reflect this in some
  18. future release.
  19.  
  20. ------------------------------------------------------------------------------
  21.  
  22. An introduction to Gofer's imperative constructs
  23. ================================================
  24.  
  25.  
  26. This short paper describes a library for imperative programming.
  27. The library consists of functions that operate on an two abstract types
  28.  
  29.     Var a        and         Proc a
  30.  
  31. "Var a" is the type of mutable variables that contain terms of type
  32. "a".  "Proc a" is the type of procedures that return a result of type
  33. "a".  Conceptually, a procedure is a function from states to pairs of
  34. states and results.
  35.  
  36.     Proc a     ~~    State -> (State, a)
  37.  
  38. A state can be thought of as a function that maps a mutable variable
  39. to its "current" value. States cannot be typed in Gofer, and they need
  40. not be, since for the purposes of type checking "Proc a" is an opaque
  41. type. In fact, the implementation of procedures does not use the above
  42. type synonym for "Proc a". For efficiency reasons it uses a global
  43. state that is updated destructively.
  44.  
  45. Any expression with type  Proc ()  will be executed as an imperative
  46. program by the Gofer interpreter.
  47.  
  48. The library contains the following functions.
  49.  
  50. 1. Mutable variables are created by the function
  51.  
  52. >     newvar :: Proc (Var a).
  53.  
  54. Executing the term
  55.  
  56.     newvar 
  57.  
  58. has the effect that a fresh, uninitialized variable is allocated and returned
  59. as a result.
  60.  
  61.  
  62. 2. Mutable variables are read and written using the functions:
  63.  
  64. >    (=:) :: a -> Var a -> Proc ()
  65. >
  66. >    deref  :: Var a -> Proc a
  67.  
  68. Executing the term 
  69.  
  70.     A =: V
  71.  
  72. has the effect of assigning A to variable V and returning the unit
  73. value ().  Note that A is not evaluated prior to the assignment.
  74.  
  75. Executing the term 
  76.  
  77.     deref V
  78.  
  79. has no effects on the state and returns the term that was last
  80. assigned to V.
  81.  
  82.  
  83. 3. Another primitive state transformer is
  84.  
  85. >    result :: a -> Proc a
  86.  
  87. Executing the term 
  88.  
  89.     result A
  90.  
  91. has no effects on the state and returns A as result.
  92.  
  93.  
  94. 4. Procedures are composed using the functions:
  95.  
  96. >    (>>)  :: Proc () -> Proc b -> Proc b
  97. >    (>>=) :: Proc a -> (a -> Proc b) -> Proc b
  98. >    (?)   :: Var a -> (a -> Proc b) -> Proc b
  99.  
  100. (>>) is sequential composition.  Executing the term
  101.  
  102.     P >> Q
  103.  
  104. first executes procedure P in the current state S, giving a new state
  105. S'. It then executes Q in the new state S'.
  106.  
  107. (>>=) is the "bind" operator of the state monad.  Executing the term
  108.  
  109.     P >>= Q
  110.  
  111. first executes procedure P in the current state S, giving a new
  112. state S' and a returned result R. It then executes (Q R) in the
  113. new state S'. 
  114.  
  115. (?) is a combination of (>>=) and (deref). Executing the term
  116.  
  117.     V ? Q
  118.  
  119. passes to procedure Q the term that is currently assigned to variable V.
  120.  
  121.  
  122. Note that
  123.  
  124.     P >> Q     =   P >>= \() -> Q.
  125.     V ? Q    =   deref V >>= Q
  126.  
  127. Note also that (result) and (>>=) form a monad, since the following laws 
  128. hold:
  129.  
  130.     result A >>= B          =    B A
  131.     A >>= \x -> result x    =    A
  132.     (A >>= \x -> B) >>= C   =    A >>= ((\x -> B) >>= C)
  133.                      if x not free in C     
  134.  
  135.  
  136. 5. An imperative computation can be encapsulated using the function
  137.  
  138.     pure :: Proc a -> a
  139.  
  140. Executing the term
  141.  
  142.     pure P
  143.  
  144. executes procedure P in an empty initial state. It returns the final
  145. result returned by P while discarding the final state.
  146.  
  147. NOTE: (pure P) is referentially transparent only if two conditions
  148. are met.
  149.  
  150.   1. The body of P may only refer to variables allocated inside P.
  151.   2. The result of P may not refer to variables allocated inside P.
  152.  
  153. Currently, it is the programmer's obligation to verify that these
  154. conditions hold. They are not checked by the compiler.  This is an
  155. implementation restriction, NOT a language feature. It is anticipated
  156. that some future version of the compiler will enforce the conditions.
  157.  
  158. 6. Simple imperative I/O:
  159.  
  160. >    getchar :: Proc Char
  161. >    getch    :: Proc Char
  162. >    putchar :: Char -> Proc ()
  163. >    puts    :: String -> Proc ()
  164.  
  165. The getchar and getch processes return a character typed on the standard
  166. input stream, with or without echoing the character on the standard output
  167. respectively.
  168.  
  169. Executing the term
  170.  
  171.     putchar C
  172.  
  173. causes the character given by the expression C to be printed on the standard
  174. output.  In a similar way, executing the term
  175.  
  176.     puts S
  177.  
  178. causes the string S to be displated on the standard output.
  179.  
  180.  
  181. Programming Examples:
  182. =====================
  183.  
  184. 1. A swap procedure:
  185.  
  186. >    swap :: Var a -> Var a -> Proc ()
  187. >    swap v w =
  188. >      v ? \x ->
  189. >      w ? \y ->
  190. >      x =: w >>
  191. >      y =: v
  192.  
  193. 2. Forming lists of mutable variables
  194.  
  195. >    newvars       :: Int -> Proc [Var a]    
  196. >    newvars 0     =  result []
  197. >    newvars (n+1) =  newvar    >>= \v ->
  198. >                  newvars n >>= \rest -> 
  199. >             result (v:rest)
  200.  
  201. "newvars n" forms a list of "n" fresh mutable variables.
  202.  
  203.  
  204. 3. An iterator:
  205.  
  206. >    seq :: [Proc ()] -> Proc ()
  207. >    seq =  foldr (>>) (result ())
  208.  
  209. To exchange the contents of all variables in two lists:
  210.  
  211. >    swapall       :: [Var a] -> [Var a] -> ([Var a], [Var a])
  212. >    swapall xs ys =  seq [swap v w | (v,w) <- zip xs ys]
  213.  
  214.  
  215. 4. Simple I/O:
  216.  
  217. The getchar and puts functions are defined in terms of the getch and
  218. putchar primitives:
  219.  
  220. >    getchar :: Proc Char
  221. >    getchar  = getch     >>= \c ->
  222. >               putchar c >>
  223. >               result c
  224.  
  225. >    puts    :: String -> Proc ()
  226. >    puts     = seq . map putchar
  227.  
  228.  
  229. More material about the semantics of these imperative constructs, and
  230. the algebraic reasoning methods associated with them, is contained in
  231. [1]. See also [2] for a similar approach.
  232.  
  233.  
  234. [1] Martin Odersky, Dan Rabin and Paul Hudak:
  235.     "Call-by-name, Assignment, and the Lambda Calculus".
  236.     Proc. 20th ACM Symp. on Principles of Programming Languages, 
  237.     pp 43-56, January 1993.
  238.  
  239. [2] Simon Peyton Jones and Philip Wadler:
  240.     "Imperative Functional Programming".
  241.     Proc. 20th ACM Symp. on Principles of Programming Languages, 
  242.     pp 71-84, January 1993.
  243.  
  244.  
  245. ------------------------------------------------------------------------------
  246.