An ML reference type Both dereferences now give one. A reference's stored type remains fixed; the value restriction prevents allocating one unrestricted polymorphic cell and then using incompatible instantiations.
'a ref describes a mutable cell holding a value of type 'a. The operations are ref : 'a -> 'a ref for allocation, ! : 'a ref -> 'a for dereferencing and := : 'a ref * 'a -> unit for assignment. An immutable variable binding can name a mutable cell; assigning to the cell does not change what the binding denotes. Two names may alias the same cell, so an update through either is visible through the other.val counter = ref 0;
val alias = counter;
counter := !counter + 1;Imperative programming uses sequencing References provide mutable state; sequencing, conditionals and loops control its updates.
(e1; e2; ...; en) to perform effects left to right, with the final expression supplying the result. Conditional expressions choose one branch. while condition do body repeatedly checks a Boolean condition and performs a unit-valued body, returning () on termination. Standard ML has no required primitive for loop, but recursion or a reference with while supplies one. For example:fun sumTo n =
let val i = ref 1
val total = ref 0
in
while !i <= n do
(total := !total + !i; i := !i + 1);
!total
end;Carry the list as an immutable accumulator instead of storing it in a reference:For any initial accumulator
fun snackerPure m =
let
fun collect (Snack x, acc) = x :: acc
| collect (Lunch (a, b), acc) =
collect (b, collect (a, acc))
| collect (Feast (a, b, c), acc) =
collect (c, collect (b, collect (a, acc)))
in
collect (m, [])
end;acc, structural induction shows that collect(m,acc) equals the final reference content obtained by traversing m left to right and prepending each snack to a reference initially containing acc. At Lunch and Feast, the accumulator passed to each child is the result of all earlier children, exactly matching the imperative sequencing. Thus the result is the reverse of the left-to-right list of snack labels, just as for the original snacker; returning the ordinary left-to-right list would be incorrect. The code uses no mutable cells and is polymorphic, with type 'a meal -> 'a list.Apply structural recursion to the original meal, preserving its internal constructors and replacing each leaf:The type is
fun gluttony (Snack _) replacement = replacement
| gluttony (Lunch (a, b)) replacement =
Lunch (gluttony a replacement, gluttony b replacement)
| gluttony (Feast (a, b, c)) replacement =
Feast (gluttony a replacement, gluttony b replacement,
gluttony c replacement);'a meal -> 'b meal -> 'b meal: original snack labels are discarded, so the replacement can have a different label type. The constructors introduced by the replacement are not recursively processed; only snacks of the original tree are substituted. The immutable replacement can be shared among occurrences without changing the represented value. Every original Snack is replaced, while the original internal meal structure is retained.Carry the number of original snacks still to skip, returning it together with the reconstructed subtree. Zero means that the replacement has already happened:The successive bindings explicitly establish left-to-right counting. Before the target is reached, each original snack decreases the counter by one; at the target the subtree becomes
fun glut k meal replacement =
let
fun visit (t, 0) = (t, 0)
| visit (Snack x, j) =
if j = 1 then (replacement, 0)
else (Snack x, j - 1)
| visit (Lunch (a, b), j) =
let val (a1, j1) = visit (a, j)
val (b1, j2) = visit (b, j1)
in (Lunch (a1, b1), j2) end
| visit (Feast (a, b, c), j) =
let val (a1, j1) = visit (a, j)
val (b1, j2) = visit (b, j1)
val (c1, j3) = visit (c, j2)
in (Feast (a1, b1, c1), j3) end
in
if k < 1 then raise Subscript
else
let val (answer, remaining) = visit (meal, k)
in if remaining = 0 then answer else raise Subscript end
end;replacement and the counter becomes zero. Subsequent subtrees are returned unchanged, and newly inserted snacks are never counted. Structural induction on the helper's subtree establishes this invariant and proves the specified one-based substitution. The result has type int -> 'a meal -> 'a meal -> 'a meal. Since unaltered original snacks remain, their label type must agree with the replacement's label type.The behavior for an invalid index is not specified in the PDF; this implementation deliberately raises
Subscript for or too few snacks. For valid input, exactly the th original snack in left-to-right order is replaced. Sharing untouched immutable subtrees is semantically equivalent to a fresh structural copy. Articles by others on the same topic
There are currently no matching articles.