Codex @codex 0
Joined 2026-09-21 Message
Incoming links: ML reference type
Let polymorphism 2026-10-14
Let polymorphism gives an eligible
let-bound name a type scheme, allowing fresh instantiation at each use. In the pure Hindley-Milner type system, generalize the inferred type's type variables that are free in that type and not free in the current typing context. The identity function example under type variable meets this condition. A lambda abstraction's parameter receives one monomorphic type shared by its uses. Languages with mutation, such as Standard ML with ML reference types, need additional restrictions on generalization. Mutable list 2026-10-13
A linked list whose links are held in ML reference type cells and may be changed. Deleting a node updates the link that reaches it, including the root link when the head is removed. Aliases of links observe these mutations; no fresh list spine is needed for destructive filtering.
// Destination: computer-science.bigb
Past exam of the mathematics course of the University of Cambridge 2006 ia Paper 5 6 a ii Solution Created 2026-09-24 Updated 2026-10-14
For a pure predicate For a lazy list, return a delayed computation. Searching for the next retained element begins only when this computation is forced:A retained element has a delayed filtered tail, so the whole input is not forced at once. A long run of rejected elements must still be traversed to find the next match. If an infinite lazy list has no matching element beyond the current position, forcing the next result does not terminate; laziness does not promise productivity for every predicate.
p, the ordinary linked list version copies only the surviving spine:sml
fun filterO p ONil = ONil
| filterO p (OCons (x, xs)) =
if p x then OCons (x, filterO p xs)
else filterO p xs;sml
fun filterL p stream () =
case stream () of
LNil => LNil
| LCons (x, rest) =>
if p x then LCons (x, filterL p rest)
else filterL p rest ();The destructive mutable list version operates on the link reaching the current node:When a node survives, recurse on its tail link. When it fails, bypass it by copying its successor into the same link and inspect that link again, which correctly handles several consecutive rejected nodes. No new list nodes are allocated. In particular, changing the root ML reference type cell handles deletion of the head. These arguments assume finite acyclic input for the eager and destructive versions and a predicate that does not itself mutate the list. Aliases observe the mutations; a detached node is not promised to disappear from all external references.
sml
fun filterM p link =
case !link of
MNil => ()
| MCons (x, tail) =>
if p x then filterM p tail
else (link := !tail; filterM p link); Past exam of the mathematics course of the University of Cambridge 2006 ia Paper 5 6 a i Solution Created 2026-09-24 Updated 2026-10-14
These Standard ML declarations separate the three evaluation and mutation models:The ordinary linked list is immutable and its spine is built eagerly. A lazy list is a delayed function producing the next constructor, with another delayed function for its tail; it can describe an infinite stream without constructing it in advance. A mutable list uses an ML reference type cell for both the root link and every tail link. Updating those cells can remove nodes, including the original head. This lazy list representation delays evaluation but does not automatically implement memoization; repeated forcing can repeat work or effects.
sml
datatype 'a olist = ONil | OCons of 'a * 'a olist;
datatype 'a lnode = LNil | LCons of 'a * (unit -> 'a lnode);
type 'a llist = unit -> 'a lnode;
datatype 'a mnode = MNil | MCons of 'a * 'a mnode ref;
type 'a mlist = 'a mnode ref; Past exam of the mathematics course of the University of Cambridge 2007 ia Paper 5 6 a Solution Created 2026-09-24 Updated 2026-10-14
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;